case pos
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : IsTwoBlockDiagonal M
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))

case neg
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬IsTwoBlockDiagonal M
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
by_cases H : IsTwoBlockDiagonal M
case pos
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬IsTwoBlockDiagonal M
hM : M (inr ()) (inr ()) ≠ 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))

case neg
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬IsTwoBlockDiagonal M
hM : ¬M (inr ()) (inr ()) ≠ 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
case neg
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬IsTwoBlockDiagonal M
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
by_cases hM : M (inr unit) (inr unit) ≠ 0
case neg
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬IsTwoBlockDiagonal M
hM : M (inr ()) (inr ()) = 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
case neg
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬IsTwoBlockDiagonal M
hM : ¬M (inr ()) (inr ()) ≠ 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
push_neg  at hM
case neg
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
case neg
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬IsTwoBlockDiagonal M
hM : M (inr ()) (inr ()) = 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
simp only [not_and_or, IsTwoBlockDiagonal, toBlocks₁₂, toBlocks₂₁, ← Matrix.ext_iff] at H
case neg.intro.inl
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))

case neg.intro.inr
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
case neg
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
this : ∃ i, M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
rcases this with ⟨i, h | h⟩
no goals
case pos
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : IsTwoBlockDiagonal M
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
refine' ⟨List.nil, List.nil, by simpa using H⟩
no goals
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : IsTwoBlockDiagonal M
⊢ IsTwoBlockDiagonal (List.prod (List.map toMatrix []) ⬝ M ⬝ List.prod (List.map toMatrix []))
simpa using H
no goals
case pos
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : ¬IsTwoBlockDiagonal M
hM : M (inr ()) (inr ()) ≠ 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
exact exists_isTwoBlockDiagonal_of_ne_zero M hM
case inl
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j
⊢ ∃ i, M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0

