-- Mathlib/LinearAlgebra/Matrix/Polynomial.lean
theorem leadingCoeff_det_X_one_add_C (A : Matrix n n α) :
    leadingCoeff (det ((X : α[X]) • (1 : Matrix n n α[X]) + A.map C)) = 1

Proof state:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ (X • 1 + A.map ⇑C).det.leadingCoeff = 1

Tactic:
cases subsingleton_or_nontrivial α

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

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

Proof state:
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 : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree < Fintype.card n
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)

Tactic:
have H := coeff_eq_zero_of_natDegree_lt h

Result:
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 : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree < Fintype.card n
H : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.coeff (Fintype.card n) = 0
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)

Proof state:
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ (X • 1 + A.map ⇑C).det.leadingCoeff = 1

Tactic:
rw [← @det_one n, ← coeff_det_X_add_C_card _ A, leadingCoeff]

Result:
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree =
    (X • Matrix.map 1 ⇑C + A.map ⇑C).det.coeff (Fintype.card n)

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

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree =
    (X • Matrix.map 1 ⇑C + A.map ⇑C).det.coeff (Fintype.card n)

Tactic:
simp only [Matrix.map_one, C_eq_zero, RingHom.map_one]

Result:
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)

Proof state:
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 : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree < Fintype.card n
H : det 1 = 0
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)

Tactic:
simp at H

Result:
no goals

Proof state:
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 : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree = Fintype.card n
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)

Tactic:
simp only [RingHom.map_one, Matrix.map_one, C_eq_zero] at h

Result:
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 : (X • 1 + A.map ⇑C).det.natDegree = Fintype.card n
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)

Proof state:
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 : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree < Fintype.card n
H : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.coeff (Fintype.card n) = 0
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)

Tactic:
rw [coeff_det_X_add_C_card] at H

Result:
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 : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree < Fintype.card n
H : det 1 = 0
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)

Proof state:
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 : (X • 1 + A.map ⇑C).det.natDegree = Fintype.card n
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)

Tactic:
rw [h]

Result:
no goals

Proof state:
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)

Tactic:
rcases (natDegree_det_X_add_C_le 1 A).eq_or_lt with h | h

Result:
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 : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree = Fintype.card n
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (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 : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree < Fintype.card n
⊢ (X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)