[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
B : Fin m → n' → α
i : Fin (Nat.succ m)
j : n'
⊢ vecCons v B i j = vecCons (v j) (fun i => B i j) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
B : Fin m → n' → α
i : Fin (Nat.succ m)
j : n'
⊢ vecCons v B 0 j = vecCons (v j) (fun i => B i j) 0
[PROOFSTEP]
simp
[GOAL]
case refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
B : Fin m → n' → α
i : Fin (Nat.succ m)
j : n'
⊢ ∀ (i : Fin m), vecCons v B (Fin.succ i) j = vecCons (v j) (fun i => B i j) (Fin.succ i)
[PROOFSTEP]
simp
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
B : Fin (Nat.succ m) → n' → α
j : n'
⊢ (vecTail fun i => B i j) = fun i => vecTail B i j
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
B : Fin (Nat.succ m) → n' → α
j : n'
x✝ : Fin m
⊢ vecTail (fun i => B i j) x✝ = vecTail B x✝ j
[PROOFSTEP]
simp [vecTail]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
⊢ vecCons x v ⬝ᵥ w = x * vecHead w + v ⬝ᵥ vecTail w
[PROOFSTEP]
simp [dotProduct, Fin.sum_univ_succ, vecHead, vecTail]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
v : Fin (Nat.succ n) → α
x : α
w : Fin n → α
⊢ v ⬝ᵥ vecCons x w = vecHead v * x + vecTail v ⬝ᵥ w
[PROOFSTEP]
simp [dotProduct, Fin.sum_univ_succ, vecHead, vecTail]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v ⬝ᵥ vecCons y w = x * y + v ⬝ᵥ w
[PROOFSTEP]
simp
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
⊢ col (vecCons x u) = vecCons (fun x_1 => x) (col u)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
i : Fin (Nat.succ m)
j : Unit
⊢ col (vecCons x u) i j = vecCons (fun x_1 => x) (col u) i j
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case a.h.refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
i : Fin (Nat.succ m)
j : Unit
⊢ col (vecCons x u) 0 j = vecCons (fun x_1 => x) (col u) 0 j
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
case a.h.refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
i : Fin (Nat.succ m)
j : Unit
⊢ ∀ (i : Fin m), col (vecCons x u) (Fin.succ i) j = vecCons (fun x_1 => x) (col u) (Fin.succ i) j
[PROOFSTEP]
simp [vecHead, vecTail]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
⊢ row ![] = fun x => ![]
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
i✝ : Unit
x✝ : Fin 0
⊢ row ![] i✝ x✝ = ![]
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
⊢ row (vecCons x u) = fun x_1 => vecCons x u
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
i✝ : Unit
x✝ : Fin (Nat.succ m)
⊢ row (vecCons x u) i✝ x✝ = vecCons x u x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
A : Matrix (Fin m) n' α
⊢ (↑of (vecCons v A))ᵀ = ↑of fun i => vecCons (v i) (Aᵀ i)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin (Nat.succ m)
⊢ (↑of (vecCons v A))ᵀ i j = ↑of (fun i => vecCons (v i) (Aᵀ i)) i j
[PROOFSTEP]
refine' Fin.cases _ _ j
[GOAL]
case a.h.refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin (Nat.succ m)
⊢ (↑of (vecCons v A))ᵀ i 0 = ↑of (fun i => vecCons (v i) (Aᵀ i)) i 0
[PROOFSTEP]
simp
[GOAL]
case a.h.refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin (Nat.succ m)
⊢ ∀ (i_1 : Fin m), (↑of (vecCons v A))ᵀ i (Fin.succ i_1) = ↑of (fun i => vecCons (v i) (Aᵀ i)) i (Fin.succ i_1)
[PROOFSTEP]
simp
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' (Fin (Nat.succ n)) α
⊢ vecTail (↑of.symm Aᵀ) = (vecTail ∘ A)ᵀ
[PROOFSTEP]
ext i j
[GOAL]
case h.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' (Fin (Nat.succ n)) α
i : Fin n
j : m'
⊢ vecTail (↑of.symm Aᵀ) i j = (vecTail ∘ A)ᵀ i j
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
⊢ ↑of (vecCons v A) * B = ↑of (vecCons (vecMul v B) (↑of.symm (↑of A * B)))
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin (Nat.succ m)
j : o'
⊢ (↑of (vecCons v A) * B) i j = ↑of (vecCons (vecMul v B) (↑of.symm (↑of A * B))) i j
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case a.h.refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin (Nat.succ m)
j : o'
⊢ (↑of (vecCons v A) * B) 0 j = ↑of (vecCons (vecMul v B) (↑of.symm (↑of A * B))) 0 j
[PROOFSTEP]
rfl
[GOAL]
case a.h.refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin (Nat.succ m)
j : o'
⊢ ∀ (i : Fin m),
    (↑of (vecCons v A) * B) (Fin.succ i) j = ↑of (vecCons (vecMul v B) (↑of.symm (↑of A * B))) (Fin.succ i) j
[PROOFSTEP]
simp [mul_val_succ]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
B : Fin (Nat.succ n) → o' → α
⊢ vecMul (vecCons x v) (↑of B) = x • vecHead B + vecMul v (↑of (vecTail B))
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
B : Fin (Nat.succ n) → o' → α
i : o'
⊢ vecMul (vecCons x v) (↑of B) i = (x • vecHead B + vecMul v (↑of (vecTail B))) i
[PROOFSTEP]
simp [vecMul]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
v : Fin (Nat.succ n) → α
w : o' → α
B : Fin n → o' → α
⊢ vecMul v (↑of (vecCons w B)) = vecHead v • w + vecMul (vecTail v) (↑of B)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
v : Fin (Nat.succ n) → α
w : o' → α
B : Fin n → o' → α
i : o'
⊢ vecMul v (↑of (vecCons w B)) i = (vecHead v • w + vecMul (vecTail v) (↑of B)) i
[PROOFSTEP]
simp [vecMul]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin n → α
w : o' → α
B : Fin n → o' → α
⊢ vecMul (vecCons x v) (↑of (vecCons w B)) = x • w + vecMul v (↑of B)
[PROOFSTEP]
simp
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
⊢ mulVec (↑of (vecCons v A)) w = vecCons (v ⬝ᵥ w) (mulVec (↑of A) w)
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin (Nat.succ m)
⊢ mulVec (↑of (vecCons v A)) w i = vecCons (v ⬝ᵥ w) (mulVec (↑of A) w) i
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin (Nat.succ m)
⊢ mulVec (↑of (vecCons v A)) w 0 = vecCons (v ⬝ᵥ w) (mulVec (↑of A) w) 0
[PROOFSTEP]
simp [mulVec]
[GOAL]
case h.refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin (Nat.succ m)
⊢ ∀ (i : Fin m), mulVec (↑of (vecCons v A)) w (Fin.succ i) = vecCons (v ⬝ᵥ w) (mulVec (↑of A) w) (Fin.succ i)
[PROOFSTEP]
simp [mulVec]
[GOAL]
α✝ : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α✝
α : Type u_1
inst✝ : CommSemiring α
A : m' → Fin (Nat.succ n) → α
x : α
v : Fin n → α
⊢ mulVec (↑of A) (vecCons x v) = x • vecHead ∘ A + mulVec (↑of (vecTail ∘ A)) v
[PROOFSTEP]
ext i
[GOAL]
case h
α✝ : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : NonUnitalNonAssocSemiring α✝
α : Type u_1
inst✝ : CommSemiring α
A : m' → Fin (Nat.succ n) → α
x : α
v : Fin n → α
i : m'
⊢ mulVec (↑of A) (vecCons x v) i = (x • vecHead ∘ A + mulVec (↑of (vecTail ∘ A)) v) i
[PROOFSTEP]
simp [mulVec, mul_comm]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
⊢ vecMulVec (vecCons x v) w = vecCons (x • w) (vecMulVec v w)
[PROOFSTEP]
ext i
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin (Nat.succ m)
x✝ : n'
⊢ vecMulVec (vecCons x v) w i x✝ = vecCons (x • w) (vecMulVec v w) i x✝
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case a.h.refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin (Nat.succ m)
x✝ : n'
⊢ vecMulVec (vecCons x v) w 0 x✝ = vecCons (x • w) (vecMulVec v w) 0 x✝
[PROOFSTEP]
simp [vecMulVec]
[GOAL]
case a.h.refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin (Nat.succ m)
x✝ : n'
⊢ ∀ (i : Fin m), vecMulVec (vecCons x v) w (Fin.succ i) x✝ = vecCons (x • w) (vecMulVec v w) (Fin.succ i) x✝
[PROOFSTEP]
simp [vecMulVec]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
v : m' → α
x : α
w : Fin n → α
⊢ vecMulVec v (vecCons x w) = fun i => v i • vecCons x w
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
v : m' → α
x : α
w : Fin n → α
i : m'
j : Fin (Nat.succ n)
⊢ vecMulVec v (vecCons x w) i j = (v i • vecCons x w) j
[PROOFSTEP]
rw [vecMulVec_apply, Pi.smul_apply, smul_eq_mul]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : n' → α
A : Fin m → n' → α
⊢ x • vecCons v A = vecCons (x • v) (x • A)
[PROOFSTEP]
ext i
[GOAL]
case h.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : n' → α
A : Fin m → n' → α
i : Fin (Nat.succ m)
x✝ : n'
⊢ (x • vecCons v A) i x✝ = vecCons (x • v) (x • A) i x✝
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case h.h.refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : n' → α
A : Fin m → n' → α
i : Fin (Nat.succ m)
x✝ : n'
⊢ (x • vecCons v A) 0 x✝ = vecCons (x • v) (x • A) 0 x✝
[PROOFSTEP]
simp
[GOAL]
case h.h.refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : n' → α
A : Fin m → n' → α
i : Fin (Nat.succ m)
x✝ : n'
⊢ ∀ (i : Fin m), (x • vecCons v A) (Fin.succ i) x✝ = vecCons (x • v) (x • A) (Fin.succ i) x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' n' α
i : m'
row : Fin m → m'
col : o' → n'
⊢ submatrix A (vecCons i row) col = vecCons (fun j => A i (col j)) (submatrix A row col)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' n' α
i✝ : m'
row : Fin m → m'
col : o' → n'
i : Fin (Nat.succ m)
j : o'
⊢ submatrix A (vecCons i✝ row) col i j = vecCons (fun j => A i✝ (col j)) (submatrix A row col) i j
[PROOFSTEP]
refine' Fin.cases _ _ i
[GOAL]
case a.h.refine'_1
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' n' α
i✝ : m'
row : Fin m → m'
col : o' → n'
i : Fin (Nat.succ m)
j : o'
⊢ submatrix A (vecCons i✝ row) col 0 j = vecCons (fun j => A i✝ (col j)) (submatrix A row col) 0 j
[PROOFSTEP]
simp [submatrix]
[GOAL]
case a.h.refine'_2
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' n' α
i✝ : m'
row : Fin m → m'
col : o' → n'
i : Fin (Nat.succ m)
j : o'
⊢ ∀ (i : Fin m),
    submatrix A (vecCons i✝ row) col (Fin.succ i) j =
      vecCons (fun j => A i✝ (col j)) (submatrix A row col) (Fin.succ i) j
[PROOFSTEP]
simp [submatrix]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 = ↑of ![![1, 0], ![0, 1]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
i j : Fin 2
⊢ OfNat.ofNat 1 i j = ↑of ![![1, 0], ![0, 1]] i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
j : Fin 2
⊢ OfNat.ofNat 1 { val := 0, isLt := (_ : 0 < 2) } j = ↑of ![![1, 0], ![0, 1]] { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
j : Fin 2
⊢ OfNat.ofNat 1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } j =
    ↑of ![![1, 0], ![0, 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![1, 0], ![0, 1]] { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![1, 0], ![0, 1]] { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![1, 0], ![0, 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![1, 0], ![0, 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ 1 = ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
i j : Fin 3
⊢ OfNat.ofNat 1 i j = ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ OfNat.ofNat 1 { val := 0, isLt := (_ : 0 < 3) } j =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 0, isLt := (_ : 0 < 3) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ OfNat.ofNat 1 { val := 1, isLt := (_ : (fun a => a < 3) 1) } j =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 1, isLt := (_ : (fun a => a < 3) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ OfNat.ofNat 1 { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } j =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 0, isLt := (_ : 0 < 3) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 0, isLt := (_ : 0 < 3) } { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 0, isLt := (_ : 0 < 3) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 0, isLt := (_ : 0 < 3) }
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 0, isLt := (_ : 0 < 3) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 0, isLt := (_ : 0 < 3) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 1, isLt := (_ : (fun a => a < 3) 1) }
      { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 1, isLt := (_ : (fun a => a < 3) 1) }
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 1, isLt := (_ : (fun a => a < 3) 1) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 1, isLt := (_ : (fun a => a < 3) 1) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.tail.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Zero α
inst✝ : One α
⊢ OfNat.ofNat 1 { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
⊢ A = ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ A i j = ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ A { val := 0, isLt := (_ : 0 < 2) } j = ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ A { val := 1, isLt := (_ : (fun a => a < 2) 1) } j =
    ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
⊢ A { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
⊢ A { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] { val := 0, isLt := (_ : 0 < 2) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
⊢ A { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 2) (Fin 2) α
⊢ A { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]] { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A = ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ A i j = ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]] i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ A { val := 0, isLt := (_ : 0 < 3) } j =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]] { val := 0, isLt := (_ : 0 < 3) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ A { val := 1, isLt := (_ : (fun a => a < 3) 1) } j =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ A { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } j =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 0, isLt := (_ : 0 < 3) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]] { val := 0, isLt := (_ : 0 < 3) }
      { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 0, isLt := (_ : 0 < 3) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]] { val := 0, isLt := (_ : 0 < 3) }
      { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 0, isLt := (_ : 0 < 3) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]] { val := 0, isLt := (_ : 0 < 3) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
rfl
[GOAL]
case a.h.tail.tail.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix (Fin 3) (Fin 3) α
⊢ A { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ ↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]] =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
i j : Fin 2
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) i j =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]] i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
j : Fin 2
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) { val := 0, isLt := (_ : 0 < 2) } j =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
      { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
j : Fin 2
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) { val := 1, isLt := (_ : (fun a => a < 2) 1) } j =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) { val := 0, isLt := (_ : 0 < 2) }
      { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
      { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ]
[GOAL]
case a.h.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) { val := 0, isLt := (_ : 0 < 2) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
      { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ]
[GOAL]
case a.h.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 0, isLt := (_ : 0 < 2) } =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ]
[GOAL]
case a.h.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ (↑of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * ↑of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) { val := 1, isLt := (_ : (fun a => a < 2) 1) }
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]]
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ ↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
      ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]] =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
