-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem mul_listTransvecRow_last_row (hM : M (inr unit) (inr unit) ≠ 0) (i : Fin r) :
    (M * (listTransvecRow M).prod) (inr unit) (inl i) = 0

Proof state:
case neg
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
⊢ (M * (List.take n (listTransvecRow M)).prod *
        transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
      (inr ()) (inl i) =
    if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
have hni : n ≠ i := by
  rintro rfl
  cases i
  tauto

Result:
case neg
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ ↑i
⊢ (M * (List.take n (listTransvecRow M)).prod *
        transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
      (inr ()) (inl i) =
    if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : n' = i
hni : n = ↑i
⊢ ¬n.succ ≤ ↑i

Tactic:
simp only [← hni, n.lt_succ_self, not_le]

Result:
no goals

Proof state:
case pos
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : n' = i
hni : n = ↑i
this : ¬n.succ ≤ ↑i
⊢ M (inr ()) (inl i) + -M (inr ()) (inl i) / M (inr ()) (inr ()) * M (inr ()) (inr ()) = 0

Tactic:
field_simp [hM]

Result:
no goals

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : n' = i
⊢ n = ↑i

Tactic:
cases i

Result:
case mk
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
n : ℕ
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
val✝ : ℕ
isLt✝ : val✝ < r
IH :
  n ≤ r →
    (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl ⟨val✝, isLt✝⟩) =
      if n ≤ ↑⟨val✝, isLt✝⟩ then M (inr ()) (inl ⟨val✝, isLt✝⟩) else 0
h : n' = ⟨val✝, isLt✝⟩
⊢ n = ↑⟨val✝, isLt✝⟩

Proof state:
case succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
⊢ (M * (List.take (n + 1) (listTransvecRow M)).prod) (inr ()) (inl i) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
have A :
  (listTransvecRow M)[n]? =
    ↑(transvection (inr unit) (inl n')
    (-M (inr unit) (inl n') / M (inr unit) (inr unit))) := by
  simp only [n', listTransvecRow, List.ofFnNthVal, hnr, dif_pos, List.getElem?_ofFn]

Result:
case succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
⊢ (M * (List.take (n + 1) (listTransvecRow M)).prod) (inr ()) (inl i) = if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

Proof state:
case mk
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
val✝ : ℕ
isLt✝ : val✝ < r
IH :
  ↑⟨val✝, isLt✝⟩ ≤ r →
    (M * (List.take (↑⟨val✝, isLt✝⟩) (listTransvecRow M)).prod) (inr ()) (inl ⟨val✝, isLt✝⟩) =
      if ↑⟨val✝, isLt✝⟩ ≤ ↑⟨val✝, isLt✝⟩ then M (inr ()) (inl ⟨val✝, isLt✝⟩) else 0
hk : ↑⟨val✝, isLt✝⟩ + 1 ≤ r
hnr : ↑⟨val✝, isLt✝⟩ < r
n' : Fin r := ⟨↑⟨val✝, isLt✝⟩, hnr⟩
A :
  (listTransvecRow M)[↑⟨val✝, isLt✝⟩]? =
    some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = ⟨val✝, isLt✝⟩
⊢ False

Tactic:
tauto

Result:
no goals

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
H : ∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0
⊢ (M * (listTransvecRow M).prod) (inr ()) (inl i) = 0

Tactic:
have A : (listTransvecRow M).length = r := by simp [listTransvecRow]

Result:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
H : ∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0
A : (listTransvecRow M).length = r
⊢ (M * (listTransvecRow M).prod) (inr ()) (inl i) = 0

Proof state:
case neg.inr.hnc
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ ¬n ≤ ↑i

Tactic:
simpa only [hni.symm, not_le, or_false] using Nat.lt_succ_iff_lt_or_eq.1 hi

Result:
no goals

Proof state:
case zero
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
hk : 0 ≤ r
⊢ (M * (List.take 0 (listTransvecRow M)).prod) (inr ()) (inl i) = if 0 ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
simp only [if_true, Matrix.mul_one, List.take_zero, zero_le', List.prod_nil]

Result:
no goals

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
H : ∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0
A : (listTransvecRow M).length = r
⊢ (M * (listTransvecRow M).prod) (inr ()) (inl i) = 0

Tactic:
rw [← List.take_length (listTransvecRow M), A]

Result:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
H : ∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ ↑i then M (inr ()) (inl i) else 0
A : (listTransvecRow M).length = r
⊢ (M * (List.take r (listTransvecRow M)).prod) (inr ()) (inl i) = 0