n : Type ?u.204767
p : Type ?u.204770
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
this : listTransvecRow M = listTransvecRow (List.prod (listTransvecCol M) ⬝ M)
⊢ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) (inr ()) (inl i) = 0
n : Type ?u.204767
p : Type ?u.204770
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
⊢ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) (inr ()) (inl i) = 0
have : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod ⬝ M) := by
  simp [listTransvecRow, listTransvecCol_mul_last_row]
n : Type ?u.204767
p : Type ?u.204770
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
this : listTransvecRow M = listTransvecRow (List.prod (listTransvecCol M) ⬝ M)
⊢ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow (List.prod (listTransvecCol M) ⬝ M))) (inr ())
      (inl i) =
    0
n : Type ?u.204767
p : Type ?u.204770
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
this : listTransvecRow M = listTransvecRow (List.prod (listTransvecCol M) ⬝ M)
⊢ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) (inr ()) (inl i) = 0
rw [this]
case hM
n : Type ?u.204767
p : Type ?u.204770
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
this : listTransvecRow M = listTransvecRow (List.prod (listTransvecCol M) ⬝ M)
⊢ (List.prod (listTransvecCol M) ⬝ M) (inr ()) (inr ()) ≠ 0
n : Type ?u.204767
p : Type ?u.204770
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
this : listTransvecRow M = listTransvecRow (List.prod (listTransvecCol M) ⬝ M)
⊢ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow (List.prod (listTransvecCol M) ⬝ M))) (inr ())
      (inl i) =
    0
apply mul_listTransvecRow_last_row
no goals
case hM
n : Type ?u.204767
p : Type ?u.204770
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
this : listTransvecRow M = listTransvecRow (List.prod (listTransvecCol M) ⬝ M)
⊢ (List.prod (listTransvecCol M) ⬝ M) (inr ()) (inr ()) ≠ 0
simpa [listTransvecCol_mul_last_row] using hM
no goals
n : Type ?u.204767
p : Type ?u.204770
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
⊢ listTransvecRow M = listTransvecRow (List.prod (listTransvecCol M) ⬝ M)
simp [listTransvecRow, listTransvecCol_mul_last_row]