-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Colimits (goal)
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
j : J
⊢ (colimitCocone F).ι.app j ≫
      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))
        ⋯ =
    s.ι.app j
have a : 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))
      (F.obj 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)
  (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))
    ((colimitCocone F).ι.app j ≫
      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))
        sorry))
  (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))
    (s.ι.app j))
Tactic: apply (forget₂ _ AddCommGrpCat).map_injective