-- 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))
r s : R
j : J
⊢ 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)
      (colimMap
        {
          app := fun (j : J) ↦
            ((F.obj j).smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj (F.obj j))) (r + s),
          naturality := ⋯ }) =
    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 ≫
      HAdd.hAdd (α :=
        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))))
        (colimMap
          {
            app := fun (j : J) ↦
              ((F.obj j).smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj (F.obj j))) r,
            naturality := ⋯ :
            NatTrans
              (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))
              (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)) })
        (colimMap
          {
            app := fun (j : J) ↦
              ((F.obj j).smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj (F.obj j))) s,
            naturality := ⋯ :
            NatTrans
              (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))
              (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)) })
have simp : HAdd.hAdd (α := End (AddCommGrpCat.of (↑(F.obj j) : Type w'))) (β := End (AddCommGrpCat.of (↑(F.obj j) : Type w')))
      (((F.obj j).smul : (a : R) → End (AddCommGrpCat.of (↑(F.obj j) : Type w'))) r :
        End (AddCommGrpCat.of (↑(F.obj j) : Type w')))
      (((F.obj j).smul : (a : R) → End (AddCommGrpCat.of (↑(F.obj j) : Type w'))) s :
        End (AddCommGrpCat.of (↑(F.obj j) : 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 =
  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 ≫
    HAdd.hAdd (α :=
      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))))
      (colimMap
        { app := fun (j : J) ↦ ((F.obj j).smul : (a : R) → End (AddCommGrpCat.of (↑(F.obj j) : Type w'))) r,
          naturality := sorry :
          NatTrans
            (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))
            (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)) })
      (colimMap
        { app := fun (j : J) ↦ ((F.obj j).smul : (a : R) → End (AddCommGrpCat.of (↑(F.obj j) : Type w'))) s,
          naturality := sorry :
          NatTrans
            (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))
            (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)) })
Tactic: simp +instances only [Functor.comp_obj, forget₂_obj, map_add, ι_colimMap]