refactor(UniformSpace): change the definition (#10901)

- replace `isOpen_uniformity` with `nhds_eq_comap_uniformity`
  as I suggested in #2028
- don't extend `UniformSpace.Core` so that we can drop `refl`,
  as it follows from `nhds_eq_comap_uniformity`;
- drop `UniformSpace.mk'` - can't be a `match_pattern` anymore;
- deprecate `UniformSpace.ofNhdsEqComap`.

Author: urkud

Mathlib/Topology/Algebra/UniformGroup.lean

@@ -558,7 +558,6 @@ commutative additive groups (see `comm_topologicalAddGroup_is_uniform`) and for
 additive groups (see `topologicalAddGroup_is_uniform_of_compactSpace`)."]
 def TopologicalGroup.toUniformSpace : UniformSpace G where
   uniformity := comap (fun p : G × G => p.2 / p.1) (𝓝 1)
-  refl := (Tendsto.mono_right (by simp) (pure_le_nhds _)).le_comap
   symm :=
     have : Tendsto (fun p : G × G ↦ (p.2 / p.1)⁻¹) (comap (fun p : G × G ↦ p.2 / p.1) (𝓝 1))
       (𝓝 1⁻¹) := tendsto_id.inv.comp tendsto_comap
@@ -568,8 +567,7 @@ def TopologicalGroup.toUniformSpace : UniformSpace G where
     refine mem_map.2 (mem_of_superset (mem_lift' <| preimage_mem_comap V_nhds) ?_)
     rintro ⟨x, y⟩ ⟨z, hz₁, hz₂⟩
     simpa using V_mul _ hz₂ _ hz₁
-  isOpen_uniformity S := by
-    simp only [isOpen_iff_mem_nhds, ← mem_comap_prod_mk, comap_comap, (· ∘ ·), nhds_translation_div]
+  nhds_eq_comap_uniformity _ := by simp only [comap_comap, (· ∘ ·), nhds_translation_div]
 #align topological_group.to_uniform_space TopologicalGroup.toUniformSpace
 #align topological_add_group.to_uniform_space TopologicalAddGroup.toUniformSpace
 

Mathlib/Topology/MetricSpace/PseudoMetric.lean

@@ -46,12 +46,14 @@ universe u v w
 
 variable {α : Type u} {β : Type v} {X ι : Type*}
 
+theorem UniformSpace.ofDist_aux (ε : ℝ) (hε : 0 < ε) : ∃ δ > (0 : ℝ), ∀ x < δ, ∀ y < δ, x + y < ε :=
+  ⟨ε / 2, half_pos hε, fun _x hx _y hy => add_halves ε ▸ add_lt_add hx hy⟩
+
 /-- Construct a uniform structure from a distance function and metric space axioms -/
 def UniformSpace.ofDist (dist : α → α → ℝ) (dist_self : ∀ x : α, dist x x = 0)
     (dist_comm : ∀ x y : α, dist x y = dist y x)
     (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z) : UniformSpace α :=
-  .ofFun dist dist_self dist_comm dist_triangle fun ε ε0 =>
-    ⟨ε / 2, half_pos ε0, fun _x hx _y hy => add_halves ε ▸ add_lt_add hx hy⟩
+  .ofFun dist dist_self dist_comm dist_triangle ofDist_aux
 #align uniform_space_of_dist UniformSpace.ofDist
 
 -- Porting note: dropped the `dist_self` argument
@@ -162,10 +164,10 @@ def PseudoMetricSpace.ofDistTopology {α : Type u} [TopologicalSpace α] (dist :
     dist_triangle := dist_triangle
     edist_dist := fun x y => by exact ENNReal.coe_nnreal_eq _
     toUniformSpace :=
-      { toCore := (UniformSpace.ofDist dist dist_self dist_comm dist_triangle).toCore
-        isOpen_uniformity := fun s => (H s).trans <| forall₂_congr fun x _ =>
-          ((UniformSpace.hasBasis_ofFun (exists_gt (0 : ℝ)) dist _ _ _ _).comap
-            (Prod.mk x)).mem_iff.symm.trans mem_comap_prod_mk }
+      (UniformSpace.ofDist dist dist_self dist_comm dist_triangle).replaceTopology <|
+        TopologicalSpace.ext_iff.2 fun s ↦ (H s).trans <| forall₂_congr fun x _ ↦
+          ((UniformSpace.hasBasis_ofFun (exists_gt (0 : ℝ)) dist dist_self dist_comm dist_triangle
+            UniformSpace.ofDist_aux).comap (Prod.mk x)).mem_iff.symm
     uniformity_dist := rfl
     toBornology := Bornology.ofDist dist dist_comm dist_triangle
     cobounded_sets := rfl }