case inr
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
⊢ ∃ i, M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
⊢ ∃ i, M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0
cases' H with H H
case inl
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ∀ (i : Fin r), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0
⊢ ∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j
case inl
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j
⊢ ∃ i, M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0
contrapose! H
case inl.unit
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ∀ (i : Fin r), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0
i : Fin r
⊢ ↑of (fun i j => M (inl i) (inr j)) i PUnit.unit = OfNat.ofNat 0 i PUnit.unit
case inl
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ∀ (i : Fin r), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0
⊢ ∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j
rintro i ⟨⟩
no goals
case inl.unit
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ∀ (i : Fin r), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0
i : Fin r
⊢ ↑of (fun i j => M (inl i) (inr j)) i PUnit.unit = OfNat.ofNat 0 i PUnit.unit
exact (H i).1
case inr
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ∀ (i : Fin r), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0
⊢ ∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
case inr
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
⊢ ∃ i, M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0
contrapose! H
case inr.unit
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ∀ (i : Fin r), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0
j : Fin r
⊢ ↑of (fun i j => M (inr i) (inl j)) PUnit.unit j = OfNat.ofNat 0 PUnit.unit j
case inr
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ∀ (i : Fin r), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0
⊢ ∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
rintro ⟨⟩ j
no goals
case inr.unit
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ∀ (i : Fin r), M (inl i) (inr ()) = 0 ∧ M (inr ()) (inl i) = 0
j : Fin r
⊢ ↑of (fun i j => M (inr i) (inl j)) PUnit.unit j = OfNat.ofNat 0 PUnit.unit j
exact (H j).2
case neg.intro.inl
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 ⬝ M
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
case neg.intro.inl
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
let M' := transvection (inr Unit.unit) (inl i) 1 ⬝ M
case neg.intro.inl
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 ⬝ M
hM' : M' (inr ()) (inr ()) ≠ 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
case neg.intro.inl
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 ⬝ M
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
have hM' : M' (inr unit) (inr unit) ≠ 0 := by simpa [hM]
case neg.intro.inl.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 ⬝ M
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M' ⬝ List.prod (List.map toMatrix L'))
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
case neg.intro.inl
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 ⬝ M
hM' : M' (inr ()) (inr ()) ≠ 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
rcases exists_isTwoBlockDiagonal_of_ne_zero M' hM' with ⟨L, L', hLL'⟩
case neg.intro.inl.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 ⬝ M
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ (M' ⬝ List.prod (List.map toMatrix L')))
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
case neg.intro.inl.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 ⬝ M
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M' ⬝ List.prod (List.map toMatrix L'))
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
rw [Matrix.mul_assoc] at hLL'
case neg.intro.inl.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 ⬝ M
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ (M' ⬝ List.prod (List.map toMatrix L')))
⊢ IsTwoBlockDiagonal
    (List.prod (List.map toMatrix (L ++ [{ i := inr (), j := inl i, hij := (_ : ¬inr () = inl i), c := 1 }])) ⬝ M ⬝
      List.prod (List.map toMatrix L'))
case neg.intro.inl.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 ⬝ M
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ (M' ⬝ List.prod (List.map toMatrix L')))
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
refine' ⟨L ++ [⟨inr unit, inl i, by simp, 1⟩], L', _⟩
case neg.intro.inl.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 ⬝ M
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ (M' ⬝ List.prod (List.map toMatrix L')))
⊢ IsTwoBlockDiagonal
    (List.prod (List.map toMatrix L) ⬝ (transvection (inr ()) (inl i) 1 ⬝ M ⬝ List.prod (List.map toMatrix L')))
case neg.intro.inl.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 ⬝ M
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ (M' ⬝ List.prod (List.map toMatrix L')))
⊢ IsTwoBlockDiagonal
    (List.prod (List.map toMatrix (L ++ [{ i := inr (), j := inl i, hij := (_ : ¬inr () = inl i), c := 1 }])) ⬝ M ⬝
      List.prod (List.map toMatrix L'))
simp only [List.map_append, List.prod_append, Matrix.mul_one, toMatrix_mk, List.prod_cons,
  List.prod_nil, mul_eq_mul, List.map, Matrix.mul_assoc (L.map toMatrix).prod]
no goals
case neg.intro.inl.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 ⬝ M
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ (M' ⬝ List.prod (List.map toMatrix L')))
⊢ IsTwoBlockDiagonal
    (List.prod (List.map toMatrix L) ⬝ (transvection (inr ()) (inl i) 1 ⬝ M ⬝ List.prod (List.map toMatrix L')))
exact hLL'
no goals
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 ⬝ M
⊢ M' (inr ()) (inr ()) ≠ 0
simpa [hM]
no goals
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 ⬝ M
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ (M' ⬝ List.prod (List.map toMatrix L')))
⊢ inr () ≠ inl i
simp
case neg.intro.inr
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M ⬝ transvection (inl i) (inr ()) 1
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
case neg.intro.inr
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
let M' := M ⬝ transvection (inl i) (inr unit) 1
case neg.intro.inr
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M ⬝ transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
case neg.intro.inr
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M ⬝ transvection (inl i) (inr ()) 1
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
have hM' : M' (inr unit) (inr unit) ≠ 0 := by simpa [hM]
case neg.intro.inr.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M ⬝ transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M' ⬝ List.prod (List.map toMatrix L'))
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
case neg.intro.inr
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M ⬝ transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
rcases exists_isTwoBlockDiagonal_of_ne_zero M' hM' with ⟨L, L', hLL'⟩
case neg.intro.inr.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M ⬝ transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M' ⬝ List.prod (List.map toMatrix L'))
⊢ IsTwoBlockDiagonal
    (List.prod (List.map toMatrix L) ⬝ M ⬝
      List.prod (List.map toMatrix ({ i := inl i, j := inr (), hij := (_ : ¬inl i = inr ()), c := 1 } :: L')))
case neg.intro.inr.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M ⬝ transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M' ⬝ List.prod (List.map toMatrix L'))
⊢ ∃ L L', IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L'))
refine' ⟨L, ⟨inl i, inr unit, by simp, 1⟩::L', _⟩
case neg.intro.inr.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M ⬝ transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M' ⬝ List.prod (List.map toMatrix L'))
⊢ IsTwoBlockDiagonal
    (List.prod (List.map toMatrix L) ⬝ M ⬝ transvection (inl i) (inr ()) 1 ⬝ List.prod (List.map toMatrix L'))
case neg.intro.inr.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M ⬝ transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M' ⬝ List.prod (List.map toMatrix L'))
⊢ IsTwoBlockDiagonal
    (List.prod (List.map toMatrix L) ⬝ M ⬝
      List.prod (List.map toMatrix ({ i := inl i, j := inr (), hij := (_ : ¬inl i = inr ()), c := 1 } :: L')))
simp only [← Matrix.mul_assoc, toMatrix_mk, List.prod_cons, mul_eq_mul, List.map]
case neg.intro.inr.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M ⬝ transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M' ⬝ List.prod (List.map toMatrix L'))
⊢ IsTwoBlockDiagonal
    (List.prod (List.map toMatrix L) ⬝ (M ⬝ transvection (inl i) (inr ()) 1) ⬝ List.prod (List.map toMatrix L'))
case neg.intro.inr.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M ⬝ transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M' ⬝ List.prod (List.map toMatrix L'))
⊢ IsTwoBlockDiagonal
    (List.prod (List.map toMatrix L) ⬝ M ⬝ transvection (inl i) (inr ()) 1 ⬝ List.prod (List.map toMatrix L'))
rw [Matrix.mul_assoc (L.map toMatrix).prod]
no goals
case neg.intro.inr.intro.intro
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M ⬝ transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M' ⬝ List.prod (List.map toMatrix L'))
⊢ IsTwoBlockDiagonal
    (List.prod (List.map toMatrix L) ⬝ (M ⬝ transvection (inl i) (inr ()) 1) ⬝ List.prod (List.map toMatrix L'))
exact hLL'
no goals
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M ⬝ transvection (inl i) (inr ()) 1
⊢ M' (inr ()) (inr ()) ≠ 0
simpa [hM]
no goals
n : Type ?u.226982
p : Type ?u.226985
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M✝ M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), ↑of (fun i j => M (inl i) (inr j)) i j = OfNat.ofNat 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), ↑of (fun i j => M (inr i) (inl j)) i j = OfNat.ofNat 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M ⬝ transvection (inl i) (inr ()) 1
hM' : M' (inr ()) (inr ()) ≠ 0
L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜)
hLL' : IsTwoBlockDiagonal (List.prod (List.map toMatrix L) ⬝ M' ⬝ List.prod (List.map toMatrix L'))
⊢ inl i ≠ inr ()
simp