-- 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
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)
simp_rw :
  Eq (α := R[X])
    (Polynomial.map
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(aeval r) : R[X] →+* 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)))
simp_rw₁ :
  Eq (α := R[X])
    (Polynomial.map
      (↑(AlgHom.comp (aeval 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)
      (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)))
⊢ 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 simp_rw₂ : Eq (α := R[X])
  (Polynomial.map
    (↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
          (aeval r : (a : R[X]) → R)
            (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)
    (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)))
Tactic: simp_rw [← coe_aeval_eq_evalRingHom, ← AlgHom.comp_toRingHom, MvPolynomial.comp_aeval,
    map_add, map_mul, aeval_C, Algebra.algebraMap_self, RingHom.id_apply, aeval_X, aux,
    MvPolynomial.coe_aeval_eq_eval, polyCharpoly_map_eq_charpoly, LieHom.coe_toLinearMap, map_add]