no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.60670
inst✝ : UniformSpace α
x : α
t : Set α
⊢ t ∈ 𝓝 x ↔ ∃ i, (i ∈ 𝓤 α ∧ SymmetricRel i) ∧ ball x i ⊆ t
simp [UniformSpace.mem_nhds_iff_symm, and_assoc]