no goals
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝 a = ⨅ (s : Set α) (_ : IsOpen s) (_ : a ∈ s), 𝓟 s
simp only [nhds_def, mem_setOf_eq, @and_comm (a ∈ _), iInf_and]