-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow
    (hM : M (inr unit) (inr unit) ≠ 0) :
    IsTwoBlockDiagonal ((listTransvecCol M).prod * M * (listTransvecRow M).prod)

Proof state:
𝕜 : 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 [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
case right
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ = 0

Tactic:
ext i j

Result:
case right.a
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Unit
j : Fin r
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ i j = 0 i j

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).IsTwoBlockDiagonal

Tactic:
constructor

Result:
case left
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₁₂ = 0

case right
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ = 0

Proof state:
𝕜 : 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 [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
case right.a
𝕜 : 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]

Result:
no goals

Proof state:
case left.a
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
j : Unit
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₁₂ i j = 0 i j

Tactic:
have : j = unit := by simp only [eq_iff_true_of_subsingleton]

Result:
case left.a
𝕜 : 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

Proof state:
case left
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₁₂ = 0

Tactic:
ext i j

Result:
case left.a
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
j : Unit
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₁₂ i j = 0 i j

Proof state:
case left.a
𝕜 : 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]

Result:
no goals

Proof state:
case right.a
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Unit
j : Fin r
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod).toBlocks₂₁ i j = 0 i j

Tactic:
have : i = unit := by simp only [eq_iff_true_of_subsingleton]

Result:
case right.a
𝕜 : 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