no goals
α : Type u
β : Type v
inst✝ : UniformSpace α
s : Set α
⊢ (∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x, x ∈ s ∧ ↑l ≤ 𝓝 x) ↔
    ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x, x ∈ s ∧ ↑l ≤ 𝓝 x
simp only [le_principal_iff, Ultrafilter.mem_coe]