-- 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
p q : A[X]
add :
  ∀ (p q_1 : 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)) =
        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) 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) p) :
              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) (q_1 * q)) =
          HSMul.hSMul (β := PolynomialModule A M) q_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) 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) q_1) :
                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) ((p + q_1) * q)) =
          HSMul.hSMul (β := PolynomialModule A M) (p + q_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) 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) (p + q_1)) :
                PolynomialModule A M)
monomial :
  ∀ (n : ℕ) (a : A),
    (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]) ((Polynomial.monomial n : (a : A) → A[X]) a : A[X]) q)) =
      HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((Polynomial.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)
                ((Polynomial.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) (p * q)) =
    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) 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) p) :
          PolynomialModule A M)

Tactic:
induction p using Polynomial.induction_on' with
    | add => simp only [add_mul, map_add, add_smul, smul_add, add_add_add_comm, *]
    | monomial n a =>
      induction q using Polynomial.induction_on' with
      | add => simp only [mul_add, map_add, add_smul, smul_add, add_add_add_comm, *]
      | monomial m b =>
        refine Finsupp.ext fun i ↦ ?_
        dsimp [PolynomialModule.equivPolynomial, PolynomialModule.map]
        simp only [toFinsupp_mul, toFinsupp_monomial, AddMonoidAlgebra.single_mul_single]
        change d _ = _ + _
        -- TODO: copy more `Finsupp` API to `PolynomialModule`.
        -- We have to do a bit of work to go through the identification
        -- `PolynomialModule A M = ℕ →₀ M`...
        dsimp only [PolynomialModule, Finsupp.mapRange.linearMap_apply, coeFn_coe]
        rw [Finsupp.mapRange_single, Finsupp.mapRange_single]
        -- ... and here we go back through the identification.
        change _ = (_ • PolynomialModule.single A _ _) _ + (_ • PolynomialModule.single A _ _) i
        simp only [PolynomialModule.monomial_smul_single, AddMonoidAlgebra.single_apply,
          apply_ite d, leibniz, map_zero, PolynomialModule.single_apply, ite_add_zero,
          add_comm m n]

Premises used: add_mul, Finsupp.ext, Polynomial.toFinsupp_monomial, AddMonoidAlgebra.single_apply, PolynomialModule.monomial_smul_single, ite_add_zero, PolynomialModule.equivPolynomial, PolynomialModule.map, PolynomialModule.single_apply, apply_ite, map_zero, PolynomialModule.single, map_add, Polynomial.monomial, Finsupp.mapRange.linearMap_apply, Derivation.leibniz, PolynomialModule, Polynomial.toFinsupp_mul, Derivation.coeFn_coe, add_smul, AddMonoidAlgebra.single_mul_single, HSMul.hSMul, mul_add, add_add_add_comm, DFunLike.coe, Finsupp.mapRange_single, smul_add