∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {I : J → Type w}
  [inst_1 : CategoryTheory.SmallCategory J] [inst_2 : (j : J) → CategoryTheory.SmallCategory (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  [CategoryTheory.IsFiltered J] [∀ (j : J), CategoryTheory.IsFiltered (I j)]
  [∀ (j : J) (i : I j), CategoryTheory.IsFinitelyPresentable ((P j).diag.obj i)],
  CategoryTheory.IsFiltered (CategoryTheory.Limits.ColimitPresentation.Total P)