-- 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
q : A[X]
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)
have monomial : ∀ (p q : 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)
          (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) →
    (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: 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: q