awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH :
  ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
    if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A :
  getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecCol M) n hn' =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
⊢ (transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ())) *
        ((List.drop (n + 1) (listTransvecCol M)).prod * M))
      (inl i) (inr ()) =
    if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have hni : n ≠ (↑i : ℕ)
Tactic: have hni : n ≠ i := by
        rintro rfl
        cases i
        simp [n'] at h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH :
  ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
    if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A :
  getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecCol M) n hn' =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
⊢ (transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ())) *
        ((List.drop (n + 1) (listTransvecCol M)).prod * M))
      (inl i) (inr ()) =
    if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have neg : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
Tactic: simp only [ne_eq, inl.injEq, Ne.symm h, not_false_eq_true, transvection_mul_apply_of_ne]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH :
  ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
    if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A :
  getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecCol M) n hn' =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
⊢ ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have neg : (if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
Tactic: rw [IH]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH :
  ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
    if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A :
  getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecCol M) n hn' =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
⊢ (if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have neg : ∀ (hi : n + 1 ≤ (↑i : ℕ)),
  (if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
Tactic: rcases le_or_gt (n + 1) i with (hi | hi)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH :
  ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
    if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A :
  getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecCol M) n hn' =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
neg :
  ∀ (hi : n + 1 ≤ (↑i : ℕ)),
    (if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
⊢ (if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have neg₁ : ∀ (hi : (↑i : ℕ) < n + 1),
  (if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
Tactic: rcases le_or_gt (n + 1) i with (hi | hi)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH :
  ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
    if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A :
  getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecCol M) n hn' =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
hi : (↑i : ℕ) < n + 1
⊢ (if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have neg : ¬n ≤ (↑i : ℕ)
Tactic: rw [if_neg, if_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH :
  ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
    if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A :
  getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecCol M) n hn' =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
hi : (↑i : ℕ) < n + 1
neg : ¬n ≤ (↑i : ℕ)
⊢ (if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have neg₁ : ¬n + 1 ≤ (↑i : ℕ)
Tactic: rw [if_neg, if_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
⊢ ((List.drop r (listTransvecCol M)).prod * M) (inl i) (inr ()) = if r ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have self : M (inl i) (inr ()) = if r ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
Tactic: simp only [length_listTransvecCol, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
      Matrix.one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
⊢ M (inl i) (inr ()) = if r ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have self : ¬r ≤ (↑i : ℕ)
Tactic: rw [if_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk : k ≤ r
⊢ ((List.drop k (listTransvecCol M)).prod * M) (inl i) (inr ()) = if k ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have of_succ : ∀ (n : ℕ) (hn : n < r)
  (IH :
    ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
      if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())),
  ((List.drop n (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
Tactic: induction hk using Nat.decreasingInduction with
  | of_succ n hn IH =>
    have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
    let n' : Fin r := ⟨n, hn⟩
    rw [List.drop_eq_getElem_cons hn']
    have A :
      (listTransvecCol M)[n] =
        transvection (inl n') (inr unit) (-M (inl n') (inr unit) / M (inr unit) (inr unit)) := by
      simp [n', listTransvecCol]
    simp only [Matrix.mul_assoc, A, List.prod_cons]
    by_cases h : n' = i
    · have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp [h]
      simp only [h, transvection_mul_apply_same, IH, ← hni, add_le_iff_nonpos_right,
          listTransvecCol_mul_last_row_drop _ _ hn]
      simp [field]
    · have hni : n ≠ i := by
        rintro rfl
        cases i
        simp [n'] at h
      simp only [ne_eq, inl.injEq, Ne.symm h, not_false_eq_true, transvection_mul_apply_of_ne]
      rw [IH]
      rcases le_or_gt (n + 1) i with (hi | hi)
      · simp only [hi, n.le_succ.trans hi, if_true]
      · rw [if_neg, if_neg]
        · simpa only [hni.symm, not_le, or_false] using Nat.lt_succ_iff_lt_or_eq.1 hi
        · simpa only [not_le] using hi
  | self =>
    simp only [length_listTransvecCol, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
      Matrix.one_mul]
    rw [if_neg]
    simpa only [not_le] using i.2
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk : k ≤ r
of_succ :
  ∀ (n : ℕ) (hn : n < r)
    (IH :
      ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
        if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())),
    ((List.drop n (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
⊢ ((List.drop k (listTransvecCol M)).prod * M) (inl i) (inr ()) = if k ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have self : ((List.drop r (listTransvecCol M)).prod * M) (inl i) (inr ()) = if r ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
Tactic: induction hk using Nat.decreasingInduction with
  | of_succ n hn IH =>
    have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
    let n' : Fin r := ⟨n, hn⟩
    rw [List.drop_eq_getElem_cons hn']
    have A :
      (listTransvecCol M)[n] =
        transvection (inl n') (inr unit) (-M (inl n') (inr unit) / M (inr unit) (inr unit)) := by
      simp [n', listTransvecCol]
    simp only [Matrix.mul_assoc, A, List.prod_cons]
    by_cases h : n' = i
    · have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp [h]
      simp only [h, transvection_mul_apply_same, IH, ← hni, add_le_iff_nonpos_right,
          listTransvecCol_mul_last_row_drop _ _ hn]
      simp [field]
    · have hni : n ≠ i := by
        rintro rfl
        cases i
        simp [n'] at h
      simp only [ne_eq, inl.injEq, Ne.symm h, not_false_eq_true, transvection_mul_apply_of_ne]
      rw [IH]
      rcases le_or_gt (n + 1) i with (hi | hi)
      · simp only [hi, n.le_succ.trans hi, if_true]
      · rw [if_neg, if_neg]
        · simpa only [hni.symm, not_le, or_false] using Nat.lt_succ_iff_lt_or_eq.1 hi
        · simpa only [not_le] using hi
  | self =>
    simp only [length_listTransvecCol, le_refl, List.drop_eq_nil_of_le, List.prod_nil,
      Matrix.one_mul]
    rw [if_neg]
    simpa only [not_le] using i.2
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
IH : ∀ (hk : k ≤ r), (M * (List.take k (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
hk : k + 1 ≤ r
⊢ (M * (List.take (k + 1) (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
have hkr : k < r
Tactic: have hkr : k < r := hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
IH : ∀ (hk : k ≤ r), (M * (List.take k (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
hk : k + 1 ≤ r
hkr : k < r
k' : Fin r := ⟨k, hkr⟩
⊢ (M * (List.take (k + 1) (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
have this : getElem? (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length) (listTransvecRow M)
    k =
  some (transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
Tactic: have :
      (listTransvecRow M)[k]? =
        ↑(transvection (inr Unit.unit) (inl k')
            (-M (inr Unit.unit) (inl k') / M (inr Unit.unit) (inr Unit.unit))) := by
      simp only [k', listTransvecRow, hkr, dif_pos, List.getElem?_ofFn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
IH : ∀ (hk : k ≤ r), (M * (List.take k (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
hk : k + 1 ≤ r
hkr : k < r
k' : Fin r := ⟨k, hkr⟩
this :
  getElem? (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecRow M) k =
    some (transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
⊢ (M * (List.take (k + 1) (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
have succ : (M * (List.take k (listTransvecRow M)).prod *
      transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
    i (inr ()) =
  M i (inr ())
Tactic: simp only [List.take_add_one, ← Matrix.mul_assoc, this, List.prod_append, Matrix.mul_one,
      List.prod_cons, List.prod_nil, Option.toList_some]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
IH : ∀ (hk : k ≤ r), (M * (List.take k (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
hk : k + 1 ≤ r
hkr : k < r
k' : Fin r := ⟨k, hkr⟩
this :
  getElem? (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecRow M) k =
    some (transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
⊢ (M * (List.take k (listTransvecRow M)).prod *
        transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
      i (inr ()) =
    M i (inr ())
have succ : inr () ≠ inl k'
Tactic: rw [mul_transvection_apply_of_ne, IH hkr.le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
hk : k ≤ r
⊢ (M * (List.take k (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
have zero : ∀ (hk : 0 ≤ r), (M * (List.take 0 (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
Tactic: induction k with
  | zero => simp only [Matrix.mul_one, List.prod_nil, List.take, Matrix.mul_one]
  | succ k IH =>
    have hkr : k < r := hk
    let k' : Fin r := ⟨k, hkr⟩
    have :
      (listTransvecRow M)[k]? =
        ↑(transvection (inr Unit.unit) (inl k')
            (-M (inr Unit.unit) (inl k') / M (inr Unit.unit) (inr Unit.unit))) := by
      simp only [k', listTransvecRow, hkr, dif_pos, List.getElem?_ofFn]
    simp only [List.take_add_one, ← Matrix.mul_assoc, this, List.prod_append, Matrix.mul_one,
      List.prod_cons, List.prod_nil, Option.toList_some]
    rw [mul_transvection_apply_of_ne, IH hkr.le]
    simp only [Ne, not_false_iff, reduceCtorEq]
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
hk : k ≤ r
zero : ∀ (hk : 0 ≤ r), (M * (List.take 0 (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
⊢ (M * (List.take k (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
have succ : ∀ (k : ℕ) (IH : ∀ (hk : k ≤ r), (M * (List.take k (listTransvecRow M)).prod) i (inr ()) = M i (inr ()))
  (hk : k + 1 ≤ r), (M * (List.take (k + 1) (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
Tactic: induction k with
  | zero => simp only [Matrix.mul_one, List.prod_nil, List.take, Matrix.mul_one]
  | succ k IH =>
    have hkr : k < r := hk
    let k' : Fin r := ⟨k, hkr⟩
    have :
      (listTransvecRow M)[k]? =
        ↑(transvection (inr Unit.unit) (inl k')
            (-M (inr Unit.unit) (inl k') / M (inr Unit.unit) (inr Unit.unit))) := by
      simp only [k', listTransvecRow, hkr, dif_pos, List.getElem?_ofFn]
    simp only [List.take_add_one, ← Matrix.mul_assoc, this, List.prod_append, Matrix.mul_one,
      List.prod_cons, List.prod_nil, Option.toList_some]
    rw [mul_transvection_apply_of_ne, IH hkr.le]
    simp only [Ne, not_false_iff, reduceCtorEq]
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
⊢ (M * (listTransvecRow M).prod) i (inr ()) = M i (inr ())
have A : (listTransvecRow M).length = r
Tactic: have A : (listTransvecRow M).length = r := by simp [listTransvecRow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
A : (listTransvecRow M).length = r
⊢ (M * (listTransvecRow M).prod) i (inr ()) = M i (inr ())
have rw : (M * (List.take r (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
Tactic: rw [← List.take_length (l := listTransvecRow M), A]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
Goal:
𝕜 : 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
have A : (listTransvecRow M).length = r
Tactic: have A : (listTransvecRow M).length = r := by simp [listTransvecRow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : 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
have rw : (M * (List.take r (listTransvecRow M)).prod) (inr ()) (inl i) = 0
Tactic: rw [← List.take_length (l := listTransvecRow M), A]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
Goal:
𝕜 : 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
have this : ¬r ≤ (↑i : ℕ)
Tactic: have : ¬r ≤ i := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ (M * (listTransvecRow M).prod) (inr ()) (inl i) = 0
have suffices : ∀ k ≤ r, (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
Tactic: suffices H :
    ∀ k : ℕ,
      k ≤ r →
        (M * ((listTransvecRow M).take k).prod) (inr unit) (inl i) =
          if k ≤ i then M (inr unit) (inl i) else 0 by
    have A : (listTransvecRow M).length = r := by simp [listTransvecRow]
    rw [← List.take_length (l := listTransvecRow M), A]
    have : ¬r ≤ i := by simp
    simpa only [this, ite_eq_right_iff] using H r le_rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH :
  ∀ (hk : 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
⊢ (M * (List.take (n + 1) (listTransvecRow M)).prod) (inr ()) (inl i) =
    if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
have hnr : n < r
Tactic: have hnr : n < r := hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (hypothesis)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH :
  ∀ (hk : 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
have A : getElem? (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length) (listTransvecRow M)
    n =
  some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
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, hnr, dif_pos, List.getElem?_ofFn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH :
  ∀ (hk : 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 :
  getElem? (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (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
have succ : (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: simp only [List.take_add_one, A, ← Matrix.mul_assoc, List.prod_append, Matrix.mul_one,
      List.prod_cons, List.prod_nil, Option.toList_some]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH :
  ∀ (hk : 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 :
  getElem? (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecRow M) n =
    some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
⊢ (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
have pos : ∀ (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: by_cases h : n' = i