-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddZeroClass M
f : S →+* R
g : MonoidHom.{u_4, u_2} (Multiplicative M) R
c : S
φ : S[M]
m : M
x : S
hfg :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M])
            ((singleAddHom m : (a : S) → S[M]) x) :
          S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
            ((singleAddHom m : (a : S) → S[M]) x : S[M]) :
          R) :
      R)
hfg₁ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M]) (single m x) : S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
hfg₂ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
        (HSMul.hSMul (β := S[M]) c (single m x)) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
hfg₃ :
  (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (HSMul.hSMul (β := S[M]) c (single m x)) =
    HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m x) : R)
hfg₄ :
  (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m (c * x)) =
    HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m x) : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c))
                (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
have hfg₅ : HMul.hMul (α := R) (β := R) (((↑f : S →+ R) : (a : S) → R) (c * x) : R)
    ((g : (a : Multiplicative M) → R) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M) : R) =
  HMul.hMul (α := R) ((f : (a : S) → R) c : R)
    (HMul.hMul (α := R) (β := R) (((↑f : S →+ R) : (a : S) → R) x : R)
      ((g : (a : Multiplicative M) → R) ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M) : R))
Tactic: simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
    AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]