no goals
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i j k : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
⊢ IsMittagLeffler F ↔ ∀ (j : J), ∃ i f, ∀ ⦃k : J⦄ (g : k ⟶ i), range (F.map f) ⊆ range (F.map (g ≫ f))
simp_rw [isMittagLeffler_iff_eventualRange, eventualRange_eq_iff]