no goals
α : Type u
β : Type v
inst✝ : TopologicalSpace α
⊢ (∀ {x y : α}, NeBot (𝓝 x ⊓ 𝓝 y) → x = y) ↔ ∀ {x y : α} (f : Ultrafilter α), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y
simp only [← exists_ultrafilter_iff, and_imp, le_inf_iff, exists_imp]