awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ())))
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
⊢ (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 neg : ∀ (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
-- 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 ())))
h : n' = i
⊢ n = (↑i : ℕ)
have mk : ∀ (val : ℕ) (isLt : val < r)
  (IH :
    ∀ (hk : n ≤ r),
      (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl (⟨val, isLt⟩ : Fin r)) =
        if n ≤ (↑(⟨val, isLt⟩ : Fin r) : ℕ) then M (inr ()) (inl ⟨val, isLt⟩) else 0)
  (h : n' = ⟨val, isLt⟩), n = (↑(⟨val, isLt⟩ : Fin r) : ℕ)
Tactic: cases i
Cleared hypotheses: i, IH, h
-- 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
n : ℕ
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 ())))
val : ℕ
isLt : val < r
IH :
  ∀ (hk : n ≤ r),
    (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl (⟨val, isLt⟩ : Fin r)) =
      if n ≤ (↑(⟨val, isLt⟩ : Fin r) : ℕ) then M (inr ()) (inl ⟨val, isLt⟩) else 0
h : n' = ⟨val, isLt⟩
⊢ n = (↑(⟨val, isLt⟩ : Fin r) : ℕ)
have h₁ : n = val
Tactic: simp only [n', Fin.mk_eq_mk] at h
Cleared hypotheses: h
-- 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⟩
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 ())))
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
have hni : n = (↑i : ℕ)
Tactic: have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp only [h]
-- 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⟩
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 ())))
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
have this : ¬n.succ ≤ (↑i : ℕ)
Tactic: have : ¬n.succ ≤ i := by simp only [← hni, n.lt_succ_self, not_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) 𝕜
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 ())))
h : n' = i
hni : n = (↑i : ℕ)
this : ¬n.succ ≤ (↑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
have pos : M (inr ()) (inl i) + -M (inr ()) (inl i) / M (inr ()) (inr ()) * M (inr ()) (inr ()) = 0
Tactic: simp only [h, mul_transvection_apply_same, if_false,
        mul_listTransvecRow_last_col_take _ _ hnr.le, hni.le, this, if_true, IH hnr.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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
IH :
  ∀ (hk : (↑i : ℕ) ≤ r),
    (M * (List.take (↑i : ℕ) (listTransvecRow M)).prod) (inr ()) (inl i) =
      if (↑i : ℕ) ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
hk : (↑i : ℕ) + 1 ≤ r
hnr : (↑i : ℕ) < r
n' : Fin r := ⟨(↑i : ℕ), hnr⟩
A :
  getElem? (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecRow M) (↑i : ℕ) =
    some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
⊢ False
have mk : ∀ (val : ℕ) (isLt : val < r)
  (IH :
    ∀ (hk : (↑(⟨val, isLt⟩ : Fin r) : ℕ) ≤ r),
      (M * (List.take (↑(⟨val, isLt⟩ : Fin r) : ℕ) (listTransvecRow M)).prod) (inr ()) (inl (⟨val, isLt⟩ : Fin r)) =
        if (↑(⟨val, isLt⟩ : Fin r) : ℕ) ≤ (↑(⟨val, isLt⟩ : Fin r) : ℕ) then M (inr ()) (inl ⟨val, isLt⟩) else 0)
  (hk : (↑(⟨val, isLt⟩ : Fin r) : ℕ) + 1 ≤ r) (hnr : (↑(⟨val, isLt⟩ : Fin r) : ℕ) < r),
  let n' := (⟨(↑(⟨val, isLt⟩ : Fin r) : ℕ), hnr⟩ : Fin r);
  ∀
    (A :
      getElem? (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
          (listTransvecRow M) (↑(⟨val, isLt⟩ : Fin r) : ℕ) =
        some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ()))))
    (h : ¬n' = ⟨val, isLt⟩), False
Tactic: cases i
Cleared hypotheses: i, IH, hk, hnr, n', A, h
-- 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⟩
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 ())))
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
have hni : n ≠ (↑i : ℕ)
Tactic: have hni : n ≠ i := by
        rintro rfl
        cases i
        tauto
-- 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 ())))
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
have neg : (if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0) = if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
Tactic: simp only [IH hnr.le, Ne, mul_transvection_apply_of_ne, Ne.symm h, inl.injEq,
        not_false_eq_true]
-- 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 ())))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
⊢ (if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0) = if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
have neg : ∀ (hi : n + 1 ≤ (↑i : ℕ)),
  (if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0) = if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
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
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 ())))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
neg :
  ∀ (hi : n + 1 ≤ (↑i : ℕ)),
    (if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0) = if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
