awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 ())))
succ : inr () ≠ inl k'
⊢ (M * (List.take k (listTransvecRow M)).prod *
        transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
      i (inr ()) =
    M i (inr ())

Tactic:
rw [mul_transvection_apply_of_ne, IH hkr.le]

Premises used: LT.lt.le, Matrix.mul_transvection_apply_of_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 ())))
⊢ inr () ≠ inl k'

Tactic:
simp only [Ne, not_false_iff, reduceCtorEq]

Premises used: reduceCtorEq, Ne, not_false_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 ())
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 ())
⊢ (M * (List.take k (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]

Premises used: reduceCtorEq, List.prod_append, Matrix.mul_assoc, Ne, Option.toList_some, List.prod_nil, Matrix.mul_one, Matrix.mul_transvection_apply_of_ne, List.take_add_one, not_false_iff, List.prod_cons, List.take, Matrix.zero
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
⊢ (listTransvecRow M).length = r

Tactic:
simp [listTransvecRow]

Premises used: Matrix.Pivot.listTransvecRow
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
⊢ (listTransvecRow M).length = r

Tactic:
have A : (listTransvecRow M).length = r := by simp [listTransvecRow]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
A : (listTransvecRow M).length = r
rw : (M * (List.take r (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
⊢ (M * (listTransvecRow M).prod) i (inr ()) = M i (inr ())

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

Premises used: List.take_length
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 * (List.take r (listTransvecRow M)).prod) i (inr ()) = M i (inr ())

Tactic:
simpa using mul_listTransvecRow_last_col_take M i le_rfl

Premises used: le_rfl, Matrix.Pivot.mul_listTransvecRow_last_col_take
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
⊢ (listTransvecRow M).length = r

Tactic:
simp [listTransvecRow]

Premises used: Matrix.Pivot.listTransvecRow
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
⊢ (listTransvecRow M).length = r

Tactic:
have A : (listTransvecRow M).length = r := by simp [listTransvecRow]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
rw : (M * (List.take r (listTransvecRow M)).prod) (inr ()) (inl i) = 0
⊢ (M * (listTransvecRow M).prod) (inr ()) (inl i) = 0

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

Premises used: List.take_length
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
⊢ ¬r ≤ (↑i : ℕ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
⊢ ¬r ≤ (↑i : ℕ)

Tactic:
have : ¬r ≤ i := by simp
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
this : ¬r ≤ (↑i : ℕ)
⊢ (M * (List.take r (listTransvecRow M)).prod) (inr ()) (inl i) = 0

Tactic:
simpa only [this, ite_eq_right_iff] using H r le_rfl

Premises used: le_rfl, ite_eq_right_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
suffices :
  ∀ 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:
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
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : 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]

Premises used: if_true, List.take_zero, List.prod_nil, zero_le', Matrix.mul_one
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
⊢ n < r

Tactic:
have hnr : n < r := hk
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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⟩
⊢ 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:
simp only [n', listTransvecRow, hnr, dif_pos, List.getElem?_ofFn]

Premises used: Matrix.Pivot.listTransvecRow, dif_pos, List.getElem?_ofFn
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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⟩
⊢ 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]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 ())))
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
⊢ (M * (List.take (n + 1) (listTransvecRow M)).prod) (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]

Premises used: List.prod_append, Matrix.mul_assoc, Option.toList_some, List.prod_nil, Matrix.mul_one, List.take_add_one, List.prod_cons
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
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
⊢ (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
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
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) : ℕ)
⊢ n = (↑i : ℕ)

Tactic:
cases i
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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

Tactic:
simp only [n', Fin.mk_eq_mk] at h

Premises used: Fin.mk_eq_mk
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
⊢ n = (↑(⟨val, isLt⟩ : Fin r) : ℕ)

Tactic:
simp only [h]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 : ℕ)

Tactic:
have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp only [h]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 : ℕ)
⊢ ¬n.succ ≤ (↑i : ℕ)

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

Premises used: not_le, Nat.lt_succ_self
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 : ℕ)
⊢ ¬n.succ ≤ (↑i : ℕ)

Tactic:
have : ¬n.succ ≤ i := by simp only [← hni, n.lt_succ_self, not_le]
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 : ℕ)
pos : M (inr ()) (inl i) + -M (inr ()) (inl i) / M (inr ()) (inr ()) * M (inr ()) (inr ()) = 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

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]

Premises used: if_true, if_false, LT.lt.le, Eq.le, Matrix.Pivot.mul_listTransvecRow_last_col_take, Matrix.mul_transvection_apply_same
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 (inr ()) (inl i) + -M (inr ()) (inl i) / M (inr ()) (inr ()) * M (inr ()) (inr ()) = 0

Tactic:
field
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
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
⊢ False

Tactic:
cases i
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
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
n' : Fin r := ⟨(↑(⟨val, isLt⟩ : Fin r) : ℕ), hnr⟩
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:
tauto
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 : ℕ)

Tactic:
have hni : n ≠ i := by
        rintro rfl
        cases i
        tauto
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 : (if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0) = 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

Tactic:
simp only [IH hnr.le, Ne, mul_transvection_apply_of_ne, Ne.symm h, inl.injEq,
        not_false_eq_true]

Premises used: LT.lt.le, Ne, Ne.symm, Sum.inl.injEq, Matrix.mul_transvection_apply_of_ne, not_false_eq_true