awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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)
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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)
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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)
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
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:
simp [ha, hb, hab, ← e.apply_eq_iff_eq_symm_apply, single]

Premises used: Matrix.single, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
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:
simp [ha, hb, hab, ← e.apply_eq_iff_eq_symm_apply, single]

Premises used: Matrix.single, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
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:
simp [ha, hb, hab, ← e.apply_eq_iff_eq_symm_apply, single]

Premises used: Matrix.single, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
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:
simp [ha, hb, hab, ← e.apply_eq_iff_eq_symm_apply, single]

Premises used: Matrix.single, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
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:
simp [ha, hb, hab, ← e.apply_eq_iff_eq_symm_apply, single]

Premises used: Matrix.single, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
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:
simp [ha, hb, hab, ← e.apply_eq_iff_eq_symm_apply, single]

Premises used: Matrix.single, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
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:
simp [ha, hb, hab, ← e.apply_eq_iff_eq_symm_apply, single]

Premises used: Matrix.single, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
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:
simp [ha, hb, hab, ← e.apply_eq_iff_eq_symm_apply, single]

Premises used: Matrix.single, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
⊢ 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:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
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)
⊢ (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:
simp only [toMatrix_reindexEquiv, IH, Function.comp_apply, List.prod_cons,
      reindexAlgEquiv_apply, List.map]

Premises used: List.map, Matrix.TransvectionStruct.toMatrix_reindexEquiv, Matrix.reindexAlgEquiv_apply, Function.comp_apply, List.prod_cons
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
⊢ 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:
(reindexAlgEquiv_mul R _ _ _ _).symm

Premises used: Matrix.submatrix, Matrix.TransvectionStruct.toMatrix, Matrix.reindexAlgEquiv_mul, Matrix.transvection, Eq.symm, List.prod
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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
⊢ 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:
exact (reindexAlgEquiv_mul R _ _ _ _).symm

Premises used: Matrix.reindexAlgEquiv_mul, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
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 [])))
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
⊢ (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

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

Premises used: List.map, Matrix.TransvectionStruct.toMatrix_reindexEquiv, Matrix.reindexAlgEquiv_mul, Matrix.reindexAlgEquiv_apply, Function.comp_apply, Eq.symm, List.prod_cons
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
⊢ (listTransvecCol M).length = r

Tactic:
simp [listTransvecCol]

Premises used: Matrix.Pivot.listTransvecCol
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : ℕ
h : i < (listTransvecCol M).length
⊢ getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecCol M) i h =
    transvection (inl ⟨i, ⋯⟩) (inr ()) (-M (inl (⟨i, ⋯⟩ : Fin r)) (inr ()) / M (inr ()) (inr ()))

Tactic:
simp [listTransvecCol]

Premises used: Matrix.Pivot.listTransvecCol
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (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 : ℕ
h : i < (listTransvecRow M).length
⊢ getElem (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecRow M) i h =
    transvection (inr ()) (inl ⟨i, ⋯⟩) (-M (inr ()) (inl (⟨i, ⋯⟩ : Fin r)) / M (inr ()) (inr ()))

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
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
⊢ n < (listTransvecCol M).length

Tactic:
simpa [listTransvecCol] using hn

Premises used: Matrix.Pivot.listTransvecCol
-- 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 n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
⊢ n < (listTransvecCol M).length

Tactic:
have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
-- 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 n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
hn' : n < (listTransvecCol M).length
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
⊢ ((List.drop n (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

Tactic:
rw [List.drop_eq_getElem_cons hn']

Premises used: List.drop_eq_getElem_cons
-- 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 n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
hn' : n < (listTransvecCol M).length
⊢ ((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:
simpa [listTransvecCol, Matrix.mul_assoc]

Premises used: Matrix.mul_assoc, Matrix.Pivot.listTransvecCol
-- 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 : ℕ
⊢ ((List.drop r (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

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) 𝕜
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
self : ((List.drop r (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
⊢ ((List.drop k (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]

Premises used: le_refl, Matrix.mul_assoc, Matrix.Pivot.listTransvecCol, 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) 𝕜
i : Fin r ⊕ Unit
⊢ ((listTransvecCol M).prod * M) (inr ()) i = M (inr ()) i

Tactic:
simpa using listTransvecCol_mul_last_row_drop M i zero_le

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

Tactic:
simpa [List.drop] using H 0

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

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
-- 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 ())
⊢ n < (listTransvecCol M).length

Tactic:
simpa [listTransvecCol] using hn

Premises used: Matrix.Pivot.listTransvecCol
-- 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 ())
⊢ n < (listTransvecCol M).length

Tactic:
have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
-- 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⟩
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 ())
⊢ ((List.drop n (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']

Premises used: List.drop_eq_getElem_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⟩
⊢ 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:
simp [n', listTransvecCol]

Premises used: Matrix.Pivot.listTransvecCol
-- 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⟩
⊢ 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]