α : Type u
β : Type v
γ : Type w
δ : Type ?u.174506
ι : Sort x
r : α → β → Prop
l : Filter α
inst✝ : NeBot l
h : ∀ᶠ (x : α) in l, ∃ y, r x y
this : Nonempty β
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.174506
ι : Sort x
r : α → β → Prop
l : Filter α
inst✝ : NeBot l
h : ∀ᶠ (x : α) in l, ∃ y, r x y
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)
haveI : Nonempty β := let ⟨_, hx⟩ := h.exists; hx.nonempty
α : Type u
β : Type v
γ : Type w
δ : Type ?u.174506
ι : Sort x
r : α → β → Prop
l : Filter α
inst✝ : NeBot l
h : ∀ᶠ (x : α) in l, ∃ y, r x y
this : Nonempty β
f : α → β
hf : ∀ (x : α), (∃ y, r x y) → r x (f x)
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)
α : Type u
β : Type v
γ : Type w
δ : Type ?u.174506
ι : Sort x
r : α → β → Prop
l : Filter α
inst✝ : NeBot l
h : ∀ᶠ (x : α) in l, ∃ y, r x y
this : Nonempty β
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)
choose! f hf using fun x (hx : ∃ y, r x y) => hx
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.174506
ι : Sort x
r : α → β → Prop
l : Filter α
inst✝ : NeBot l
h : ∀ᶠ (x : α) in l, ∃ y, r x y
this : Nonempty β
f : α → β
hf : ∀ (x : α), (∃ y, r x y) → r x (f x)
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)
exact ⟨f, h.mono hf⟩