no goals
α : Type u
β : Type v
X : Type ?u.158749
ι : Type ?u.158752
inst✝ : PseudoMetricSpace α
⊢ 𝓤 α = ⨅ (ε : ℝ≥0∞) (_ : ε > 0), 𝓟 {p | edist p.fst p.snd < ε}
simp only [PseudoMetricSpace.uniformity_dist, dist_nndist, edist_nndist,
  Metric.uniformity_edist_aux]