case left
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
⊢ toBlocks₁₂ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) = 0

case right
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
⊢ toBlocks₂₁ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) = 0
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
⊢ IsTwoBlockDiagonal (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M))
constructor
case left.a.h
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
j : Unit
⊢ toBlocks₁₂ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) i j = OfNat.ofNat 0 i j
case left
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
⊢ toBlocks₁₂ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) = 0
ext (i j)
case left.a.h
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
j : Unit
this : j = ()
⊢ toBlocks₁₂ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) i j = OfNat.ofNat 0 i j
case left.a.h
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
j : Unit
⊢ toBlocks₁₂ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) i j = OfNat.ofNat 0 i j
have : j = unit := by simp only [eq_iff_true_of_subsingleton]
no goals
case left.a.h
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
j : Unit
this : j = ()
⊢ toBlocks₁₂ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) i j = OfNat.ofNat 0 i j
simp [toBlocks₁₂, this, listTransvecCol_mul_mul_listTransvecRow_last_row M hM]
no goals
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
j : Unit
⊢ j = ()
simp only [eq_iff_true_of_subsingleton]
case right.a.h
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Unit
j : Fin r
⊢ toBlocks₂₁ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) i j = OfNat.ofNat 0 i j
case right
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
⊢ toBlocks₂₁ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) = 0
ext (i j)
case right.a.h
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Unit
j : Fin r
this : i = ()
⊢ toBlocks₂₁ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) i j = OfNat.ofNat 0 i j
case right.a.h
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Unit
j : Fin r
⊢ toBlocks₂₁ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) i j = OfNat.ofNat 0 i j
have : i = unit := by simp only [eq_iff_true_of_subsingleton]
no goals
case right.a.h
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Unit
j : Fin r
this : i = ()
⊢ toBlocks₂₁ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) i j = OfNat.ofNat 0 i j
simp [toBlocks₂₁, this, listTransvecCol_mul_mul_listTransvecRow_last_col M hM]
no goals
n : Type ?u.214920
p : Type ?u.214923
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Unit
j : Fin r
⊢ i = ()
simp only [eq_iff_true_of_subsingleton]