∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{u_3, u_1, u_2} C] {X : C} {J : Type u_3}
  [inst_3 : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (CategoryTheory.MonoOver X))
  [inst_4 : CategoryTheory.IsFiltered J] (j : J),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Limits.colimit.cocone
              (F.comp ((CategoryTheory.MonoOver.forget X).comp (CategoryTheory.Over.forget X)))).ι.app
        j)
      (CategoryTheory.Limits.colimit.desc
        (F.comp ((CategoryTheory.MonoOver.forget X).comp (CategoryTheory.Over.forget X)))
        { pt := X, ι := { app := fun j => (F.obj j).obj.hom, naturality := ⋯ } }) =
    (F.obj j).obj.hom