Update

Mathlib/Topology/MetricSpace/EMetricSpace.lean

@@ -58,9 +58,9 @@ export EDist (edist)
 def uniformSpaceOfEDist (edist : α → α → ℝ≥0∞) (edist_self : ∀ x : α, edist x x = 0)
     (edist_comm : ∀ x y : α, edist x y = edist y x)
     (edist_triangle : ∀ x y z : α, edist x z ≤ edist x y + edist y z) : UniformSpace α :=
-  .ofCore <| .ofFun edist edist_self edist_comm <| fun ε ε0 =>
-    ⟨ε / 2, ENNReal.half_pos ε0.ne', fun x y z h₁ h₂ =>
-      (edist_triangle x y z).trans_lt <| ENNReal.add_halves ε ▸ ENNReal.add_lt_add h₁ h₂⟩
+  .ofCore <| .ofFun edist edist_self edist_comm edist_triangle <| fun ε ε0 =>
+    ⟨ε / 2, ENNReal.half_pos ε0.ne', fun _ h₁ _ h₂ =>
+      (ENNReal.add_lt_add h₁ h₂).trans_eq (ENNReal.add_halves _)⟩
 #align uniform_space_of_edist uniformSpaceOfEDist
 
 -- the uniform structure is embedded in the emetric space structure
@@ -176,7 +176,7 @@ theorem uniformSpace_edist : ‹PseudoEMetricSpace α›.toUniformSpace =
 
 theorem uniformity_basis_edist :
     (𝓤 α).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) fun ε => { p : α × α | edist p.1 p.2 < ε } :=
-  (@uniformSpace_edist α _).symm ▸ UniformSpace.Core.hasBasis_ofFun ⟨1, one_pos⟩ _ _ _ _
+  (@uniformSpace_edist α _).symm ▸ UniformSpace.Core.hasBasis_ofFun ⟨1, one_pos⟩ _ _ _ _ _
 #align uniformity_basis_edist uniformity_basis_edist
 
 /-- Characterization of the elements of the uniformity in terms of the extended distance -/

Mathlib/Topology/UniformSpace/AbsoluteValue.lean

@@ -41,12 +41,11 @@ variable {R : Type _} [CommRing R] (abv : R → 𝕜) [IsAbsoluteValue abv]
 
 /-- The uniformity coming from an absolute value. -/
 def uniformSpaceCore : UniformSpace.Core R :=
-  .ofFun (fun x y => abv (y - x)) (by simp [abv_zero]) (fun x y => abv_sub abv y x) fun ε ε0 =>
-    ⟨ε / 2, half_pos ε0, fun x y z h₁ h₂ =>
-      calc abv (z - x) = abv ((z - y) + (y - x)) := by rw [sub_add_sub_cancel]
-      _ ≤ abv (z - y) + abv (y - x) := abv_add abv _ _
-      _ < ε / 2 + ε / 2 := add_lt_add h₂ h₁
-      _ = ε := add_halves ε⟩
+  .ofFun (fun x y => abv (y - x)) (by simp [abv_zero]) (fun x y => abv_sub abv y x)
+    (fun x y z =>
+      calc abv (z - x) = abv ((y - x) + (z - y)) := by rw [add_comm, sub_add_sub_cancel]
+      _ ≤ abv (y - x) + abv (z - y) := abv_add _ _ _)
+    fun ε ε0 => ⟨ε / 2, half_pos ε0, fun _ h₁ _ h₂ => (add_lt_add h₁ h₂).trans_eq (add_halves ε)⟩
 #align is_absolute_value.uniform_space_core IsAbsoluteValue.uniformSpaceCore
 
 /-- The uniform structure coming from an absolute value. -/
@@ -56,7 +55,7 @@ def uniformSpace : UniformSpace R :=
 
 theorem mem_uniformity {s : Set (R × R)} :
     s ∈ (uniformSpaceCore abv).uniformity ↔ ∃ ε > 0, ∀ {a b : R}, abv (b - a) < ε → (a, b) ∈ s :=
-  ((UniformSpace.Core.hasBasis_ofFun (exists_gt _) _ _ _ _).1 s).trans <| by
+  ((UniformSpace.Core.hasBasis_ofFun (exists_gt _) _ _ _ _ _).1 s).trans <| by
     simp only [subset_def, Prod.forall]; rfl
 #align is_absolute_value.mem_uniformity IsAbsoluteValue.mem_uniformity
 

