awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
⊢ IsSolvable.{u_2} ↥(LieIdeal.killingCompl R L ⊤)
have refine : ∀ (x : L),
  Membership.mem (γ := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) x →
    ∀ (y : L),
      Membership.mem (γ := LieIdeal R L)
          (Bracket.bracket (L := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) (LieIdeal.killingCompl R L ⊤)) y →
        Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
Tactic: refine LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero _ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : IsNoetherian R L
inst_6 : Module.Free R L
x : L
hx : Membership.mem (γ := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) x
y : L
h :
  Membership.mem (γ := LieIdeal R L)
    (Bracket.bracket (L := LieIdeal R L) (LieIdeal.killingCompl R L ⊤) (LieIdeal.killingCompl R L ⊤)) y
⊢ Eq.{u_1 + 1} (α := R) ((((killingForm R L : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R) (0 : R)
have rw : Eq.{u_1 + 1} (α := R) ((((LieModule.traceForm R L L : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) x : R) (0 : R)
Tactic: rw [LieModule.traceForm_comm]
-- 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
⊢ natDegree (R := R[X]) (lieCharpoly R M x y) = finrank R M
have rw : natDegree
    (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))) =
  finrank R M
Tactic: rw [lieCharpoly, (polyCharpoly_monic _ _).natDegree_map, polyCharpoly_natDegree]
-- 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
rw :
  natDegree
      (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))) =
    finrank R M
⊢ natDegree (R := R[X]) (lieCharpoly R M x y) = finrank R M
have rw₁ : natDegree (R := MvPolynomial.{u_3, u_2} (ChooseBasisIndex R L) R)
    (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L)) =
  finrank R M
Tactic: rw [lieCharpoly, (polyCharpoly_monic _ _).natDegree_map, polyCharpoly_natDegree]
-- 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
rw :
  natDegree
      (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))) =
    finrank R M
rw₁ :
  natDegree (R := MvPolynomial.{u_3, u_2} (ChooseBasisIndex R L) R)
      (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L)) =
    finrank R M
⊢ natDegree (R := R[X]) (lieCharpoly R M x y) = finrank R M
have rw₂ : finrank R M = finrank R M
Tactic: rw [lieCharpoly, (polyCharpoly_monic _ _).natDegree_map, polyCharpoly_natDegree]
-- 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
r : R
⊢ Eq (α := R[X]) (Polynomial.map (evalRingHom r) (lieCharpoly R M x y))
    (charpoly.{u_2, u_4} (M := M) (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y + x)))
have rw : Polynomial.map
    (RingHom.comp (evalRingHom 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]))
    (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L)) =
  charpoly.{u_2, u_4} (M := M) (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y + x))
Tactic: rw [lieCharpoly, map_map]
-- 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
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
⊢ Eq (α := (i : ChooseBasisIndex R L) → R)
    (fun (i : ChooseBasisIndex R L) ↦
      HAdd.hAdd (β := R)
        (HMul.hMul (α := R)
          ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) y : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
                (a : ChooseBasisIndex R L) → R)
              i :
            R)
          r)
        ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) x : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
              (a : ChooseBasisIndex R L) → R)
            i :
          R))
    (⇑((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) (r • y + x) : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
      (a : ChooseBasisIndex R L) → R)
have h : ∀ (i : ChooseBasisIndex R L),
  HAdd.hAdd (β := R)
      (HMul.hMul (α := R)
        ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) y : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
              (a : ChooseBasisIndex R L) → R)
            i :
          R)
        r)
      ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) x : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
            (a : ChooseBasisIndex R L) → R)
          i :
        R) =
    (((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) (r • y + x) : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
        (a : ChooseBasisIndex R L) → R)
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (hypothesis)
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
r : R
b : Basis (ChooseBasisIndex R L) R L := chooseBasis R L
⊢ Polynomial.map
      (RingHom.comp (evalRingHom r)
        (↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
              HAdd.hAdd (β := R[X])
                (HMul.hMul (α := R[X]) (β := R[X])
                  ((C : (a : R) → R[X])
                      ((((b.repr : (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])
                    ((((b.repr : (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) b) =
    charpoly.{u_2, u_4} (M := M) (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y + x))
have aux : Eq (α := (i : ChooseBasisIndex R L) → R)
  (fun (i : ChooseBasisIndex R L) ↦
    HAdd.hAdd (β := R)
      (HMul.hMul (α := R)
        ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) y : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
              (a : ChooseBasisIndex R L) → R)
            i :
          R)
        r)
      ((((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) x : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
            (a : ChooseBasisIndex R L) → R)
          i :
        R))
  (⇑((b.repr : (a : L) → ChooseBasisIndex R L →₀ R) (r • y + x) : Finsupp.{u_3, u_2} (ChooseBasisIndex R L) R) :
    (a : ChooseBasisIndex R L) → R)
Tactic: have aux : (fun i ↦ (b.repr y) i * r + (b.repr x) i) = b.repr (r • y + x) := by
    ext i; simp [mul_comm r]
-- 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
⊢ natDegree (coeff (lieCharpoly R M x y) i) ≤ j
have 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
Tactic: rw [← mul_one j, lieCharpoly, coeff_map]
-- 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
⊢ 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
have hF : MvPolynomial.totalDegree (σ := ChooseBasisIndex R L) (coeff (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L)) i) ≤
  j
Tactic: apply MvPolynomial.aeval_natDegree_le
-- 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
hF :
  MvPolynomial.totalDegree (σ := ChooseBasisIndex R L)
      (coeff (polyCharpoly (↑φ : L →ₗ[R] End R M) (chooseBasis R L)) i) ≤
    j
⊢ 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
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: apply MvPolynomial.aeval_natDegree_le
-- 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
⊢ natDegree (coeff (lieCharpoly R M x y) i) ≤ j
have rw : natDegree (coeff (lieCharpoly R M x y) i) ≤ j * 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
-- 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
⊢ natDegree (coeff (lieCharpoly R M x y) i) ≤ j
have 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
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
-- 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
⊢ natDegree (coeff (lieCharpoly R M x y) i) ≤ j
have 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
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