-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
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)
⊢ (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)
have 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]) ((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)
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]
Cleared hypotheses: p