Mathlib/Topology/UniformSpace/Basic.lean

@@ -277,24 +277,27 @@ def UniformSpace.Core.mkOfBasis {α : Type u} (B : FilterBasis (α × α))
 #align uniform_space.core.mk_of_basis UniformSpace.Core.mkOfBasis
 
 -- porting note: rfc: use `UniformSpace.Core.mkOfBasis`? This will change defeq here and there
-/-- Define a `UniformSpace.Core` using a "distance" function. The function can be, e.g., the distance
-in a (usual or extended) metric space or an absolute value on a ring. -/
-def UniformSpace.Core.ofFun {α : Type u} {β : Type v} [Zero β] [PartialOrder β] (d : α → α → β)
-    (refl : ∀ x, d x x = 0) (symm : ∀ x y, d x y = d y x)
-    (comp : ∀ ε > (0 : β), ∃ δ > (0 : β), ∀ x y z, d x y < δ → d y z < δ → d x z < ε) :
+/-- Define a `UniformSpace.Core` using a "distance" function. The function can be, e.g., the
+distance in a (usual or extended) metric space or an absolute value on a ring. -/
+def UniformSpace.Core.ofFun {α : Type u} {β : Type v} [OrderedAddCommMonoid β]
+    (d : α → α → β) (refl : ∀ x, d x x = 0) (symm : ∀ x y, d x y = d y x)
+    (triangle : ∀ x y z, d x z ≤ d x y + d y z)
+    (half : ∀ ε > (0 : β), ∃ δ > (0 : β), ∀ x < δ, ∀ y < δ, x + y < ε) :
     UniformSpace.Core α where
   uniformity := ⨅ r > 0, 𝓟 { x | d x.1 x.2 < r }
   refl := le_infᵢ₂ fun r hr => principal_mono.2 <| idRel_subset.2 fun x => by simpa [refl]
   symm := tendsto_infᵢ_infᵢ fun r => tendsto_infᵢ_infᵢ fun _ => tendsto_principal_principal.2
     fun x hx => by rwa [mem_setOf, symm]
-  comp := le_infᵢ₂ fun r hr => let ⟨δ, h0, hδr⟩ := comp r hr; le_principal_iff.2 <| mem_of_superset
+  comp := le_infᵢ₂ fun r hr => let ⟨δ, h0, hδr⟩ := half r hr; le_principal_iff.2 <| mem_of_superset
     (mem_lift' <| mem_infᵢ_of_mem δ <| mem_infᵢ_of_mem h0 <| mem_principal_self _)
-    fun _ ⟨_, h₁, h₂⟩ => hδr _ _ _ h₁ h₂
+    fun (x, z) ⟨y, h₁, h₂⟩ => (triangle _ _ _).trans_lt (hδr _ h₁ _ h₂)
 
-lemma UniformSpace.Core.hasBasis_ofFun {α : Type u} {β : Type v} [Zero β] [LinearOrder β]
+lemma UniformSpace.Core.hasBasis_ofFun {α : Type u} {β : Type v} [LinearOrderedAddCommMonoid β]
     (h₀ : ∃ x : β, 0 < x) (d : α → α → β) (refl : ∀ x, d x x = 0) (symm : ∀ x y, d x y = d y x)
-    (comp : ∀ ε > (0 : β), ∃ δ > (0 : β), ∀ x y z, d x y < δ → d y z < δ → d x z < ε) :
-    (ofFun d refl symm comp).uniformity.HasBasis ((0 : β) < ·) (fun ε => { x | d x.1 x.2 < ε }) :=
+    (triangle : ∀ x y z, d x z ≤ d x y + d y z)
+    (half : ∀ ε > (0 : β), ∃ δ > (0 : β), ∀ x < δ, ∀ y < δ, x + y < ε) :
+    (ofFun d refl symm triangle half).uniformity.HasBasis ((0 : β) < ·)
+      (fun ε => { x | d x.1 x.2 < ε }) :=
   hasBasis_binfᵢ_principal'
     (fun ε₁ h₁ ε₂ h₂ => ⟨min ε₁ ε₂, lt_min h₁ h₂, fun _x hx => lt_of_lt_of_le hx (min_le_left _ _),
       fun _x hx => lt_of_lt_of_le hx (min_le_right _ _)⟩) h₀