no goals
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
t : Set X
f : Ultrafilter (OnePoint X)
⊢ ↑f ≤ 𝓝 ∞ ↔ ∀ (s : Set X), IsClosed s → IsCompact s → ¬some '' s ∈ f
simp only [le_nhds_infty, ← compl_image_coe, Ultrafilter.mem_coe,
  Ultrafilter.compl_mem_iff_not_mem]