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
n : ℕ
IH :
  ∀ (hk : n ≤ r),
    (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A :
  getElem? (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecRow M) n =
    some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
neg :
  ∀ (hi : n + 1 ≤ (↑i : ℕ)),
    (if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0) = if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
neg₁ :
  ∀ (hi : (↑i : ℕ) < n + 1),
    (if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0) = if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
⊢ (if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0) = if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0

Tactic:
rcases le_or_gt (n + 1) i with (hi | hi)

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
n : ℕ
IH :
  ∀ (hk : n ≤ r),
    (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A :
  getElem? (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecRow M) n =
    some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
hi : n + 1 ≤ (↑i : ℕ)
⊢ (if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0) = if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0

Tactic:
simp [hi, n.le_succ.trans hi]

Premises used: 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
n : ℕ
IH :
  ∀ (hk : n ≤ r),
    (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A :
  getElem? (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecRow M) n =
    some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
hi : (↑i : ℕ) < n + 1
neg : ¬n + 1 ≤ (↑i : ℕ)
neg₁ : ¬n ≤ (↑i : ℕ)
⊢ (if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0) = if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0

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
n : ℕ
IH :
  ∀ (hk : n ≤ r),
    (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A :
  getElem? (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecRow M) n =
    some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
hi : (↑i : ℕ) < n + 1
⊢ ¬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
n : ℕ
IH :
  ∀ (hk : n ≤ r),
    (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A :
  getElem? (valid := fun (as : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)) (i : ℕ) ↦ i < as.length)
      (listTransvecRow M) n =
    some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : ¬n' = i
hni : n ≠ (↑i : ℕ)
hi : (↑i : ℕ) < n + 1
⊢ ¬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 : ℕ
hk : k ≤ r
zero :
  ∀ (hk : 0 ≤ r),
    (M * (List.take 0 (listTransvecRow M)).prod) (inr ()) (inl i) = if 0 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
succ :
  ∀ (n : ℕ)
    (IH :
      ∀ (hk : n ≤ r),
        (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0)
    (hk : n + 1 ≤ r),
    (M * (List.take (n + 1) (listTransvecRow M)).prod) (inr ()) (inl i) =
      if n + 1 ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0
⊢ (M * (List.take k (listTransvecRow M)).prod) (inr ()) (inl i) = if k ≤ (↑i : ℕ) then M (inr ()) (inl i) else 0

Tactic:
induction k with
  | zero => simp only [if_true, Matrix.mul_one, List.take_zero, zero_le', List.prod_nil]
  | succ n IH =>
    have hnr : n < r := hk
    let n' : Fin r := ⟨n, hnr⟩
    have A :
      (listTransvecRow M)[n]? =
        ↑(transvection (inr unit) (inl n')
        (-M (inr unit) (inl n') / M (inr unit) (inr unit))) := by
      simp only [n', listTransvecRow, hnr, dif_pos, List.getElem?_ofFn]
    simp only [List.take_add_one, A, ← Matrix.mul_assoc, List.prod_append, Matrix.mul_one,
      List.prod_cons, List.prod_nil, Option.toList_some]
    by_cases h : n' = i
    · have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp only [h]
      have : ¬n.succ ≤ i := by simp only [← hni, n.lt_succ_self, not_le]
      simp only [h, mul_transvection_apply_same, if_false,
        mul_listTransvecRow_last_col_take _ _ hnr.le, hni.le, this, if_true, IH hnr.le]
      field
    · have hni : n ≠ i := by
        rintro rfl
        cases i
        tauto
      simp only [IH hnr.le, Ne, mul_transvection_apply_of_ne, Ne.symm h, inl.injEq,
        not_false_eq_true]
      rcases le_or_gt (n + 1) i with (hi | hi)
      · simp [hi, n.le_succ.trans hi]
      · rw [if_neg, if_neg]
        · simpa only [not_le] using hi
        · simpa only [hni.symm, not_le, or_false] using Nat.lt_succ_iff_lt_or_eq.1 hi

Premises used: not_le, List.prod_append, if_true, Matrix.mul_assoc, if_false, List.take_zero, Ne, Sum.inl.injEq, Option.toList_some, List.prod_nil, zero_le', Matrix.mul_one, or_false, Matrix.mul_transvection_apply_of_ne, List.take_add_one, not_false_eq_true, List.prod_cons, Matrix.zero, if_neg, 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
⊢ listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)

Tactic:
simp [listTransvecRow, listTransvecCol_mul_last_row]

Premises used: Matrix.Pivot.listTransvecRow, Matrix.Pivot.listTransvecCol_mul_last_row
-- 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
⊢ listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)

Tactic:
have : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M) := by
    simp [listTransvecRow, listTransvecCol_mul_last_row]
-- 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
this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
rw : ((listTransvecCol M).prod * M * (listTransvecRow ((listTransvecCol M).prod * M)).prod) (inr ()) (inl i) = 0
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inr ()) (inl i) = 0

Tactic:
rw [this]
-- 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
this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
hM₁ : ((listTransvecCol M).prod * M) (inr ()) (inr ()) ≠ 0
⊢ ((listTransvecCol M).prod * M * (listTransvecRow ((listTransvecCol M).prod * M)).prod) (inr ()) (inl i) = 0

Tactic:
apply mul_listTransvecRow_last_row

Premises used: Matrix.Pivot.mul_listTransvecRow_last_row
-- 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
this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
⊢ ((listTransvecCol M).prod * M) (inr ()) (inr ()) ≠ 0

Tactic:
simpa [listTransvecCol_mul_last_row] using hM

Premises used: Matrix.Pivot.listTransvecCol_mul_last_row
-- 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
⊢ listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)

Tactic:
simp [listTransvecCol, mul_listTransvecRow_last_col]

Premises used: Matrix.Pivot.mul_listTransvecRow_last_col, 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
⊢ listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)

Tactic:
have : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod) := by
    simp [listTransvecCol, mul_listTransvecRow_last_col]
-- 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
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
rw : ((listTransvecCol (M * (listTransvecRow M).prod)).prod * (M * (listTransvecRow M).prod)) (inl i) (inr ()) = 0
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inl i) (inr ()) = 0

Tactic:
rw [this, Matrix.mul_assoc]

Premises used: Matrix.mul_assoc
-- 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
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
hM₁ : (M * (listTransvecRow M).prod) (inr ()) (inr ()) ≠ 0
⊢ ((listTransvecCol (M * (listTransvecRow M).prod)).prod * (M * (listTransvecRow M).prod)) (inl i) (inr ()) = 0

Tactic:
apply listTransvecCol_mul_last_col

Premises used: Matrix.Pivot.listTransvecCol_mul_last_col
-- 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
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
⊢ (M * (listTransvecRow M).prod) (inr ()) (inr ()) ≠ 0

Tactic:
simpa [mul_listTransvecRow_last_col] using hM

Premises used: Matrix.Pivot.mul_listTransvecRow_last_col
-- 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
left : ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₁₂ = 0
right : ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ = 0
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).IsTwoBlockDiagonal

Tactic:
constructor
-- 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
left : ∀ (i : Fin r) (j : Unit), ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₁₂ i j = 0 i j
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₁₂ = 0

Tactic:
ext i j

Premises used: Matrix.TransvectionStruct.i, Matrix.TransvectionStruct.j
-- 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
j : Unit
⊢ j = ()

Tactic:
simp only
-- 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
j : Unit
⊢ j = ()

Tactic:
have : j = unit := by simp only
-- 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
j : Unit
this : j = ()
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₁₂ i j = 0 i j

Tactic:
simp [toBlocks₁₂, this, listTransvecCol_mul_mul_listTransvecRow_last_row M hM]

Premises used: Matrix.toBlocks₁₂, Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_row
-- 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
right : ∀ (i : Unit) (j : Fin r), ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ i j = 0 i j
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ = 0

Tactic:
ext i j

Premises used: Matrix.TransvectionStruct.i, Matrix.TransvectionStruct.j
-- 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 : Unit
j : Fin r
⊢ i = ()

Tactic:
simp only
-- 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 : Unit
j : Fin r
⊢ i = ()

Tactic:
have : i = unit := by simp only
-- 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 : Unit
j : Fin r
this : i = ()
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ i j = 0 i j

Tactic:
simp [toBlocks₂₁, this, listTransvecCol_mul_mul_listTransvecRow_last_col M hM]

Premises used: Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_col, Matrix.toBlocks₂₁
-- 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
⊢ inl i ≠ inr ()

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
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
i : Fin r
⊢ inr () ≠ inl 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
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
⟨L, L', ?_⟩

Premises used: Exists.intro
-- 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
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
refine : ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
refine ⟨L, L', ?_⟩
-- 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
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
⊢ List.map toMatrix L = listTransvecCol M

Tactic:
simp [L, listTransvecCol, Function.comp_def]

Premises used: Function.comp_def, 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
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
⊢ List.map toMatrix L = listTransvecCol M

Tactic:
have A : L.map toMatrix = listTransvecCol M := by simp [L, listTransvecCol, Function.comp_def]
-- 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
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
A : List.map toMatrix L = listTransvecCol M
⊢ List.map toMatrix L' = listTransvecRow M

Tactic:
simp [L', listTransvecRow, Function.comp_def]

Premises used: Matrix.Pivot.listTransvecRow, Function.comp_def
-- 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
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
A : List.map toMatrix L = listTransvecCol M
⊢ List.map toMatrix L' = listTransvecRow M

Tactic:
have B : L'.map toMatrix = listTransvecRow M := by simp [L', listTransvecRow, Function.comp_def]
-- 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
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
A : List.map toMatrix L = listTransvecCol M
B : List.map toMatrix L' = listTransvecRow M
rw : ((listTransvecCol M).prod * M * (listTransvecRow M).prod).IsTwoBlockDiagonal
⊢ ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
rw [A, B]
-- 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
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
A : List.map toMatrix L = listTransvecCol M
B : List.map toMatrix L' = listTransvecRow M
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).IsTwoBlockDiagonal

Tactic:
isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow M hM

Premises used: Matrix.Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_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
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn (n := r) fun (i : Fin r) ↦
    { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
A : List.map toMatrix L = listTransvecCol M
B : List.map toMatrix L' = listTransvecRow M
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).IsTwoBlockDiagonal

Tactic:
exact isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow M hM

Premises used: Matrix.Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
pos :
  ∀ (H : M.IsTwoBlockDiagonal),
    ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
      ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
neg :
  ∀ (H : ¬M.IsTwoBlockDiagonal),
    ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
      ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
by_cases H : IsTwoBlockDiagonal M

Premises used: Matrix.IsTwoBlockDiagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : M.IsTwoBlockDiagonal
⊢ (List.prod (List.map toMatrix []) * M * List.prod (List.map toMatrix [])).IsTwoBlockDiagonal

Tactic:
simpa using H
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : M.IsTwoBlockDiagonal
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
refine ⟨List.nil, List.nil, by simpa using H⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Transvection
Goal:
𝕜 : Type u_3
inst : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬M.IsTwoBlockDiagonal
pos :
  ∀ (hM : M (inr ()) (inr ()) = 0),
    ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
      ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
neg :
  ∀ (hM : ¬M (inr ()) (inr ()) = 0),
    ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
      ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
⊢ ∃ (L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)),
    ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
by_cases hM : M (inr unit) (inr unit) = 0

Premises used: Unit.unit, Sum.inr