case intro
ι : Type ?u.364441
ι' : Type ?u.364444
α : Type u_1
β : Type ?u.364450
γ : Type ?u.364453
f : Filter α
inst✝¹ : IsCountablyGenerated f
inst✝ : NeBot f
B : ℕ → Set α
h : HasAntitoneBasis f B
⊢ ∃ x, Tendsto x atTop f
ι : Type ?u.364441
ι' : Type ?u.364444
α : Type u_1
β : Type ?u.364450
γ : Type ?u.364453
f : Filter α
inst✝¹ : IsCountablyGenerated f
inst✝ : NeBot f
⊢ ∃ x, Tendsto x atTop f
obtain ⟨B, h⟩ := f.exists_antitone_basis
case intro
ι : Type ?u.364441
ι' : Type ?u.364444
α : Type u_1
β : Type ?u.364450
γ : Type ?u.364453
f : Filter α
inst✝¹ : IsCountablyGenerated f
inst✝ : NeBot f
B : ℕ → Set α
h : HasAntitoneBasis f B
x : ℕ → α
hx : ∀ (n : ℕ), x n ∈ B n
⊢ ∃ x, Tendsto x atTop f
case intro
ι : Type ?u.364441
ι' : Type ?u.364444
α : Type u_1
β : Type ?u.364450
γ : Type ?u.364453
f : Filter α
inst✝¹ : IsCountablyGenerated f
inst✝ : NeBot f
B : ℕ → Set α
h : HasAntitoneBasis f B
⊢ ∃ x, Tendsto x atTop f
choose x hx using fun n => Filter.nonempty_of_mem (h.mem n)
no goals
case intro
ι : Type ?u.364441
ι' : Type ?u.364444
α : Type u_1
β : Type ?u.364450
γ : Type ?u.364453
f : Filter α
inst✝¹ : IsCountablyGenerated f
inst✝ : NeBot f
B : ℕ → Set α
h : HasAntitoneBasis f B
x : ℕ → α
hx : ∀ (n : ℕ), x n ∈ B n
⊢ ∃ x, Tendsto x atTop f
exact ⟨x, h.tendsto hx⟩