i j : Fin 3
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      i j =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      i j
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
j : Fin 3
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 0, isLt := (_ : 0 < 3) } j =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 0, isLt := (_ : 0 < 3) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
j : Fin 3
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } j =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
j : Fin 3
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } j =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 0, isLt := (_ : 0 < 3) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 0, isLt := (_ : 0 < 3) } { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 0, isLt := (_ : 0 < 3) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 0, isLt := (_ : 0 < 3) } { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 0, isLt := (_ : 0 < 3) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 0, isLt := (_ : 0 < 3) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.tail.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 1, isLt := (_ : (fun a => a < 3) 1) } { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.tail.tail.head.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 0, isLt := (_ : 0 < 3) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.tail.tail.head.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 1, isLt := (_ : (fun a => a < 3) 1) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
case a.h.tail.tail.head.tail.tail.head
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α
⊢ (↑of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] *
        ↑of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]])
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } =
    ↑of
      ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃],
        ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃],
        ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
      { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, ← add_assoc]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
a₀ a₁ b₀ b₁ : α
h₀ : a₀ = b₀
h₁ : a₁ = b₁
⊢ ![a₀, a₁] = ![b₀, b₁]
[PROOFSTEP]
subst_vars
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
b₀ b₁ : α
⊢ ![b₀, b₁] = ![b₀, b₁]
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
a₀ a₁ a₂ b₀ b₁ b₂ : α
h₀ : a₀ = b₀
h₁ : a₁ = b₁
h₂ : a₂ = b₂
⊢ ![a₀, a₁, a₂] = ![b₀, b₁, b₂]
[PROOFSTEP]
subst_vars
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
b₀ b₁ b₂ : α
⊢ ![b₀, b₁, b₂] = ![b₀, b₁, b₂]
[PROOFSTEP]
rfl
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : Add α
a₀ a₁ b₀ b₁ : α
⊢ ![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁]
[PROOFSTEP]
rw [cons_add_cons, cons_add_cons, empty_add_empty]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : Add α
a₀ a₁ a₂ b₀ b₁ b₂ : α
⊢ ![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂]
[PROOFSTEP]
rw [cons_add_cons, cons_add_cons, cons_add_cons, empty_add_empty]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
R : Type u_1
inst✝ : SMul R α
x : R
a₀ a₁ : α
⊢ x • ![a₀, a₁] = ![x • a₀, x • a₁]
[PROOFSTEP]
rw [smul_cons, smul_cons, smul_empty]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
R : Type u_1
inst✝ : SMul R α
x : R
a₀ a₁ a₂ : α
⊢ x • ![a₀, a₁, a₂] = ![x • a₀, x • a₁, x • a₂]
[PROOFSTEP]
rw [smul_cons, smul_cons, smul_cons, smul_empty]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₀ a₁ b₀ b₁ : α
⊢ ![a₀, a₁] ⬝ᵥ ![b₀, b₁] = a₀ * b₀ + a₁ * b₁
[PROOFSTEP]
rw [cons_dotProduct_cons, cons_dotProduct_cons, dotProduct_empty, add_zero]
[GOAL]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₀ a₁ a₂ b₀ b₁ b₂ : α
⊢ ![a₀, a₁, a₂] ⬝ᵥ ![b₀, b₁, b₂] = a₀ * b₀ + a₁ * b₁ + a₂ * b₂
[PROOFSTEP]
rw [cons_dotProduct_cons, cons_dotProduct_cons, cons_dotProduct_cons, dotProduct_empty, add_zero, add_assoc]
