case intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i✝ j✝ k : J
s : Set (F.obj i✝)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
i j : J
f : i ⟶ j
x✝ : (toEventualRanges F).obj j
y : F.obj i
hy : y ∈ eventualRange F i
hx : F.map f y ∈ eventualRange F j
⊢ ∃ a, (toEventualRanges F).map f a = { val := F.map f y, property := hx }
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i✝ j✝ k : J
s : Set (F.obj i✝)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
i j : J
f : i ⟶ j
x✝ : (toEventualRanges F).obj j
x : F.obj j
hx : x ∈ eventualRange F j
⊢ ∃ a, (toEventualRanges F).map f a = { val := x, property := hx }
obtain ⟨y, hy, rfl⟩ := h.subset_image_eventualRange F f hx
no goals
case intro.intro
J : Type u
inst✝¹ : Category J
F : J ⥤ Type v
i✝ j✝ k : J
s : Set (F.obj i✝)
inst✝ : IsCofilteredOrEmpty J
h : IsMittagLeffler F
i j : J
f : i ⟶ j
x✝ : (toEventualRanges F).obj j
y : F.obj i
hy : y ∈ eventualRange F i
hx : F.map f y ∈ eventualRange F j
⊢ ∃ a, (toEventualRanges F).map f a = { val := F.map f y, property := hx }
exact ⟨⟨y, hy⟩, rfl⟩