-- Module: Mathlib.Algebra.Category.ModuleCat.Stalk
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_1 :
  ∀ {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 ⋯
α_1 : 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)
s : C
α : IsFiltered.max i i ⟶ s
H : leftToMax i i ≫ α = rightToMax i i ≫ α
⊢ Eq (α :=
    ToType (FC := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC :=
      AddMonCat.carrier)
      (Functor.obj
        (forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1)))
          (CC := AddGrpCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
          (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD := AddMonCat.carrier))
        (Functor.obj
          (forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
            (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier) AddGrpCat (FD :=
            fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
            AddGrpCat.carrier))
          (M.obj s))))
    ((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 (leftToMax i i ≫ α)) :
          (a : (↑(M.obj i) : Type (max u_1 u_3))) → (↑(M.obj s) : Type (max u_1 u_3)))
        (r • m) :
      (↑(M.obj s) : 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 α) :
          (a : (↑(M.obj (IsFiltered.max i i)) : Type (max u_1 u_3))) → (↑(M.obj s) : Type (max u_1 u_3)))
        (HSMul.hSMul (α := (↑(R.obj (IsFiltered.max i i)) : Type (max u_1 u_2))) (β :=
          (↑(M.obj (IsFiltered.max i i)) : 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) (Y := R.obj (IsFiltered.max i i)) (R.map (leftToMax i i)) :
                (a : (↑(R.obj i) : Type (max u_1 u_2))) → (↑(R.obj (IsFiltered.max i i)) : Type (max u_1 u_2)))
              r :
            (↑(R.obj (IsFiltered.max i i)) : 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) (Y :=
                  M.obj (IsFiltered.max i i)) (M.map (rightToMax i i)) :
                (a : (↑(M.obj i) : Type (max u_1 u_3))) → (↑(M.obj (IsFiltered.max i i)) : Type (max u_1 u_3)))
              m :
            (↑(M.obj (IsFiltered.max i i)) : Type (max u_1 u_3)))) :
      (↑(M.obj s) : Type (max u_1 u_3)))

Tactic:
simp only [← ConcreteCategory.comp_apply, ← Functor.map_comp, *]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.Functor.map_comp