awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin m.succ
⊢ ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) *ᵥ w) i =
    vecCons (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w) i

Tactic:
Fin.cases ?_ ?_ i

Premises used: Fin.cases
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin m.succ
h :
  mulVec (m := Fin m.succ) ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A)) w 0 =
    vecCons (n := m) (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w) 0
h₁ :
  ∀ (i : Fin m),
    ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) *ᵥ w) i.succ =
      vecCons (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w) i.succ
⊢ ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) *ᵥ w) i =
    vecCons (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w) i

Tactic:
refine Fin.cases ?_ ?_ i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin m.succ
⊢ mulVec (m := Fin m.succ) ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A)) w 0 =
    vecCons (n := m) (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w) 0

Tactic:
simp [mulVec]

Premises used: Matrix.mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
inst_1 : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin m.succ
⊢ ∀ (i : Fin m),
    ((of : (a : Fin m.succ → n' → α) → Matrix (Fin m.succ) n' α) (vecCons v A) *ᵥ w) i.succ =
      vecCons (v ⬝ᵥ w) ((of : (a : Fin m → n' → α) → Matrix (Fin m) n' α) A *ᵥ w) i.succ

Tactic:
simp [mulVec]

Premises used: Matrix.mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
n : ℕ
m' : Type uₘ
α : Type u_1
inst : NonUnitalCommSemiring α
A : m' → Fin n.succ → α
x : α
v : Fin n → α
h :
  ∀ (i : m'),
    ((of : (a : m' → Fin n.succ → α) → Matrix m' (Fin n.succ) α) A *ᵥ vecCons x v) i =
      HAdd.hAdd (β := m' → α) (x • vecHead ∘ A) ((of : (a : m' → Fin n → α) → Matrix m' (Fin n) α) (vecTail ∘ A) *ᵥ v) i
⊢ (of : (a : m' → Fin n.succ → α) → Matrix m' (Fin n.succ) α) A *ᵥ vecCons x v =
    x • vecHead ∘ A + (of : (a : m' → Fin n → α) → Matrix m' (Fin n) α) (vecTail ∘ A) *ᵥ v

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
n : ℕ
m' : Type uₘ
α : Type u_1
inst : NonUnitalCommSemiring α
A : m' → Fin n.succ → α
x : α
v : Fin n → α
i : m'
⊢ ((of : (a : m' → Fin n.succ → α) → Matrix m' (Fin n.succ) α) A *ᵥ vecCons x v) i =
    HAdd.hAdd (β := m' → α) (x • vecHead ∘ A) ((of : (a : m' → Fin n → α) → Matrix m' (Fin n) α) (vecTail ∘ A) *ᵥ v) i

Tactic:
simp [mulVec, mul_comm]

Premises used: mul_comm, Matrix.mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
v : Fin 0 → α
w : n' → α
⊢ vecMulVec v w = ![]

Tactic:
empty_eq _

Premises used: Matrix, Matrix.empty_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m' : Type uₘ
inst : NonUnitalNonAssocSemiring α
v : m' → α
w : Fin 0 → α
⊢ vecMulVec v w = (of : (a : m' → Fin 0 → α) → Matrix m' (Fin 0) α) fun (x : m') ↦ ![]

Tactic:
funext fun _ => empty_eq _

Premises used: Matrix, funext, Matrix.empty_eq, Matrix.vecMulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
a : ∀ (i : Fin m.succ) (j : n'), vecMulVec (vecCons x v) w i j = vecCons (x • w) (vecMulVec v w) i j
⊢ vecMulVec (vecCons x v) w = vecCons (x • w) (vecMulVec v w)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j : n'
⊢ vecMulVec (vecCons x v) w i j = vecCons (x • w) (vecMulVec v w) i j

Tactic:
Fin.cases ?_ ?_ i

Premises used: Fin.cases
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j : n'
a : vecMulVec (vecCons x v) w 0 j = vecCons (x • w) (vecMulVec v w) 0 j
a₁ : ∀ (i : Fin m), vecMulVec (vecCons x v) w i.succ j = vecCons (x • w) (vecMulVec v w) i.succ j
⊢ vecMulVec (vecCons x v) w i j = vecCons (x • w) (vecMulVec v w) i j

Tactic:
refine Fin.cases ?_ ?_ i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j : n'
⊢ vecMulVec (vecCons x v) w 0 j = vecCons (x • w) (vecMulVec v w) 0 j

Tactic:
simp [vecMulVec]

Premises used: Matrix.vecMulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
inst : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j : n'
⊢ ∀ (i : Fin m), vecMulVec (vecCons x v) w i.succ j = vecCons (x • w) (vecMulVec v w) i.succ j

Tactic:
simp [vecMulVec]

Premises used: Matrix.vecMulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n : ℕ
m' : Type uₘ
inst : NonUnitalNonAssocSemiring α
v : m' → α
x : α
w : Fin n → α
⊢ vecMulVec v (vecCons x w) =
    (of : (a : m' → Fin n.succ → α) → Matrix m' (Fin n.succ) α) fun (i : m') ↦ v i • vecCons x w

Tactic:
rfl

Premises used: rfl, Matrix.vecMulVec
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : NonUnitalNonAssocSemiring α
m' : Type u_1
x : α
A : Fin 0 → m' → α
⊢ x • A = ![]

Tactic:
empty_eq _

Premises used: Matrix.empty_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
row : Fin 0 → m'
col : o' → n'
⊢ A.submatrix row col = ![]

Tactic:
empty_eq _

Premises used: Matrix, Matrix.empty_eq
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : 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 :
  ∀ (i_1 : Fin m.succ) (j : o'),
    A.submatrix (vecCons i row) col i_1 j = vecCons (fun (j : o') ↦ A i (col j)) (A.submatrix row col) i_1 j
⊢ A.submatrix (vecCons i row) col = vecCons (fun (j : o') ↦ A i (col j)) (A.submatrix row col)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i_1 : m'
row : Fin m → m'
col : o' → n'
i : Fin m.succ
j : o'
⊢ A.submatrix (vecCons i_1 row) col i j = vecCons (fun (j : o') ↦ A i_1 (col j)) (A.submatrix row col) i j

Tactic:
Fin.cases ?_ ?_ i

Premises used: Fin.cases
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i_1 : m'
row : Fin m → m'
col : o' → n'
i : Fin m.succ
j : o'
a : A.submatrix (vecCons i_1 row) col 0 j = vecCons (fun (j : o') ↦ A i_1 (col j)) (A.submatrix row col) 0 j
a₁ :
  ∀ (i : Fin m),
    A.submatrix (vecCons i_1 row) col i.succ j = vecCons (fun (j : o') ↦ A i_1 (col j)) (A.submatrix row col) i.succ j
⊢ A.submatrix (vecCons i_1 row) col i j = vecCons (fun (j : o') ↦ A i_1 (col j)) (A.submatrix row col) i j

Tactic:
refine Fin.cases ?_ ?_ i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i_1 : m'
row : Fin m → m'
col : o' → n'
i : Fin m.succ
j : o'
⊢ A.submatrix (vecCons i_1 row) col 0 j = vecCons (fun (j : o') ↦ A i_1 (col j)) (A.submatrix row col) 0 j

Tactic:
simp [submatrix]

Premises used: Matrix.submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i_1 : m'
row : Fin m → m'
col : o' → n'
i : Fin m.succ
j : o'
⊢ ∀ (i : Fin m),
    A.submatrix (vecCons i_1 row) col i.succ j = vecCons (fun (j : o') ↦ A i_1 (col j)) (A.submatrix row col) i.succ j

Tactic:
simp [submatrix]

Premises used: Matrix.submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
A : Matrix (Fin m.succ) n' α
v : n' → α
f : o' → n'
i : Fin m.succ
⊢ (A.updateRow i v).submatrix i.succAbove f = A.submatrix i.succAbove f

Tactic:
ext fun r s => (congr_fun (updateRow_ne (Fin.succAbove_ne i r) : _ = A _) (f s) :)

Premises used: Fin.succAbove_ne, Matrix.updateRow_ne, congr_fun, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
n : ℕ
m' : Type uₘ
o' : Type uₒ
A : Matrix m' (Fin n.succ) α
v : m' → α
f : o' → m'
i : Fin n.succ
⊢ (A.updateCol i v).submatrix f i.succAbove = A.submatrix f i.succAbove

Tactic:
ext fun _r s => updateCol_ne (Fin.succAbove_ne i s)

Premises used: Fin.succAbove_ne, Matrix.updateCol_ne, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
a : ∀ (i j : Fin 2), Eq.{u + 1} (α := α) (1 i j : α) (!![1, 0; 0, 1] i j : α)
⊢ Eq.{u + 1} (α := Matrix (Fin 2) (Fin 2) α) (1 : Matrix (Fin 2) (Fin 2) α) (!![1, 0; 0, 1] : Matrix (Fin 2) (Fin 2) α)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
i j : Fin 2
a : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : α) (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : α)
a₁ : Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : α) (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : α)
⊢ Eq.{u + 1} (α := α) (1 i j : α) (!![1, 0; 0, 1] i j : α)

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
j : Fin 2
a :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
    (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
a₁ :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)
    (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : α) (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : α)

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
j : Fin 2
a :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
    (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
a₁ :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)
    (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : α) (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : α)

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
    (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)
    (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
    (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)
    (!![1, 0; 0, 1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
a : ∀ (i j : Fin 3), Eq.{u + 1} (α := α) (1 i j : α) (!![1, 0, 0; 0, 1, 0; 0, 0, 1] i j : α)
⊢ Eq.{u + 1} (α := Matrix (Fin 3) (Fin 3) α) (1 : Matrix (Fin 3) (Fin 3) α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] : Matrix (Fin 3) (Fin 3) α)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
i j : Fin 3
a :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
a₁ :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j : α)
a₂ :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) j : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) j : α)
⊢ Eq.{u + 1} (α := α) (1 i j : α) (!![1, 0, 0; 0, 1, 0; 0, 0, 1] i j : α)

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
j : Fin 3
a :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
a₁ :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
a₂ :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
j : Fin 3
a :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
a₁ :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
a₂ :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j : α)

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
j : Fin 3
a :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
a₁ :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
a₂ :
  Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) j : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) j : α)

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : Zero α
inst_1 : One α
⊢ Eq.{u + 1} (α := α) (1 ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)
    (!![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
a :
  ∀ (i j : Fin 2), Eq.{u + 1} (α := α) ((↑n : Matrix (Fin 2) (Fin 2) α) i j : α) (!![(↑n : α), 0; 0, (↑n : α)] i j : α)
⊢ Eq.{u + 1} (α := Matrix (Fin 2) (Fin 2) α) ((↑n : Matrix (Fin 2) (Fin 2) α) : Matrix (Fin 2) (Fin 2) α)
    (!![(↑n : α), 0; 0, (↑n : α)] : Matrix (Fin 2) (Fin 2) α)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
i j : Fin 2
a :
  Eq.{u + 1} (α := α) ((↑n : Matrix (Fin 2) (Fin 2) α) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : α)
    (!![(↑n : α), 0; 0, (↑n : α)] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : α)
a₁ :
  Eq.{u + 1} (α := α) ((↑n : Matrix (Fin 2) (Fin 2) α) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : α)
    (!![(↑n : α), 0; 0, (↑n : α)] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : α)
⊢ Eq.{u + 1} (α := α) ((↑n : Matrix (Fin 2) (Fin 2) α) i j : α) (!![(↑n : α), 0; 0, (↑n : α)] i j : α)

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
j : Fin 2
a :
  Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 2) (Fin 2) α) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
    (!![(↑n : α), 0; 0, (↑n : α)] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
a₁ :
  Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 2) (Fin 2) α) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)
    (!![(↑n : α), 0; 0, (↑n : α)] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)
⊢ Eq.{u + 1} (α := α) ((↑n : Matrix (Fin 2) (Fin 2) α) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : α)
    (!![(↑n : α), 0; 0, (↑n : α)] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : α)

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
j : Fin 2
a :
  Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 2) (Fin 2) α) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
    (!![(↑n : α), 0; 0, (↑n : α)] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
a₁ :
  Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 2) (Fin 2) α) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)
    (!![(↑n : α), 0; 0, (↑n : α)] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)
⊢ Eq.{u + 1} (α := α) ((↑n : Matrix (Fin 2) (Fin 2) α) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : α)
    (!![(↑n : α), 0; 0, (↑n : α)] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : α)

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 2) (Fin 2) α) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
    (!![(↑n : α), 0; 0, (↑n : α)] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 2) (Fin 2) α) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)
    (!![(↑n : α), 0; 0, (↑n : α)] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 2) (Fin 2) α) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)
    (!![(↑n : α), 0; 0, (↑n : α)] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := α)
    ((↑n : Matrix (Fin 2) (Fin 2) α) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)
    (!![(↑n : α), 0; 0, (↑n : α)] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
a :
  ∀ (i j : Fin 3),
    Eq.{u + 1} (α := α) ((↑n : Matrix (Fin 3) (Fin 3) α) i j : α)
      (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] i j : α)
⊢ Eq.{u + 1} (α := Matrix (Fin 3) (Fin 3) α) ((↑n : Matrix (Fin 3) (Fin 3) α) : Matrix (Fin 3) (Fin 3) α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] : Matrix (Fin 3) (Fin 3) α)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Notation
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
i j : Fin 3
a :
  Eq.{u + 1} (α := α) ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨0, ⋯⟩) j : α)
a₁ :
  Eq.{u + 1} (α := α) ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨1, ⋯⟩) j : α)
a₂ :
  Eq.{u + 1} (α := α) ((↑n : Matrix (Fin 3) (Fin 3) α) ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) j : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] ((fun (i : Fin 3) ↦ i) ⟨2, ⋯⟩) j : α)
⊢ Eq.{u + 1} (α := α) ((↑n : Matrix (Fin 3) (Fin 3) α) i j : α)
    (!![(↑n : α), 0, 0; 0, (↑n : α), 0; 0, 0, (↑n : α)] i j : α)

Tactic:
fin_cases i