-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Stalk (goal)
Goal:
C : Type u_1
inst : SmallCategory C
inst_1 : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst_2 : (i : C) → Module (↑(R.obj i) : Type (max u_1 u_2)) (↑(M.obj i) : Type (max u_1 u_3))
H :
  ∀ {i j : C} (f : i ⟶ j) (r : (↑(R.obj i) : Type (max u_1 u_2))) (m : (↑(M.obj i) : Type (max u_1 u_3))),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u_1 u_3)) →+ (↑x2 : Type (max u_1 u_3)))
            (CC := AddCommGrpCat.carrier) (M.map f) :
          (a : (↑(M.obj i) : Type (max u_1 u_3))) → (↑(M.obj j) : Type (max u_1 u_3)))
        (r • m) =
      HSMul.hSMul (α := (↑(R.obj j) : Type (max u_1 u_2))) (β := (↑(M.obj j) : Type (max u_1 u_3)))
        ((ConcreteCategory.hom (FC := fun (R S : RingCat) ↦ (↑R : Type (max u_1 u_2)) →+* (↑S : Type (max u_1 u_2)))
                (CC := RingCat.carrier) (R.map f) :
              (a : (↑(R.obj i) : Type (max u_1 u_2))) → (↑(R.obj j) : Type (max u_1 u_2)))
            r :
          (↑(R.obj j) : Type (max u_1 u_2)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦
                (↑x1 : Type (max u_1 u_3)) →+ (↑x2 : Type (max u_1 u_3))) (CC := AddCommGrpCat.carrier) (M.map f) :
              (a : (↑(M.obj i) : Type (max u_1 u_3))) → (↑(M.obj j) : Type (max u_1 u_3)))
            m :
          (↑(M.obj j) : Type (max u_1 u_3)))
cR : Cocone R
hcR : IsColimit cR
cM : Cocone M
hcM : IsColimit cM
i : C
r : (↑(R.obj i) : Type (max u_1 u_2))
m : (↑(M.obj i) : Type (max u_1 u_3))
this : Module (↑(RingCat.FilteredColimits.colimit.{u_1, u_2} R) : Type (max u_1 u_2))
  (↑(AddCommGrpCat.FilteredColimits.colimit.{u_1, u_3} M) : Type (max u_1 u_3)) :=
  filteredColimitsModule R M ⋯
α : cM.pt ≅ (AddCommGrpCat.FilteredColimits.colimitCocone.{u_1, u_3} M).pt :=
  hcM.coconePointUniqueUpToIso (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)
β : cR.pt ≅ (RingCat.FilteredColimits.colimitCocone.{u_1, u_2} R).pt :=
  hcR.coconePointUniqueUpToIso (RingCat.FilteredColimits.colimitCoconeIsColimit R)
