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
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
j i : J
f : i ⟶ j
h : eventualRange F j = range (F.map f)
⊢ _root_.Nonempty ((toEventualRanges F).obj j)
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
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
j : J
⊢ _root_.Nonempty ((toEventualRanges F).obj j)
let ⟨i, f, h⟩ := F.isMittagLeffler_iff_eventualRange.1 h j
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
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
j i : J
f : i ⟶ j
h : eventualRange F j = range (F.map f)
⊢ _root_.Nonempty ↑(range (F.map f))
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
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
j i : J
f : i ⟶ j
h : eventualRange F j = range (F.map f)
⊢ _root_.Nonempty ((toEventualRanges F).obj j)
rw [toEventualRanges_obj, h]
no goals
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
inst✝ : ∀ (j : J), _root_.Nonempty (F.obj j)
j i : J
f : i ⟶ j
h : eventualRange F j = range (F.map f)
⊢ _root_.Nonempty ↑(range (F.map f))
infer_instance