-- 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
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
n : ℕ
a : A
monomial :
  HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
        (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) =
    HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HSMul.hSMul (β := M')
        (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((↑n : B) : B) * x ^ (n - 1))
        ((d' : (a : B) → M') x : M')
monomial₁ :
  HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
        (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) =
    HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((↑n : B) : B) •
        HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')
monomial₂ :
  HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
        (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) =
    HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
        (HSMul.hSMul.{u_4, u_5, u_5} (α := B) (↑n : B)
          (HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')))
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
        (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) +
      HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') =
    HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
      HSMul.hSMul (β := M')
        (HMul.hMul (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((↑n : B) : B) * x ^ (n - 1))
        ((d' : (a : B) → M') x : M')
have monomial₃ : HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
    HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
      (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M')) =
  HSMul.hSMul (β := M') (x ^ n) ((d' : (a : B) → M') ((algebraMap A B : (a : A) → B) a : B) : M') +
    HSMul.hSMul.{u_4, u_5, u_5} (α := B) ((algebraMap A B : (a : A) → B) a : B)
      (n • HSMul.hSMul (β := M') (x ^ (n - 1)) ((d' : (a : B) → M') x : M'))
Tactic: rw [add_comm, ← smul_smul, ← smul_smul, Nat.cast_smul_eq_nsmul]