-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank [Nontrivial R] :
    IsNilRegular φ x ↔ (φ x).charpoly.natTrailingDegree = nilRank φ

Proof state:
case mpr
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
h : (charpoly (φ x)).natTrailingDegree = φ.nilRank
⊢ (charpoly (φ x)).coeff (charpoly (φ x)).natTrailingDegree ≠ 0

Tactic:
apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr

Result:
case mpr
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
h : (charpoly (φ x)).natTrailingDegree = φ.nilRank
⊢ charpoly (φ x) ≠ 0

Proof state:
case mp
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
h : (charpoly (φ x)).coeff φ.nilRank ≠ 0
⊢ (charpoly (φ x)).natTrailingDegree = φ.nilRank

Tactic:
exact le_antisymm
  (Polynomial.natTrailingDegree_le_of_ne_zero h)
  (nilRank_le_natTrailingDegree_charpoly φ x)

Result:
no goals

Proof state:
case mpr
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
h : (charpoly (φ x)).natTrailingDegree = φ.nilRank
⊢ charpoly (φ x) ≠ 0

Tactic:
apply (LinearMap.charpoly_monic _).ne_zero

Result:
no goals

Proof state:
case mp
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
⊢ (charpoly (φ x)).coeff φ.nilRank ≠ 0 → (charpoly (φ x)).natTrailingDegree = φ.nilRank

Tactic:
intro h

Result:
case mp
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
h : (charpoly (φ x)).coeff φ.nilRank ≠ 0
⊢ (charpoly (φ x)).natTrailingDegree = φ.nilRank

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
⊢ (charpoly (φ x)).coeff φ.nilRank ≠ 0 ↔ (charpoly (φ x)).natTrailingDegree = φ.nilRank

Tactic:
constructor

Result:
case mp
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
⊢ (charpoly (φ x)).coeff φ.nilRank ≠ 0 → (charpoly (φ x)).natTrailingDegree = φ.nilRank

case mpr
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
⊢ (charpoly (φ x)).natTrailingDegree = φ.nilRank → (charpoly (φ x)).coeff φ.nilRank ≠ 0

Proof state:
case mpr
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
h : (charpoly (φ x)).natTrailingDegree = φ.nilRank
⊢ (charpoly (φ x)).coeff φ.nilRank ≠ 0

Tactic:
rw [← h]

Result:
case mpr
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
h : (charpoly (φ x)).natTrailingDegree = φ.nilRank
⊢ (charpoly (φ x)).coeff (charpoly (φ x)).natTrailingDegree ≠ 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
⊢ φ.IsNilRegular x ↔ (charpoly (φ x)).natTrailingDegree = φ.nilRank

Tactic:
rw [isNilRegular_def]

Result:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
⊢ (charpoly (φ x)).coeff φ.nilRank ≠ 0 ↔ (charpoly (φ x)).natTrailingDegree = φ.nilRank

Proof state:
case mpr
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
⊢ (charpoly (φ x)).natTrailingDegree = φ.nilRank → (charpoly (φ x)).coeff φ.nilRank ≠ 0

Tactic:
intro h

Result:
case mpr
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
inst✝² : Module.Finite R L
inst✝¹ : Free R L
x : L
inst✝ : Nontrivial R
h : (charpoly (φ x)).natTrailingDegree = φ.nilRank
⊢ (charpoly (φ x)).coeff φ.nilRank ≠ 0