-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem listTransvecCol_mul_last_row_drop (i : Fin r ⊕ Unit) {k : ℕ} (hk : k ≤ r) :
    (((listTransvecCol M).drop k).prod * M) (inr unit) i = M (inr unit) i

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
⊢ n < (listTransvecCol M).length

Tactic:
simpa [listTransvecCol] using hn

Result:
no goals

Proof state:
case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
⊢ ((List.drop n (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

Tactic:
have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn

Result:
case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
hn' : n < (listTransvecCol M).length
⊢ ((List.drop n (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
hk : k ≤ r
⊢ ((List.drop k (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

Tactic:
induction hk using Nat.decreasingInduction with
| of_succ n hn IH =>
  have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
  rw [List.drop_eq_getElem_cons hn']
  simpa [listTransvecCol, Matrix.mul_assoc]
| self =>
  simp only [length_listTransvecCol, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
    Matrix.one_mul]

Result:
no goals

Proof state:
case self
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
⊢ ((List.drop r (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

Tactic:
simp only [length_listTransvecCol, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
  Matrix.one_mul]

Result:
no goals

Proof state:
case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
hn' : n < (listTransvecCol M).length
⊢ (((listTransvecCol M)[n] :: List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

Tactic:
simpa [listTransvecCol, Matrix.mul_assoc]

Result:
no goals

Proof state:
case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
hn' : n < (listTransvecCol M).length
⊢ ((List.drop n (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

Tactic:
rw [List.drop_eq_getElem_cons hn']

Result:
case of_succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
hn' : n < (listTransvecCol M).length
⊢ (((listTransvecCol M)[n] :: List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i