∀ {R : Type u_4} {S : Type u_5} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {J : Type u_2}
  [inst_2 : CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J (ModuleCat S))
  [CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat S) AddCommGrpCat))],
  CategoryTheory.Limits.HasColimit
    ((F.comp (ModuleCat.restrictScalars f)).comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))