no goals
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
A : Set α
x : α
⊢ x ∈ closure A ↔ NeBot (comap Subtype.val (𝓝 x))
simp_rw [mem_closure_iff_nhds, comap_neBot_iff, Set.inter_nonempty_iff_exists_right,
  SetCoe.exists, exists_prop]