∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {I : Type u_2} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S X : C} (πX : X ⟶ S)
  [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C],
  CategoryTheory.Limits.HasColimit
    (CategoryTheory.Discrete.functor (CategoryTheory.SmallObject.functorObjSrcFamily f πX))