-- Module: Mathlib.Algebra.Category.ModuleCat.Colimits
Goal:
R : Type w
inst : Ring R
J : Type u
inst_1 : Category.{v, u} J
F : J ⥤ ModuleCat.{w', w} R
inst_2 :
  HasColimit
    (F ⋙
      forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦ (↑x1 : Type w') →ₗ[R] (↑x2 : Type w'))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w'))
        (CD := AddCommGrpCat.carrier))
s : Cocone F
r : R
j : J
w :
  Eq (α := AddCommGrpCat.of (↑(F.obj j) : Type w') ⟶ AddCommGrpCat.of (↑s.pt : Type w'))
    (CategoryStruct.comp (Y := AddCommGrpCat.of (↑s.pt : Type w'))
      (AddCommGrpCat.ofHom (↑(Hom.hom (s.ι.app j)) : (↑(F.obj j) : Type w') →+ (↑s.pt : Type w')))
      ((s.pt.smul : (a : R) → End (AddCommGrpCat.of (↑s.pt : Type w'))) r))
    (CategoryStruct.comp (Y := AddCommGrpCat.of (↑(F.obj j) : Type w'))
      (((F.obj j).smul : (a : R) → End (AddCommGrpCat.of (↑(F.obj j) : Type w'))) r)
      (AddCommGrpCat.ofHom (↑(Hom.hom (s.ι.app j)) : (↑(F.obj j) : Type w') →+ (↑s.pt : Type w'))))
⊢ Eq (α := AddCommGrpCat.of (↑(F.obj j) : Type w') ⟶ AddCommGrpCat.of (↑s.pt : Type w'))
    (CategoryStruct.comp (Y := AddCommGrpCat.of (↑s.pt : Type w'))
      (AddCommGrpCat.ofHom (↑(Hom.hom (s.ι.app j)) : (↑(F.obj j) : Type w') →+ (↑s.pt : Type w')))
      ((s.pt.smul : (a : R) → End (AddCommGrpCat.of (↑s.pt : Type w'))) r))
    (CategoryStruct.comp (Y :=
      colimit
        (F ⋙
          forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
            (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
            fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier)))
      (colimit.ι
        (F ⋙
          forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
            (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
            fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
        j)
      (CategoryStruct.comp (Y :=
        AddCommGrpCat.of
          (↑(mkOfSMul' (A :=
                colimit
                  (F ⋙
                    forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
                      (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
                      fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD :=
                      AddCommGrpCat.carrier)))
                (coconePointSMul F)) :
            Type w'))
        (colimMap
          { app := fun (j : J) ↦ ((F.obj j).smul : (a : R) → End (AddCommGrpCat.of (↑(F.obj j) : Type w'))) r,
            naturality := ⋯ })
        (colimit.desc
          (F ⋙
            forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
              (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
              fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
          (Functor.mapCocone
            (forget₂ (ModuleCat.{w', w} R) (FC := fun (x1 x2 : ModuleCat.{w', w} R) ↦
              (↑x1 : Type w') →ₗ[R] (↑x2 : Type w')) (CC := carrier) AddCommGrpCat (FD :=
              fun (x1 x2 : AddCommGrpCat.{w'}) ↦ (↑x1 : Type w') →+ (↑x2 : Type w')) (CD := AddCommGrpCat.carrier))
            s))))

Tactic:
simp only [ι_colimMap_assoc, Functor.comp_obj, forget₂_obj, colimit.ι_desc,
      Functor.mapCocone_pt, Functor.mapCocone_ι_app, forget₂_map]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.mapCocone_ι_app, CategoryTheory.Limits.ι_colimMap_assoc, ModuleCat.forget₂_obj, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Functor.mapCocone_pt, ModuleCat.forget₂_map