-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem charpoly_degree_eq_dim [Nontrivial R] (M : Matrix n n R) :
    M.charpoly.degree = Fintype.card n

Proof state:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ ↑(Fintype.card n - 1) < ↑(Fintype.card n)

Tactic:
rw [Nat.cast_lt]

Result:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ Fintype.card n - 1 < Fintype.card n

Proof state:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∑ i : n, (X - C (M i i)).natDegree = Fintype.card n

Tactic:
simp_rw [natDegree_X_sub_C]

Result:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∑ x : n, 1 = Fintype.card n

Proof state:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ M.charpoly.degree = ↑(Fintype.card n)

Tactic:
rw [← sub_add_cancel M.charpoly (∏ i : n, (X - C (M i i)))]

Result:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ (M.charpoly - ∏ i : n, (X - C (M i i)) + ∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)

Proof state:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (Fintype.card n).pred < Fintype.card n

Tactic:
apply Nat.pred_lt

Result:
case neg.a
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ Fintype.card n ≠ 0

Proof state:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∑ x : n, 1 = Fintype.card n

Tactic:
rw [← Finset.card_univ, sum_const, smul_eq_mul, mul_one]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (M.charpoly - ∏ i : n, (X - C (M i i))).degree < (∏ i : n, (X - C (M i i))).degree

Tactic:
rw [h1]

Result:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (M.charpoly - ∏ i : n, (X - C (M i i))).degree < ↑(Fintype.card n)

Proof state:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
⊢ M.charpoly.degree = ↑(Fintype.card n)

Tactic:
by_cases h : Fintype.card n = 0

Result:
case pos
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ M.charpoly.degree = ↑(Fintype.card n)

case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ M.charpoly.degree = ↑(Fintype.card n)

Proof state:
case h
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∏ i : n, (X - C (M i i)).leadingCoeff ≠ 0

Tactic:
simp_rw [(monic_X_sub_C _).leadingCoeff]

Result:
case h
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∏ x : n, 1 ≠ 0

Proof state:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)

Tactic:
exact h1

Result:
no goals

Proof state:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (M.charpoly - ∏ i : n, (X - C (M i i)) + ∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)

Tactic:
rw [degree_add_eq_right_of_degree_lt]

Result:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)

case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (M.charpoly - ∏ i : n, (X - C (M i i))).degree < (∏ i : n, (X - C (M i i))).degree

Proof state:
case pos
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ M.charpoly.degree = ↑(Fintype.card n)

Tactic:
rw [h]

Result:
case pos
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ M.charpoly.degree = ↑0

Proof state:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (M.charpoly - ∏ i : n, (X - C (M i i))).degree < ↑(Fintype.card n)

Tactic:
apply lt_trans (charpoly_sub_diagonal_degree_lt M)

Result:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ ↑(Fintype.card n - 1) < ↑(Fintype.card n)

Proof state:
case pos
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ degree 1 = ↑0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)

Tactic:
rw [degree_eq_iff_natDegree_eq_of_pos (Nat.pos_of_ne_zero h), natDegree_prod']

Result:
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∑ i : n, (X - C (M i i)).natDegree = Fintype.card n

case h
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∏ i : n, (X - C (M i i)).leadingCoeff ≠ 0