mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.StarRingHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Star A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : Star B
f : A →⋆ₙ+* B
h₁ : ∀ (x y : A), f (x * y) = f x * f y
h₂ : { toFun := ⇑f, map_mul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_mul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_mul' := h₁ }.toFun x + { toFun := ⇑f, map_mul' := h₁ }.toFun y
h₄ :
  ∀ (a : A),
    { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (star a) =
      star ({ toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun a)
x✝ : A
⊢ { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ } x✝ = f x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
v : n → α
⊢ (diagonal fun m ↦ star (v m)) = diagonal (star v)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : Mul α
inst✝ : StarMul α
w : m → α
v : n → α
⊢ (vecMulVec w v).map star = (vecMulVec w v)ᴴᵀ

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x✝ : ↥(skewAdjoint.submodule R A)
x : A
hx : star x = -x
⊢ x = ↑(LinearMap.id ⟨x, hx⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : n
val✝ : l
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val✝¹) (Sum.inl val✝) =
    M (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : n
val✝ : m
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inl val✝¹) (Sum.inr val✝) =
    M (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : o
val✝ : l
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val✝¹) (Sum.inl val✝) =
    M (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
val✝¹ : o
val✝ : m
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ (Sum.inr val✝¹) (Sum.inr val✝) =
    M (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : o
val✝ : l
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inl val✝) = fromBlocks C D A B (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : o
val✝ : m
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inr val✝) = fromBlocks C D A B (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : n
val✝ : l
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inl val✝) = fromBlocks C D A B (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
j : p
val✝¹ : n
val✝ : m
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inr val✝) = fromBlocks C D A B (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : m
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝) (Sum.inr val✝¹) = fromBlocks B A D C (Sum.inl val✝) (Sum.inl val✝¹)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : m
val✝ : o
⊢ fromBlocks A B C D (Sum.inr val✝) (Sum.inr val✝¹) = fromBlocks B A D C (Sum.inr val✝) (Sum.inl val✝¹)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : l
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝) (Sum.inl val✝¹) = fromBlocks B A D C (Sum.inl val✝) (Sum.inr val✝¹)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
val✝¹ : l
val✝ : o
⊢ fromBlocks A B C D (Sum.inr val✝) (Sum.inl val✝¹) = fromBlocks B A D C (Sum.inr val✝) (Sum.inr val✝¹)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : n
val✝ : l
⊢ fromBlocks 0 0 0 0 (Sum.inl val✝¹) (Sum.inl val✝) = 0 (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : n
val✝ : m
⊢ fromBlocks 0 0 0 0 (Sum.inl val✝¹) (Sum.inr val✝) = 0 (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : o
val✝ : l
⊢ fromBlocks 0 0 0 0 (Sum.inr val✝¹) (Sum.inl val✝) = 0 (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Zero α
val✝¹ : o
val✝ : m
⊢ fromBlocks 0 0 0 0 (Sum.inr val✝¹) (Sum.inr val✝) = 0 (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
val✝¹ : n
val✝ : l
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
val✝¹ : n
val✝ : m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inl val✝¹) (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
val✝¹ : o
val✝ : l
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inr val✝¹) (Sum.inl val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inr.inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
val✝¹ : o
val✝ : m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (A + A') (B + B') (C + C') (D + D') (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Add α
v w : m → α
i✝ : m
j✝ : ι
⊢ replicateCol ι (v + w) i✝ j✝ = (replicateCol ι v + replicateCol ι w) i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst✝ : SMul R α
x : R
v : m → α
i✝ : m
j✝ : ι
⊢ replicateCol ι (x • v) i✝ j✝ = (x • replicateCol ι v) i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Add α
v w : m → α
i✝ : ι
j✝ : m
⊢ replicateRow ι (v + w) i✝ j✝ = (replicateRow ι v + replicateRow ι w) i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst✝ : SMul R α
x : R
v : m → α
i✝ : ι
j✝ : m
⊢ replicateRow ι (x • v) i✝ j✝ = (x • replicateRow ι v) i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case neg
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : ¬i✝.2 = j✝.2
⊢ 0 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
v : m → α
i✝ : ι
j✝ : m
⊢ (replicateCol ι v)ᵀ i✝ j✝ = replicateRow ι v i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
v : m → α
i✝ : m
j✝ : ι
⊢ (replicateRow ι v)ᵀ i✝ j✝ = replicateCol ι v i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Star α
v : m → α
i✝ : ι
j✝ : m
⊢ (replicateCol ι v)ᴴ i✝ j✝ = replicateRow ι (star v) i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Star α
v : m → α
i✝ : m
j✝ : ι
⊢ (replicateRow ι v)ᴴ i✝ j✝ = replicateCol ι (star v) i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
i✝ : ι
j✝ : n
⊢ replicateRow ι (v ᵥ* M) i✝ j✝ = (replicateRow ι v * M) i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
i✝ : n
j✝ : ι
⊢ replicateCol ι (v ᵥ* M) i✝ j✝ = (replicateRow ι v * M)ᵀ i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
i✝ : m
j✝ : ι
⊢ replicateCol ι (M *ᵥ v) i✝ j✝ = (M * replicateCol ι v) i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
i✝ : ι
j✝ : m
⊢ replicateRow ι (M *ᵥ v) i✝ j✝ = (M * replicateCol ι v)ᵀ i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
i✝ : n
j✝ : m
⊢ (if i✝ = j then c j✝ else Mᵀ i✝ j✝) = if i✝ = j then c j✝ else M j✝ i✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
i✝ : n
j✝ : m
⊢ (if j✝ = i then b i✝ else Mᵀ i✝ j✝) = if j✝ = i then b i✝ else M j✝ i✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ ((M.map star).updateCol j (star c))ᵀ = ((M.map star).updateCol j (star ∘ c))ᵀ

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
b : n → α
inst✝¹ : DecidableEq m
inst✝ : Star α
⊢ ((M.map star).updateRow i (star b))ᵀ = ((M.map star).updateRow i (star ∘ b))ᵀ

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case pos
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h✝¹ : ji = ii
h✝ : ii = ji
⊢ M ji jx (cast ⋯ ix) = M ii (cast ⋯ jx) ix

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case neg
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h✝¹ : ji = ii
h✝ : ¬ii = ji
⊢ M ji jx (cast ⋯ ix) = 0

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case pos
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h✝¹ : ¬ji = ii
h✝ : ii = ji
⊢ 0 = M ii (cast ⋯ jx) ix

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case neg
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
h✝¹ : ¬ji = ii
h✝ : ¬ii = ji
⊢ 0 = 0

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case refl
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
hij : i ≠ i
⊢ i = i

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
n : ℕ
m' : Type uₘ
A : Matrix m' (Fin n.succ) α
i : Fin n
j : m'
⊢ vecTail (of.symm Aᵀ) i j = (vecTail ∘ A)ᵀ i j

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case refine_1
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ (of (vecCons v A) * B) 0 j = of (vecCons (v ᵥ* B) (of.symm (of A * B))) 0 j

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i : m'
row : Fin m → m'
col : o' → n'
⊢ A.submatrix (vecCons i row) col = vecCons (fun j ↦ A i (col j)) (A.submatrix row col)

Tactic:
by
  ext i j
  refine Fin.cases ?_ ?_ i <;> simp [submatrix]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : Monoid R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : Star A
inst✝² : NonUnitalNonAssocSemiring B
inst✝¹ : DistribMulAction R B
inst✝ : Star B
f : A →⋆ₙₐ[R] B
h₁ : ∀ (m : R) (x : A), f (m • x) = (MonoidHom.id R) m • f x
h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y
h₄ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
      { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
        { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y
h₅ :
  ∀ (a : A),
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun (star a) =
      star ({ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun a)
x✝ : A
⊢ { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄, map_star' := h₅ } x✝ = f x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Star A
inst✝² : Semiring B
inst✝¹ : Algebra R B
inst✝ : Star B
f : A →⋆ₐ[R] B
h₁ : f 1 = 1
h₂ :
  ∀ (x y : A),
    { toFun := ⇑f, map_one' := h₁ }.toFun (x * y) =
      { toFun := ⇑f, map_one' := h₁ }.toFun x * { toFun := ⇑f, map_one' := h₁ }.toFun y
h₃ : (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0
h₄ :
  ∀ (x y : A),
    (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) =
      (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun x +
        (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun y
h₅ :
  ∀ (r : R),
    (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) =
      (algebraMap R B) r
h₆ :
  ∀ (x : A),
    (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                  commutes' := h₅ }.toRingHom).toFun
        (star x) =
      star
        ((↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                    commutes' := h₅ }.toRingHom).toFun
          x)
x✝ : A
⊢ { toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_star' := h₆ }
      x✝ =
    f x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«2»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«2»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «2».«0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «2».«1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «2».«2»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨2, ⋯⟩) ((fun i ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : Monoid R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : DistribMulAction R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction R B
inst✝³ : Star B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R C
inst✝ : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
x✝ : A
⊢ ((fst R B C).comp (f.prod g)) x✝ = f x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «0».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case «1».«1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
rfl

Goal state after: