-- 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))
j : J
r : R
⊢ Eq (α :=
    AddCommGrpCat.of (↑(F.obj j) : Type w') ⟶
      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'))
    (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'))
        (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)
        (((coconePointSMul F :
              RingHom.{w, w'} R
                (End
                  (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))))) :
            (a : R) → End (colimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)))
          r) :
      AddCommGrpCat.of (↑(F.obj j) : Type w') ⟶
        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'))
    (((F.obj j).smul : (a : R) → End (AddCommGrpCat.of (↑(F.obj j) : Type w'))) r ≫
        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 :
      AddCommGrpCat.of (↑(F.obj j) : Type w') ⟶
        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'))

Tactic:
simp