-- 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
n : ℕ
a : A
p q : A[X]
h :
  (PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
      ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
        (HMul.hMul (α := A[X]) ((monomial n : (a : A) → A[X]) a : A[X]) p)) =
    HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial n : (a : A) → A[X]) a : A[X])
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) p) :
          PolynomialModule A M) +
      HSMul.hSMul (β := PolynomialModule A M) p
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
              ((monomial n : (a : A) → A[X]) a)) :
          PolynomialModule A M)
h_1 :
  (PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
      ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
        (HMul.hMul (α := A[X]) ((monomial n : (a : A) → A[X]) a : A[X]) q)) =
    HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial n : (a : A) → A[X]) a : A[X])
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) q) :
          PolynomialModule A M) +
      HSMul.hSMul (β := PolynomialModule A M) q
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
              ((monomial n : (a : A) → A[X]) a)) :
          PolynomialModule A M)
⊢ (PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
      ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
        (HMul.hMul (α := A[X]) ((monomial n : (a : A) → A[X]) a : A[X]) (p + q))) =
    HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial n : (a : A) → A[X]) a : A[X])
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) (p + q)) :
          PolynomialModule A M) +
      HSMul.hSMul (β := PolynomialModule A M) (p + q)
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
              ((monomial n : (a : A) → A[X]) a)) :
          PolynomialModule A M)

Tactic:
simp only [mul_add, map_add, add_smul, smul_add, add_add_add_comm, *]

Premises used: map_add, add_smul, mul_add, add_add_add_comm, smul_add