∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w} [inst_3 : CategoryTheory.SmallCategory J]
  (F : CategoryTheory.Functor J (CategoryTheory.MonoOver X)) [CategoryTheory.IsFiltered J]
  {c : CategoryTheory.Limits.Cocone (F.comp ((CategoryTheory.MonoOver.forget X).comp (CategoryTheory.Over.forget X)))}
  (hc : CategoryTheory.Limits.IsColimit c) (f : c.pt ⟶ X),
  (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) f = (F.obj j).obj.hom) → CategoryTheory.Mono f