awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : (e : (a : n) → p) t_i = a
hb : ¬(e : (a : n) → p) t_j = b
pos :
  ∀ (hab : a = b),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
have neg : ∀ (hab : ¬a = b),
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : ¬(e : (a : n) → p) t_i = a
hb : (e : (a : n) → p) t_j = b
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
have pos : ∀ (hab : a = b),
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : ¬(e : (a : n) → p) t_i = a
hb : (e : (a : n) → p) t_j = b
pos :
  ∀ (hab : a = b),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
have neg : ∀ (hab : ¬a = b),
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : ¬(e : (a : n) → p) t_i = a
hb : ¬(e : (a : n) → p) t_j = b
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
have pos : ∀ (hab : a = b),
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t_i t_j : n
hij : t_i ≠ t_j
c : R
a b : p
ha : ¬(e : (a : n) → p) t_i = a
hb : ¬(e : (a : n) → p) t_j = b
pos :
  ∀ (hab : a = b),
    HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
        (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
      HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
⊢ HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
have neg : ∀ (hab : ¬a = b),
  HAdd.hAdd (α := Matrix p p R) (β := Matrix p p R) 1
      (single ((e : (a : n) → p) t_i) ((e : (a : n) → p) t_j) c : Matrix p p R) a b =
    HAdd.hAdd (α := Matrix n n R) 1 (single t_i t_j c) ((e.symm : (a : p) → n) a) ((e.symm : (a : p) → n) b)
Tactic: by_cases hab : a = b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH :
  (List.map (toMatrix ∘ reindexEquiv e) L).prod =
    (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) (List.map toMatrix L).prod
⊢ (List.map (toMatrix ∘ reindexEquiv e) (t :: L)).prod =
    (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) (List.map toMatrix (t :: L)).prod
have cons : HMul.hMul (α := Matrix p p R) (β := Matrix p p R)
    ((reindex e e : (a : Matrix n n R) → Matrix p p R) t.toMatrix : Matrix p p R)
    ((reindex e e : (a : Matrix n n R) → Matrix p p R) (List.map toMatrix L).prod : Matrix p p R) =
  (reindex e e : (a : Matrix n n R) → Matrix p p R) (t.toMatrix * (List.map toMatrix L).prod)
Tactic: simp only [toMatrix_reindexEquiv, IH, Function.comp_apply, List.prod_cons,
      reindexAlgEquiv_apply, List.map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
L : List (TransvectionStruct n R)
⊢ (List.map (toMatrix ∘ reindexEquiv e) L).prod =
    (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) (List.map toMatrix L).prod
have nil : Eq (α := Matrix p p R) (List.prod (List.map (toMatrix ∘ reindexEquiv e) []))
  ((reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) (List.prod (List.map toMatrix [])))
Tactic: induction L with
  | nil => simp
  | cons t L IH =>
    simp only [toMatrix_reindexEquiv, IH, Function.comp_apply, List.prod_cons,
      reindexAlgEquiv_apply, List.map]
    exact (reindexAlgEquiv_mul R _ _ _ _).symm
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Transvection (goal)
Goal:
n : Type u_1
p : Type u_2
R : Type u₂
inst : DecidableEq n
inst_1 : DecidableEq p
inst_2 : CommRing R
inst_3 : Fintype n
inst_4 : Fintype p
e : n ≃ p
L : List (TransvectionStruct n R)
nil :
  Eq (α := Matrix p p R) (List.prod (List.map (toMatrix ∘ reindexEquiv e) []))
    ((reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) (List.prod (List.map toMatrix [])))
⊢ (List.map (toMatrix ∘ reindexEquiv e) L).prod =
    (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) (List.map toMatrix L).prod
have cons : ∀ (t : TransvectionStruct n R) (L : List (TransvectionStruct n R))
  (IH :
    (List.map (toMatrix ∘ reindexEquiv e) L).prod =
      (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) (List.map toMatrix L).prod),
  (List.map (toMatrix ∘ reindexEquiv e) (t :: L)).prod =
    (reindexAlgEquiv R R e : (a : Matrix n n R) → Matrix p p R) (List.map toMatrix (t :: L)).prod
Tactic: induction L with
  | nil => simp
  | cons t L IH =>
    simp only [toMatrix_reindexEquiv, IH, Function.comp_apply, List.prod_cons,
      reindexAlgEquiv_apply, List.map]
    exact (reindexAlgEquiv_mul R _ _ _ _).symm
Cleared hypotheses: L
-- 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 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
have hn' : n < (listTransvecCol M).length
Tactic: have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
-- 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 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
have of_succ : ((getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
            (listTransvecCol M) n hn' ::
          List.drop (n + 1) (listTransvecCol M)).prod *
      M)
    (inr ()) i =
  M (inr ()) i
Tactic: rw [List.drop_eq_getElem_cons hn']
-- 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
⊢ ((List.drop k (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
have of_succ : ∀ (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: 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]
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) 𝕜
i : Fin r ⊕ Unit
k : ℕ
hk : k ≤ r
of_succ :
  ∀ (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
⊢ ((List.drop k (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
have self : ((List.drop r (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]
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
⊢ ((listTransvecCol M).prod * M) (inl i) (inr ()) = 0
have suffices : ∀ k ≤ r, ((List.drop k (listTransvecCol M)).prod * M) (inl i) (inr ()) = if k ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
Tactic: suffices H :
    ∀ k : ℕ,
      k ≤ r →
        (((listTransvecCol M).drop k).prod * M) (inl i) (inr unit) =
          if k ≤ i then 0 else M (inl i) (inr unit) by
    simpa [List.drop] using H 0
-- 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 ())
⊢ ((List.drop n (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have hn' : n < (listTransvecCol M).length
Tactic: have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
-- 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⟩
⊢ ((List.drop n (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have of_succ : ((getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
            (listTransvecCol M) n hn' ::
          List.drop (n + 1) (listTransvecCol M)).prod *
      M)
    (inl i) (inr ()) =
  if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
Tactic: rw [List.drop_eq_getElem_cons hn']
-- 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⟩
⊢ ((getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
              (listTransvecCol M) n hn' ::
            List.drop (n + 1) (listTransvecCol M)).prod *
        M)
      (inl i) (inr ()) =
    if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have 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 ()))
Tactic: have A :
      (listTransvecCol M)[n] =
        transvection (inl n') (inr unit) (-M (inl n') (inr unit) / M (inr unit) (inr unit)) := by
      simp [n', listTransvecCol]
-- 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 ()))
⊢ ((getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
              (listTransvecCol M) n hn' ::
            List.drop (n + 1) (listTransvecCol M)).prod *
        M)
      (inl i) (inr ()) =
    if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
have of_succ : (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 ())
Tactic: simp only [Matrix.mul_assoc, A, List.prod_cons]
-- 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 ()))
⊢ (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 pos : ∀ (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 ())
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
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 ()))
pos :
  ∀ (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 ())
⊢ (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 : ∀ (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 ())
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
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
⊢ n = (↑i : ℕ)
have mk : ∀ (val : ℕ) (isLt : val < r)
  (IH :
    ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl (⟨val, isLt⟩ : Fin r)) (inr ()) =
      if n + 1 ≤ (↑(⟨val, isLt⟩ : Fin r) : ℕ) then 0 else M (inl ⟨val, isLt⟩) (inr ()))
  (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
k n : ℕ
hn : n < r
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 ()))
val : ℕ
isLt : val < r
IH :
  ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl (⟨val, isLt⟩ : Fin r)) (inr ()) =
    if n + 1 ≤ (↑(⟨val, isLt⟩ : Fin r) : ℕ) then 0 else M (inl ⟨val, isLt⟩) (inr ())
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
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
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp [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 pos : (if LE.le (α := ℕ) 1 0 then 0 else M (inl i) (inr ())) +
    -M (inl i) (inr ()) / M (inr ()) (inr ()) * M (inr ()) (inr ()) =
  if n ≤ n then 0 else M (inl i) (inr ())
Tactic: simp only [h, transvection_mul_apply_same, IH, ← hni, add_le_iff_nonpos_right,
          listTransvecCol_mul_last_row_drop _ _ hn]
-- 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 : ℕ
hn : (↑i : ℕ) < r
IH :
  ((List.drop ((↑i : ℕ) + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) =
    if (↑i : ℕ) + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
hn' : (↑i : ℕ) < (listTransvecCol M).length
n' : Fin r := ⟨(↑i : ℕ), hn⟩
A :
  getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecCol M) (↑i : ℕ) hn' =
    transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
⊢ False
have mk : ∀ (val : ℕ) (isLt : val < r) (hn : (↑(⟨val, isLt⟩ : Fin r) : ℕ) < r)
  (IH :
    ((List.drop ((↑(⟨val, isLt⟩ : Fin r) : ℕ) + 1) (listTransvecCol M)).prod * M) (inl (⟨val, isLt⟩ : Fin r)) (inr ()) =
      if (↑(⟨val, isLt⟩ : Fin r) : ℕ) + 1 ≤ (↑(⟨val, isLt⟩ : Fin r) : ℕ) then 0 else M (inl ⟨val, isLt⟩) (inr ()))
  (hn' : (↑(⟨val, isLt⟩ : Fin r) : ℕ) < (listTransvecCol M).length),
  let n' := (⟨(↑(⟨val, isLt⟩ : Fin r) : ℕ), hn⟩ : Fin r);
  ∀
    (A :
      getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
          (listTransvecCol M) (↑(⟨val, isLt⟩ : Fin r) : ℕ) hn' =
        transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ())))
    (h : ¬n' = ⟨val, isLt⟩), False
Tactic: cases i
Cleared hypotheses: i, hn, IH, hn', n', A, h