no goals
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
a : α
⊢ a ∈ closure s ↔ ∀ (t : Set α), t ∈ 𝓝 a → ∃ y, ↑y ∈ t
simp only [mem_closure_iff_nhds, Set.inter_nonempty_iff_exists_right, SetCoe.exists, exists_prop]