-- 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
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)))
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)))
simp_rw₃ :
  Polynomial.map
      (↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
            HAdd.hAdd (α := R) (β := R)
              ((aeval r : (a : R[X]) → R)
                  (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) :
                R)
              ((aeval r : (a : R[X]) → R)
                  ((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]) :
                R)) :
        MvPolynomial (ChooseBasisIndex R L) R →+* R)
      (polyCharpoly (↑φ : L →ₗ[R] End R M) b) =
    charpoly
      (HAdd.hAdd (α := End R M) (β := End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y) : End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
simp_rw₄ :
  Polynomial.map
      (↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
            HAdd.hAdd (β := R)
              (HMul.hMul (α := R) (β := R)
                ((aeval r : (a : R[X]) → R)
                    ((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]) :
                  R)
                ((aeval r : (a : R[X]) → R) X : R))
              ((aeval r : (a : R[X]) → R)
                  ((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]) :
                R)) :
        MvPolynomial (ChooseBasisIndex R L) R →+* R)
      (polyCharpoly (↑φ : L →ₗ[R] End R M) b) =
    charpoly
      (HAdd.hAdd (α := End R M) (β := End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y) : End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
simp_rw₅ :
  Polynomial.map
      (↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
            HAdd.hAdd (β := R)
              (HMul.hMul (α := R) (β := R)
                ((algebraMap R R : (a : R) → 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)
                ((aeval r : (a : R[X]) → R) X : R))
              ((algebraMap R R : (a : 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) :
                R)) :
        MvPolynomial (ChooseBasisIndex R L) R →+* R)
      (polyCharpoly (↑φ : L →ₗ[R] End R M) b) =
    charpoly
      (HAdd.hAdd (α := End R M) (β := End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y) : End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
simp_rw₆ :
  Polynomial.map
      (↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
            HAdd.hAdd (β := R)
              (HMul.hMul (α := R) (β := R)
                ((RingHom.id R : (a : R) → 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)
                ((aeval r : (a : R[X]) → R) X : R))
              ((RingHom.id R : (a : 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) :
                R)) :
        MvPolynomial (ChooseBasisIndex R L) R →+* R)
      (polyCharpoly (↑φ : L →ₗ[R] End R M) b) =
    charpoly
      (HAdd.hAdd (α := End R M) (β := End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y) : End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
simp_rw₇ :
  Polynomial.map
      (↑(MvPolynomial.aeval fun (i : ChooseBasisIndex R L) ↦
            HAdd.hAdd (β := R)
              (HMul.hMul (α := R) (β := 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)
                ((aeval r : (a : R[X]) → R) X : 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)) :
        MvPolynomial (ChooseBasisIndex R L) R →+* R)
      (polyCharpoly (↑φ : L →ₗ[R] End R M) b) =
    charpoly
      (HAdd.hAdd (α := End R M) (β := End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y) : End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
simp_rw₈ :
  Polynomial.map
      (↑(MvPolynomial.aeval 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)) :
        MvPolynomial (ChooseBasisIndex R L) R →+* R)
      (polyCharpoly (↑φ : L →ₗ[R] End R M) b) =
    charpoly
      (HAdd.hAdd (α := End R M) (β := End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y) : End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
simp_rw₉ :
  Polynomial.map
      (↑(MvPolynomial.aeval
            (⇑((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)) :
        MvPolynomial (ChooseBasisIndex R L) R →+* R)
      (polyCharpoly (↑φ : L →ₗ[R] End R M) b) =
    charpoly
      (HAdd.hAdd (α := End R M) (β := End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y) : End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
simp_rw₁₀ :
  Polynomial.map
      (MvPolynomial.eval
        (⇑((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))
      (polyCharpoly (↑φ : L →ₗ[R] End R M) b) =
    charpoly
      (HAdd.hAdd (α := End R M) (β := End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y) : End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
simp_rw₁₁ :
  charpoly.{u_2, u_4} (M := M)
      ((((↑φ : LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R M)) :
            LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R M)) :
          (a : L) → End R M)
        (r • y + x)) =
    charpoly
      (HAdd.hAdd (α := End R M) (β := End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y) : End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
simp_rw₁₂ :
  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)) =
    charpoly
      (HAdd.hAdd (α := End R M) (β := End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) (r • y) : End R M)
        (((φ : LieHom.{u_2, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
⊢ 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))

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]

Premises used: AlgHom.comp_toRingHom, RingHom.id_apply, Algebra.algebraMap_self, map_add, MvPolynomial.comp_aeval, map_mul, LieHom.coe_toLinearMap, Polynomial.aeval_C, LinearMap.polyCharpoly_map_eq_charpoly, Polynomial.coe_aeval_eq_evalRingHom, MvPolynomial.coe_aeval_eq_eval, Polynomial.aeval_X