-- Module: Mathlib.RingTheory.Derivation.MapCoeffs
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
d : Derivation R A M
B : Type u_4
M' : Type u_5
inst_6 : CommRing B
inst_7 : Algebra R B
inst_8 : Algebra A B
inst_9 : AddCommGroup M'
inst_10 : Module B M'
inst_11 : Module R M'
inst_12 : Module A M'
d' : Derivation R B M'
f : M →ₗ[A] M'
h :
  ∀ (a : A),
    Eq.{u_5 + 1} (α := M') ((f : (a : M) → M') ((d : (a : A) → M) a : M) : M')
      ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M')
x : B
p : A[X]
add :
  ∀ (p q : A[X]),
    (d' : (a : B) → M') ((aeval x : (a : A[X]) → B) p : B) =
        HAdd.hAdd (α := M')
          ((PolynomialModule.eval x : (a : PolynomialModule B M') → M')
              (((PolynomialModule.map B f :
                      LinearMap.{u_2, u_2, u_3, u_5} (RingHom.id A) (PolynomialModule A M) (PolynomialModule B M')) :
                    (a : PolynomialModule A M) → PolynomialModule B M')
                  ((d.mapCoeffs : (a : A[X]) → PolynomialModule A M) p) :
                PolynomialModule B M') :
            M')
          (HSMul.hSMul.{u_4, u_5, u_5} (α := B) (β := M')
            ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) p : A[X]) : B) ((d' : (a : B) → M') x : M')) →
      (d' : (a : B) → M') ((aeval x : (a : A[X]) → B) q : B) =
          HAdd.hAdd (α := M')
            ((PolynomialModule.eval x : (a : PolynomialModule B M') → M')
                (((PolynomialModule.map B f :
                        LinearMap.{u_2, u_2, u_3, u_5} (RingHom.id A) (PolynomialModule A M) (PolynomialModule B M')) :
                      (a : PolynomialModule A M) → PolynomialModule B M')
                    ((d.mapCoeffs : (a : A[X]) → PolynomialModule A M) q) :
                  PolynomialModule B M') :
              M')
            (HSMul.hSMul.{u_4, u_5, u_5} (α := B) (β := M')
              ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) q : A[X]) : B)
              ((d' : (a : B) → M') x : M')) →
        (d' : (a : B) → M') ((aeval x : (a : A[X]) → B) (p + q) : B) =
          HAdd.hAdd (α := M')
            ((PolynomialModule.eval x : (a : PolynomialModule B M') → M')
                (((PolynomialModule.map B f :
                        LinearMap.{u_2, u_2, u_3, u_5} (RingHom.id A) (PolynomialModule A M) (PolynomialModule B M')) :
                      (a : PolynomialModule A M) → PolynomialModule B M')
                    ((d.mapCoeffs : (a : A[X]) → PolynomialModule A M) (p + q)) :
                  PolynomialModule B M') :
              M')
            (HSMul.hSMul.{u_4, u_5, u_5} (α := B) (β := M')
              ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (p + q) : A[X]) : B)
              ((d' : (a : B) → M') x : M'))
monomial :
  ∀ (n : ℕ) (a : A),
    (d' : (a : B) → M') ((aeval x : (a : A[X]) → B) ((Polynomial.monomial n : (a : A) → A[X]) a : A[X]) : B) =
      HAdd.hAdd (α := M')
        ((PolynomialModule.eval x : (a : PolynomialModule B M') → M')
            (((PolynomialModule.map B f :
                    LinearMap.{u_2, u_2, u_3, u_5} (RingHom.id A) (PolynomialModule A M) (PolynomialModule B M')) :
                  (a : PolynomialModule A M) → PolynomialModule B M')
                ((d.mapCoeffs : (a : A[X]) → PolynomialModule A M) ((Polynomial.monomial n : (a : A) → A[X]) a)) :
              PolynomialModule B M') :
          M')
        (HSMul.hSMul.{u_4, u_5, u_5} (α := B) (β := M')
          ((aeval x : (a : A[X]) → B)
              ((derivative : (a : A[X]) → A[X]) ((Polynomial.monomial n : (a : A) → A[X]) a) : A[X]) :
            B)
          ((d' : (a : B) → M') x : M'))
⊢ (d' : (a : B) → M') ((aeval x : (a : A[X]) → B) p : B) =
    HAdd.hAdd (α := M')
      ((PolynomialModule.eval x : (a : PolynomialModule B M') → M')
          (((PolynomialModule.map B f :
                  LinearMap.{u_2, u_2, u_3, u_5} (RingHom.id A) (PolynomialModule A M) (PolynomialModule B M')) :
                (a : PolynomialModule A M) → PolynomialModule B M')
              ((d.mapCoeffs : (a : A[X]) → PolynomialModule A M) p) :
            PolynomialModule B M') :
        M')
      (HSMul.hSMul.{u_4, u_5, u_5} (α := B) (β := M')
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) p : A[X]) : B) ((d' : (a : B) → M') x : M'))

Tactic:
induction p using Polynomial.induction_on' with
  | add => simp_all only [map_add, add_smul]; abel
  | monomial =>
    simp only [aeval_monomial, leibniz, leibniz_pow, mapCoeffs_monomial,
      PolynomialModule.map_single, PolynomialModule.eval_single, derivative_monomial, map_mul,
      _root_.map_natCast, h]
    rw [add_comm, ← smul_smul, ← smul_smul, Nat.cast_smul_eq_nsmul]

Premises used: Polynomial.derivative_monomial, Derivation.mapCoeffs_monomial, smul_smul, map_add, Polynomial.monomial, add_comm, Derivation.leibniz, map_mul, map_natCast, add_smul, Derivation.leibniz_pow, Nat.cast_smul_eq_nsmul, Polynomial.aeval_monomial, PolynomialModule.map_single, PolynomialModule.eval_single