⊢ (α.addCommGroupIsoToAddEquiv :
        (a : (↑cM.pt : Type (max u_1 u_3))) →
          (↑(AddCommGrpCat.FilteredColimits.colimitCocone M).pt : Type (max u_1 u_3)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦
            (↑x1 : Type (max u_1 u_3)) →+ (↑x2 : Type (max u_1 u_3))) (CC := AddCommGrpCat.carrier) (cM.ι.app i) :
          (a : (↑(M.obj i) : Type (max u_1 u_3))) → (↑(((Functor.const C).obj cM.pt).obj i) : Type (max u_1 u_3)))
        (r • m)) =
    HSMul.hSMul (α := (↑(RingCat.FilteredColimits.colimit.{u_1, u_2} R) : Type (max u_1 u_2))) (β :=
      (↑(AddCommGrpCat.FilteredColimits.colimit.{u_1, u_3} M) : Type (max u_1 u_3)))
      (((↑(RingHom.toMonoidWithZeroHom
                  (RingEquiv.toRingHom
                    (Iso.ringCatIsoToRingEquiv
                      (hcR.coconePointUniqueUpToIso (RingCat.FilteredColimits.colimitCoconeIsColimit R))))) :
              ZeroHom (↑cR.pt : Type (max u_1 u_2)) (↑(RingCat.FilteredColimits.colimit R) : Type (max u_1 u_2))) :
            (a : (↑cR.pt : Type (max u_1 u_2))) → (↑(RingCat.FilteredColimits.colimit R) : Type (max u_1 u_2)))
          ((ConcreteCategory.hom (FC := fun (R S : RingCat) ↦ (↑R : Type (max u_1 u_2)) →+* (↑S : Type (max u_1 u_2)))
                (CC := RingCat.carrier) (cR.ι.app i) :
              (a : (↑(R.obj i) : Type (max u_1 u_2))) → (↑(((Functor.const C).obj cR.pt).obj i) : Type (max u_1 u_2)))
            r) :
        (↑(RingCat.FilteredColimits.colimit.{u_1, u_2} R) : Type (max u_1 u_2)))
      ((AddEquiv.toEquiv
              (Iso.addCommGroupIsoToAddEquiv
                (hcM.coconePointUniqueUpToIso (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M))) :
            (a : (↑cM.pt : Type (max u_1 u_3))) → (↑(AddCommGrpCat.FilteredColimits.colimit M) : Type (max u_1 u_3)))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦
                (↑x1 : Type (max u_1 u_3)) →+ (↑x2 : Type (max u_1 u_3))) (CC := AddCommGrpCat.carrier) (cM.ι.app i) :
              (a : (↑(M.obj i) : Type (max u_1 u_3))) → (↑(((Functor.const C).obj cM.pt).obj i) : Type (max u_1 u_3)))
            m) :
        (↑(AddCommGrpCat.FilteredColimits.colimit.{u_1, u_3} M) : Type (max u_1 u_3)))
have change : (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u_1 u_3)) →+ (↑x2 : Type (max u_1 u_3)))
        (CC := AddCommGrpCat.carrier) (cM.ι.app i ≫ α.hom) :
      (a : (↑(M.obj i) : Type (max u_1 u_3))) →
        (↑(AddCommGrpCat.FilteredColimits.colimitCocone M).pt : Type (max u_1 u_3)))
    (r • m) =
  HSMul.hSMul (α := (↑(RingCat.FilteredColimits.colimit.{u_1, u_2} R) : Type (max u_1 u_2))) (β :=
    (↑(AddCommGrpCat.FilteredColimits.colimit.{u_1, u_3} M) : Type (max u_1 u_3)))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat) ↦ (↑R : Type (max u_1 u_2)) →+* (↑S : Type (max u_1 u_2))) (CC :=
            RingCat.carrier) (cR.ι.app i ≫ β.hom) :
          (a : (↑(R.obj i) : Type (max u_1 u_2))) →
            (↑(RingCat.FilteredColimits.colimitCocone R).pt : Type (max u_1 u_2)))
        r :
      (↑(RingCat.FilteredColimits.colimitCocone.{u_1, u_2} R).pt : Type (max u_1 u_2)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦
            (↑x1 : Type (max u_1 u_3)) →+ (↑x2 : Type (max u_1 u_3))) (CC := AddCommGrpCat.carrier)
            (cM.ι.app i ≫ α.hom) :
          (a : (↑(M.obj i) : Type (max u_1 u_3))) →
            (↑(AddCommGrpCat.FilteredColimits.colimitCocone M).pt : Type (max u_1 u_3)))
        m :
      (↑(AddCommGrpCat.FilteredColimits.colimitCocone.{u_1, u_3} M).pt : Type (max u_1 u_3)))
Tactic: change (cM.ι.app i ≫ α.hom) _ = (HSMul.hSMul (α := RingCat.FilteredColimits.colimit R)
    (β := AddCommGrpCat.FilteredColimits.colimit M)
    ((cR.ι.app i ≫ β.hom) r) ((cM.ι.app i ≫ α.hom) m))