∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J}
  (s : Set (F.obj i)) [CategoryTheory.IsCofilteredOrEmpty J], F.IsMittagLeffler → (F.toPreimages s).IsMittagLeffler