-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M'_1 : PresheafOfModules R
cM'_1 : Cocone M'_1.presheaf
hcM'_1 : IsColimit cM'_1
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
U : Cᵒᵖ
r : (↑(R.obj U) : Type w)
m : (↑(M.obj U) : Type w)
c : Cocone ((toPresheaf R).obj M) := (Cocone.precompose ((toPresheaf R).map f)).obj cM'
h₁ :
  Eq (α := (↑cM'.pt : Type w))
    ((AddMonoidHom.comp (AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM')))
            (AddCommGrpCat.Hom.hom (cM.ι.app U)) :
          (a : (↑(M.obj U) : Type w)) → (↑cM'.pt : Type w))
        (r • m) :
      (↑cM'.pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (((toPresheaf R).map f).app U ≫ cM'.ι.app U) :
          (a : (↑(M.obj U) : Type w)) → (↑cM'.pt : Type w))
        (r • m) :
      (↑cM'.pt : Type w))
h₂ :
  Eq (α := (↑cM'.pt : Type w))
    ((AddMonoidHom.comp (AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM')))
            (AddCommGrpCat.Hom.hom (cM.ι.app U)) :
          (a : (↑(M.obj U) : Type w)) → (↑cM'.pt : Type w))
        m :
      (↑cM'.pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (((toPresheaf R).map f).app U ≫ cM'.ι.app U) :
          (a : (↑(M.obj U) : Type w)) → (↑cM'.pt : Type w))
        m :
      (↑cM'.pt : Type w))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
          AddCommGrpCat.carrier) (Y := cM'.pt)
          (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM') :
            cM.pt ⟶ ((Cocone.precompose ((toPresheaf R).map f)).obj cM').pt) :
        (a : (↑cM.pt : Type w)) → (↑cM'.pt : Type w))
      (HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r : (↑cR.pt : Type w))
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM)) =
    HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM')
      ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r : (↑cR.pt : Type w))
      (((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                AddCommGrpCat.carrier) (Y := cM'.pt)
                (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM') :
                  cM.pt ⟶ ((Cocone.precompose ((toPresheaf R).map f)).obj cM').pt) :
              (↑cM.pt : Type w) →+ (↑cM'.pt : Type w)) :
            (a : (↑cM.pt : Type w)) → (↑cM'.pt : Type w))
          ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) :
        (↑cM'.pt : Type w))
have rw : ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
          AddCommGrpCat.carrier) (Y := cM'.pt)
          (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM') :
            cM.pt ⟶ ((Cocone.precompose ((toPresheaf R).map f)).obj cM').pt) :
        (↑cM.pt : Type w) →+ (↑cM'.pt : Type w)) :
      (a : (↑cM.pt : Type w)) → (↑cM'.pt : Type w))
    ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) (r • m) : ModuleColimit hcR hcM) =
  HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM')
    ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r : (↑cR.pt : Type w))
    (((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier) (Y := cM'.pt)
              (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM') :
                cM.pt ⟶ ((Cocone.precompose ((toPresheaf R).map f)).obj cM').pt) :
            (↑cM.pt : Type w) →+ (↑cM'.pt : Type w)) :
          (a : (↑cM.pt : Type w)) → (↑cM'.pt : Type w))
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) :
      (↑cM'.pt : Type w))
Tactic: rw [ModuleColimit.smul_eq]