no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.62335
inst✝ : UniformSpace α
s : Set α
x : α
⊢ x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SymmetricRel V → Set.Nonempty (s ∩ ball x V)
simp [mem_closure_iff_nhds_basis (hasBasis_nhds x), Set.Nonempty]