-- 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 :=
        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 (↑s.pt : Type w'))
          (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) :
            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)) ⟶
              Cocone.pt (F :=
                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))
          ((s.pt.smul : (a : R) → End (AddCommGrpCat.of (↑s.pt : Type w'))) r)) :
      AddCommGrpCat.of (↑(F.obj j) : Type w') ⟶ AddCommGrpCat.of (↑s.pt : Type w'))
    (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'))
          (((colimitCocone F).pt.smul : (a : R) → End (AddCommGrpCat.of (↑(mkOfSMul' (coconePointSMul F)) : Type w')))
            r)
          (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))) :
      AddCommGrpCat.of (↑(F.obj j) : Type w') ⟶ AddCommGrpCat.of (↑s.pt : Type w'))
⊢ Eq (α :=
    Functor.obj
        (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 ⟶
      Functor.obj
        (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.pt)
    (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 :=
          Functor.obj
            (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.pt)
          (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) :
            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)) ⟶
              Cocone.pt (F :=
                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))
          ((s.pt.smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj s.pt)) r)) :
      Functor.obj
          (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 ⟶
        Functor.obj
          (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.pt)
    (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 :=
          Functor.obj
            (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))
            (colimitCocone F).pt)
          (((colimitCocone F).pt.smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj (colimitCocone F).pt))
            r)
          (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))) :
      Functor.obj
          (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 ⟶
        Functor.obj
          (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.pt)

Tactic:
dsimp