∀ {α : Type u_1} {β : Type u_2} (f : α → β) (m : PseudoEMetricSpace β),
  Filter.comap (Prod.map f f) (uniformity β) =
    ⨅ i, ⨅ (_ : 0 < i), Filter.principal (Prod.map f f ⁻¹' {p | edist p.1 p.2 < i})