∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type v} [inst_1 : CategoryTheory.SmallCategory I]
  [CategoryTheory.IsFiltered I] {J : Type} [inst_3 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor I C)),
  (∀ (i : I),
      CategoryTheory.Limits.IsIndObject (CategoryTheory.Limits.limit ((F.flip.obj i).comp CategoryTheory.yoneda))) →
    CategoryTheory.Limits.IsIndObject
      (CategoryTheory.Limits.limit
        (F.comp
          (((CategoryTheory.Functor.whiskeringRight I C (CategoryTheory.Functor Cᵒᵖ (Type v))).obj
                CategoryTheory.yoneda).comp
            CategoryTheory.Limits.colim)))