case inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Subsingleton α
⊢ leadingCoeff (det (X • 1 + Matrix.map A ↑C)) = 1

case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ leadingCoeff (det (X • 1 + Matrix.map A ↑C)) = 1
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ leadingCoeff (det (X • 1 + Matrix.map A ↑C)) = 1
cases subsingleton_or_nontrivial α
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) (Fintype.card n)
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ leadingCoeff (det (X • 1 + Matrix.map A ↑C)) = 1
rw [← @det_one n, ← coeff_det_X_add_C_card _ A, leadingCoeff]
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) (Fintype.card n)
simp only [Matrix.map_one, C_eq_zero, RingHom.map_one]
case inr.inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) = Fintype.card n
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)

case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) < Fintype.card n
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
cases' (natDegree_det_X_add_C_le 1 A).eq_or_lt with h h
no goals
case inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Subsingleton α
⊢ leadingCoeff (det (X • 1 + Matrix.map A ↑C)) = 1
simp
case inr.inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • 1 + Matrix.map A ↑C)) = Fintype.card n
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
case inr.inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) = Fintype.card n
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
simp only [RingHom.map_one, Matrix.map_one, C_eq_zero] at h
no goals
case inr.inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • 1 + Matrix.map A ↑C)) = Fintype.card n
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
rw [h]
case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) < Fintype.card n
H : coeff (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) (Fintype.card n) = 0
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) < Fintype.card n
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
have H := coeff_eq_zero_of_natDegree_lt h
case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) < Fintype.card n
H : det 1 = 0
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) < Fintype.card n
H : coeff (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) (Fintype.card n) = 0
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
rw [coeff_det_X_add_C_card] at H
no goals
case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) < Fintype.card n
H : det 1 = 0
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
simp at H