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) 𝕜
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 ()))
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 ())
⊢ ((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:
simp only [Matrix.mul_assoc, A, List.prod_cons]

Premises used: Matrix.mul_assoc, 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
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 ())
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 ())
⊢ (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
-- 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
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
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) : ℕ)
⊢ 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
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

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
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
⊢ n = (↑(⟨val, isLt⟩ : Fin r) : ℕ)

Tactic:
simp [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
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 : ℕ)

Tactic:
have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp [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
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 : ℕ)
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 ())
⊢ (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 [h, transvection_mul_apply_same, IH, ← hni, add_le_iff_nonpos_right,
          listTransvecCol_mul_last_row_drop _ _ hn]

Premises used: add_le_iff_nonpos_right, Matrix.transvection_mul_apply_same, Matrix.Pivot.listTransvecCol_mul_last_row_drop
-- 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
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 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 [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
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
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
⊢ 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
k 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
n' : Fin r := ⟨(↑(⟨val, isLt⟩ : Fin r) : ℕ), hn⟩
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:
simp [n'] at 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
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 : ℕ)

Tactic:
have hni : n ≠ i := by
        rintro rfl
        cases i
        simp [n'] at 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
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 :
  ((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 ())

Tactic:
simp only [ne_eq, inl.injEq, Ne.symm h, not_false_eq_true, transvection_mul_apply_of_ne]

Premises used: Ne.symm, Sum.inl.injEq, ne_eq, not_false_eq_true, Matrix.transvection_mul_apply_of_ne
-- 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
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 : (if n + 1 ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
⊢ ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())

Tactic:
rw [IH]
-- 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
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 ())
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 ())
⊢ (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)

Premises used: Fin.val, le_or_gt, HAdd.hAdd, OfNat.ofNat
-- 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
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 : 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:
simp only [hi, n.le_succ.trans hi, if_true]

Premises used: if_true, Nat.le_succ, LE.le.trans
-- 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
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 : ℕ)
neg₁ : ¬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:
rw [if_neg, if_neg]

Premises used: if_neg
-- 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
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
⊢ ¬n ≤ (↑i : ℕ)

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

Premises used: not_le, Ne.symm, Iff.mp, Nat.lt_succ_iff_lt_or_eq, or_false
-- 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
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
⊢ ¬n + 1 ≤ (↑i : ℕ)

Tactic:
simpa only [not_le] using hi

Premises used: 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
k : ℕ
self : M (inl i) (inr ()) = if r ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())
⊢ ((List.drop r (listTransvecCol M)).prod * 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]

Premises used: le_refl, List.prod_nil, Matrix.Pivot.length_listTransvecCol, List.drop_eq_nil_of_le, Matrix.one_mul
-- 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
k : ℕ
self : ¬r ≤ (↑i : ℕ)
⊢ M (inl i) (inr ()) = if r ≤ (↑i : ℕ) then 0 else M (inl i) (inr ())

Tactic:
rw [if_neg]

Premises used: if_neg
-- 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
k : ℕ
⊢ ¬r ≤ (↑i : ℕ)

Tactic:
simpa only [not_le] using i.2

Premises used: not_le, Fin.isLt
-- 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
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 ())
self : ((List.drop r (listTransvecCol M)).prod * M) (inl i) (inr ()) = if r ≤ (↑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 ())

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

Premises used: not_le, le_refl, if_true, add_le_iff_nonpos_right, Matrix.mul_assoc, Fin.isLt, Matrix.transvection_mul_apply_same, Sum.inl.injEq, ne_eq, List.prod_nil, Matrix.Pivot.length_listTransvecCol, or_false, not_false_eq_true, List.prod_cons, List.drop_eq_nil_of_le, if_neg, Matrix.transvection_mul_apply_of_ne, Matrix.one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
hk : 0 ≤ r
⊢ (M * (List.take 0 (listTransvecRow M)).prod) i (inr ()) = M i (inr ())

Tactic:
simp only [Matrix.mul_one, List.prod_nil, List.take, Matrix.mul_one]

Premises used: List.prod_nil, Matrix.mul_one, List.take
-- 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
⊢ k < r

Tactic:
have hkr : k < r := hk
-- 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⟩
⊢ 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:
simp only [k', listTransvecRow, hkr, 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) 𝕜
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⟩
⊢ 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]
-- 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 :
  (M * (List.take k (listTransvecRow M)).prod *
        transvection (inr ()) (inl k') (-M (inr ()) (inl k') / M (inr ()) (inr ())))
      i (inr ()) =
    M i (inr ())
⊢ (M * (List.take (k + 1) (listTransvecRow M)).prod) 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]

Premises used: List.prod_append, Matrix.mul_assoc, Option.toList_some, List.prod_nil, Matrix.mul_one, List.take_add_one, List.prod_cons