-- Module: Mathlib.Algebra.Lie.CartanExists
Goal:
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : Module.Finite R L
inst_8 : Free R L
inst_9 : Module.Finite R M
inst_10 : Free R M
x y : L
inst_11 : Nontrivial R
i j : ℕ
hij : i + j = finrank R M
rw : natDegree (coeff (lieCharpoly R M x y) i) ≤ j * 1
rw₁ :
  (coeff
        (Polynomial.map
          (↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
                HAdd.hAdd (β := R[X])
                  (HMul.hMul (α := R[X]) (β := R[X])
                    ((C : (a : R) → R[X])
                        ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) y :
                              Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                            (a : ChooseBasisIndex R L) → R)
                          i) :
                      R[X])
                    X)
                  ((C : (a : R) → R[X])
                      ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) x :
                            Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                          (a : ChooseBasisIndex R L) → R)
                        i) :
                    R[X])) :
            MvPolynomial (ChooseBasisIndex R L) R →+* R[X])
          (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L)))
        i).natDegree ≤
    j * 1
rw₂ rw₃ rw₄ :
  natDegree.{u_2} (R := R)
      (((↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
                HAdd.hAdd (β := R[X])
                  (HMul.hMul (α := R[X]) (β := R[X])
                    ((C : (a : R) → R[X])
                        ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) y :
                              Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                            (a : ChooseBasisIndex R L) → R)
                          i) :
                      R[X])
                    X)
                  ((C : (a : R) → R[X])
                      ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) x :
                            Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                          (a : ChooseBasisIndex R L) → R)
                        i) :
                    R[X])) :
            MvPolynomial (ChooseBasisIndex R L) R →+* R[X]) :
          (a : MvPolynomial (ChooseBasisIndex R L) R) → R[X])
        (coeff (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L)) i)) ≤
    j * 1
hF :
  MvPolynomial.totalDegree (σ := ChooseBasisIndex R L)
      (coeff (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L)) i) ≤
    j
hf hf₁ hf₂ :
  ∀ (k : ChooseBasisIndex R L),
    (HAdd.hAdd (β := R[X])
          (HMul.hMul (α := R[X]) (β := R[X])
            ((C : (a : R) → R[X])
                ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) y :
                      Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                    (a : ChooseBasisIndex R L) → R)
                  k) :
              R[X])
            X)
          ((C : (a : R) → R[X])
              ((((Basis.repr (chooseBasis R L) : (a : L) → ChooseBasisIndex R L →₀ R) x :
                    Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                  (a : ChooseBasisIndex R L) → R)
                k) :
            R[X])).natDegree ≤
      1
⊢ natDegree (coeff (lieCharpoly R M x y) i) ≤ j

Tactic:
classical
  rw [← mul_one j, lieCharpoly, coeff_map]
  apply MvPolynomial.aeval_natDegree_le
  · apply (polyCharpoly_coeff_isHomogeneous φ (chooseBasis R L) _ _ hij).totalDegree_le
  intro k
  exact natDegree_linear_le

Premises used: Polynomial.coeff_map, _private.0.LieAlgebra.engel_isBot_of_isMin.lieCharpoly, Polynomial.natDegree_linear_le, mul_one, MvPolynomial.aeval_natDegree_le