⊢ (if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0) = if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
have neg₁ : ∀ (hi : (↑i : ℕ) < n + 1),
  (if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0) = if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
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
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 ())))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
hi : (↑i : ℕ) < n + 1
⊢ (if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0) = if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
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
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 ())))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
hi : (↑i : ℕ) < n + 1
neg : ¬n + 1 ≤ (↑i : ℕ)
⊢ (if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0) = if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
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 : ℕ
hk : k ≤ r
⊢ (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
have zero : ∀ (hk : 0 ≤ r),
  (M * (List.take 0 (listTransvecRow M)).prod) (inr ()) (inl i) = if 0 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
Tactic: induction k with
  | zero => simp only [if_true, Matrix.mul_one, List.take_zero, zero_le', List.prod_nil]
  | succ n IH =>
    have hnr : n < r := hk
    let n' : Fin r := ⟨n, hnr⟩
    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]
    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]
    by_cases h : n' = i
    · have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp only [h]
      have : ¬n.succ ≤ i := by simp only [← hni, n.lt_succ_self, not_le]
      simp only [h, mul_transvection_apply_same, if_false,
        mul_listTransvecRow_last_col_take _ _ hnr.le, hni.le, this, if_true, IH hnr.le]
      field
    · have hni : n ≠ i := by
        rintro rfl
        cases i
        tauto
      simp only [IH hnr.le, Ne, mul_transvection_apply_of_ne, Ne.symm h, inl.injEq,
        not_false_eq_true]
      rcases le_or_gt (n + 1) i with (hi | hi)
      · simp [hi, n.le_succ.trans hi]
      · rw [if_neg, if_neg]
        · simpa only [not_le] using hi
        · simpa only [hni.symm, not_le, or_false] using Nat.lt_succ_iff_lt_or_eq.1 hi
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
hk : k ≤ r
zero :
  ∀ (hk : 0 ≤ r),
    (M * (List.take 0 (listTransvecRow M)).prod) (inr ()) (inl i) = if 0 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
⊢ (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
have succ : ∀ (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
Tactic: induction k with
  | zero => simp only [if_true, Matrix.mul_one, List.take_zero, zero_le', List.prod_nil]
  | succ n IH =>
    have hnr : n < r := hk
    let n' : Fin r := ⟨n, hnr⟩
    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]
    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]
    by_cases h : n' = i
    · have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp only [h]
      have : ¬n.succ ≤ i := by simp only [← hni, n.lt_succ_self, not_le]
      simp only [h, mul_transvection_apply_same, if_false,
        mul_listTransvecRow_last_col_take _ _ hnr.le, hni.le, this, if_true, IH hnr.le]
      field
    · have hni : n ≠ i := by
        rintro rfl
        cases i
        tauto
      simp only [IH hnr.le, Ne, mul_transvection_apply_of_ne, Ne.symm h, inl.injEq,
        not_false_eq_true]
      rcases le_or_gt (n + 1) i with (hi | hi)
      · simp [hi, n.le_succ.trans hi]
      · rw [if_neg, if_neg]
        · simpa only [not_le] using hi
        · simpa only [hni.symm, not_le, or_false] using Nat.lt_succ_iff_lt_or_eq.1 hi
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inr ()) (inl i) = 0
have this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
Tactic: have : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M) := by
    simp [listTransvecRow, listTransvecCol_mul_last_row]
-- 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
this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inr ()) (inl i) = 0
have rw : ((listTransvecCol M).prod * M * (listTransvecRow ((listTransvecCol M).prod * M)).prod) (inr ()) (inl i) = 0
Tactic: rw [this]
-- 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
this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
⊢ ((listTransvecCol M).prod * M * (listTransvecRow ((listTransvecCol M).prod * M)).prod) (inr ()) (inl i) = 0
have hM₁ : ((listTransvecCol M).prod * M) (inr ()) (inr ()) ≠ 0
Tactic: apply mul_listTransvecRow_last_row
-- 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
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inl i) (inr ()) = 0
have this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
Tactic: have : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod) := by
    simp [listTransvecCol, mul_listTransvecRow_last_col]
-- 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
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inl i) (inr ()) = 0
have rw : ((listTransvecCol (M * (listTransvecRow M).prod)).prod * (M * (listTransvecRow M).prod)) (inl i) (inr ()) = 0
Tactic: rw [this, Matrix.mul_assoc]
-- 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
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
⊢ ((listTransvecCol (M * (listTransvecRow M).prod)).prod * (M * (listTransvecRow M).prod)) (inl i) (inr ()) = 0
have hM₁ : (M * (listTransvecRow M).prod) (inr ()) (inr ()) ≠ 0
Tactic: apply listTransvecCol_mul_last_col
-- 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
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).IsTwoBlockDiagonal
have left : ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₁₂ = 0
Tactic: constructor
-- 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
left : ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₁₂ = 0
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).IsTwoBlockDiagonal
have right : ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ = 0
Tactic: constructor
-- 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
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₁₂ = 0
have left : ∀ (i : Fin r) (j : Unit), ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₁₂ i j = 0 i j
Tactic: ext i j
-- 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
j : Unit
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₁₂ i j = 0 i j
have this : j = ()
Tactic: have : j = unit := by simp only
-- 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
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ = 0
have right : ∀ (i : Unit) (j : Fin r), ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ i j = 0 i j
Tactic: ext i j
-- 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 : Unit
j : Fin r
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ i j = 0 i j
have this : i = ()
Tactic: have : i = unit := by simp only
-- 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
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
have refine : ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
Tactic: refine ⟨L, L', ?_⟩