-- Mathlib/Algebra/Lie/CartanExists.lean
lemma lieCharpoly_coeff_natDegree [Nontrivial R] (i j : ℕ) (hij : i + j = finrank R M) :
    ((lieCharpoly R M x y).coeff i).natDegree ≤ j

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
⊢ ((LieAlgebra.engel_isBot_of_isMin.lieCharpoly R M x y).coeff i).natDegree ≤ j

Tactic:
rw [← mul_one j, lieCharpoly, coeff_map]

Result:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
⊢ (↑(MvPolynomial.aeval fun i => C (((chooseBasis R L).repr y) i) * X + C (((chooseBasis R L).repr x) i))
        (((↑φ).polyCharpoly (chooseBasis R L)).coeff i)).natDegree ≤
    j * 1

Proof state:
case hf
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
⊢ ∀ (i : ChooseBasisIndex R L), (C (((chooseBasis R L).repr y) i) * X + C (((chooseBasis R L).repr x) i)).natDegree ≤ 1

Tactic:
intro k

Result:
case hf
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
k : ChooseBasisIndex R L
⊢ (C (((chooseBasis R L).repr y) k) * X + C (((chooseBasis R L).repr x) k)).natDegree ≤ 1

Proof state:
case hf
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
k : ChooseBasisIndex R L
⊢ (C (((chooseBasis R L).repr y) k) * X + C (((chooseBasis R L).repr x) k)).natDegree ≤ 1

Tactic:
apply Polynomial.natDegree_add_le_of_degree_le

Result:
case hf.hp
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
k : ChooseBasisIndex R L
⊢ (C (((chooseBasis R L).repr y) k) * X).natDegree ≤ 1

case hf.hq
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
k : ChooseBasisIndex R L
⊢ (C (((chooseBasis R L).repr x) k)).natDegree ≤ 1

Proof state:
case hF
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
⊢ (((↑φ).polyCharpoly (chooseBasis R L)).coeff i).totalDegree ≤ j

Tactic:
apply (polyCharpoly_coeff_isHomogeneous φ (chooseBasis R L) _ _ hij).totalDegree_le

Result:
no goals

Proof state:
case hf.hp
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
k : ChooseBasisIndex R L
⊢ X.natDegree ≤ 1

Tactic:
simp only [natDegree_X, le_rfl]

Result:
no goals

Proof state:
case hf.hp
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
k : ChooseBasisIndex R L
⊢ (C (((chooseBasis R L).repr y) k) * X).natDegree ≤ 1

Tactic:
apply (Polynomial.natDegree_C_mul_le _ _).trans

Result:
case hf.hp
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
k : ChooseBasisIndex R L
⊢ X.natDegree ≤ 1

Proof state:
case hf.hq
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
k : ChooseBasisIndex R L
⊢ (C (((chooseBasis R L).repr x) k)).natDegree ≤ 1

Tactic:
simp only [natDegree_C, zero_le]

Result:
no goals

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
⊢ (↑(MvPolynomial.aeval fun i => C (((chooseBasis R L).repr y) i) * X + C (((chooseBasis R L).repr x) i))
        (((↑φ).polyCharpoly (chooseBasis R L)).coeff i)).natDegree ≤
    j * 1

Tactic:
apply MvPolynomial.aeval_natDegree_le

Result:
case hF
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
⊢ (((↑φ).polyCharpoly (chooseBasis R L)).coeff i).totalDegree ≤ j

case hf
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : Module.Finite R L
inst✝³ : Free R L
inst✝² : Module.Finite R M
inst✝¹ : Free R M
x y : L
inst✝ : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
⊢ ∀ (i : ChooseBasisIndex R L), (C (((chooseBasis R L).repr y) i) * X + C (((chooseBasis R L).repr x) i)).natDegree ≤ 1