-- 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
m : (colimitCocone F).pt ⟶ s.pt
hm : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
a :
  ∀ (j : J),
    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)
        (CategoryTheory.Functor.map
          (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))
          m))
      (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)
        (CategoryTheory.Functor.map
          (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))
          (homMk
            (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))
            ⋯)))
⊢ Eq (α :=
    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 ⟶
      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)
    (CategoryTheory.Functor.map
      (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))
      m)
    (CategoryTheory.Functor.map
      (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))
      (homMk
        (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:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext