-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (goal)
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
⊢ natDegree (coeff (lieCharpoly R M x y) i) ≤ j
have hf : ∀ (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])).natDegree ≤
    1
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