no goals
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
a b : α
⊢ (a, b) ∈ 𝓢 α ↔ a ⤳ b
simp only [(𝓤 α).basis_sets.mem_separationRel, id, mem_setOf_eq,
  (nhds_basis_uniformity (𝓤 α).basis_sets).specializes_iff]