case zero
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.zero
⊢ ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D

case succ
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.succ r
⊢ ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n✝ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝³ : Fintype n✝
inst✝² : Fintype p
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
⊢ ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
induction' hn : Fintype.card n with r IH generalizing n M
case zero
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.zero
⊢ List.prod (List.map toMatrix []) ⬝ M ⬝ List.prod (List.map toMatrix []) = diagonal fun x => 1
case zero
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.zero
⊢ ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
refine' ⟨List.nil, List.nil, fun _ => 1, _⟩
case zero.a.h
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.zero
i j : n
⊢ (List.prod (List.map toMatrix []) ⬝ M ⬝ List.prod (List.map toMatrix [])) i j = diagonal (fun x => 1) i j
case zero
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.zero
⊢ List.prod (List.map toMatrix []) ⬝ M ⬝ List.prod (List.map toMatrix []) = diagonal fun x => 1
ext (i j)
case zero.a.h
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : IsEmpty n
i j : n
⊢ (List.prod (List.map toMatrix []) ⬝ M ⬝ List.prod (List.map toMatrix [])) i j = diagonal (fun x => 1) i j
case zero.a.h
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.zero
i j : n
⊢ (List.prod (List.map toMatrix []) ⬝ M ⬝ List.prod (List.map toMatrix [])) i j = diagonal (fun x => 1) i j
rw [Fintype.card_eq_zero_iff] at hn
no goals
case zero.a.h
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : IsEmpty n
i j : n
⊢ (List.prod (List.map toMatrix []) ⬝ M ⬝ List.prod (List.map toMatrix [])) i j = diagonal (fun x => 1) i j
exact hn.elim' i
case succ
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.succ r
e : n ≃ Fin r ⊕ Unit
⊢ ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
case succ
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.succ r
⊢ ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
have e : n ≃ Sum (Fin r) Unit := by
  refine' Fintype.equivOfCardEq _
  rw [hn]
  rw [@Fintype.card_sum (Fin r) Unit _ _]
  simp
case succ
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.succ r
e : n ≃ Fin r ⊕ Unit
⊢ ∃ L L' D, List.prod (List.map toMatrix L) ⬝ ↑(reindexAlgEquiv 𝕜 e) M ⬝ List.prod (List.map toMatrix L') = diagonal D
case succ
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.succ r
e : n ≃ Fin r ⊕ Unit
⊢ ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
apply reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal M e
no goals
case succ
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.succ r
e : n ≃ Fin r ⊕ Unit
⊢ ∃ L L' D, List.prod (List.map toMatrix L) ⬝ ↑(reindexAlgEquiv 𝕜 e) M ⬝ List.prod (List.map toMatrix L') = diagonal D
apply
  exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction fun N =>
    IH (Fin r) N (by simp)
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.succ r
⊢ Fintype.card n = Fintype.card (Fin r ⊕ Unit)
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.succ r
⊢ n ≃ Fin r ⊕ Unit
refine' Fintype.equivOfCardEq _
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.succ r
⊢ Nat.succ r = Fintype.card (Fin r ⊕ Unit)
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.succ r
⊢ Fintype.card n = Fintype.card (Fin r ⊕ Unit)
rw [hn]
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.succ r
⊢ Nat.succ r = Fintype.card (Fin r) + Fintype.card Unit
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.succ r
⊢ Nat.succ r = Fintype.card (Fin r ⊕ Unit)
rw [@Fintype.card_sum (Fin r) Unit _ _]
no goals
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.succ r
⊢ Nat.succ r = Fintype.card (Fin r) + Fintype.card Unit
simp
no goals
n✝¹ : Type ?u.315793
p : Type ?u.315796
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) 𝕜
inst✝⁵ : Fintype n✝¹
inst✝⁴ : Fintype p
n✝ : Type
inst✝³ : Fintype n✝
inst✝² : DecidableEq n✝
M✝ : Matrix n✝ n✝ 𝕜
x✝ : ℕ
hn✝ : Fintype.card n✝ = x✝
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, List.prod (List.map toMatrix L) ⬝ M ⬝ List.prod (List.map toMatrix L') = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = Nat.succ r
e : n ≃ Fin r ⊕ Unit
N : Matrix (Fin r) (Fin r) 𝕜
⊢ Fintype.card (Fin r) = r
simp