chore(topology/metric_space): remove instances that duplicate lemmas (#…

…14639)

We can use the structure projections directly as instances, rather than duplicating them with primed names. This removes;

* `metric_space.to_uniform_space'` (was misnamed, now `pseudo_metric_space.to_uniform_space`)
* `pseudo_metric_space.to_bornology'` (now `pseudo_metric_space.to_bornology`)
* `pseudo_emetric_space.to_uniform_space'` (now `pseudo_metric_space.to_uniform_space`)
* `emetric_space.to_uniform_space'` (redundant)

Follows up from review comments in #13927

src/topology/metric_space/basic.lean

@@ -192,13 +192,8 @@ end
 
 variables [pseudo_metric_space α]
 
-@[priority 100] -- see Note [lower instance priority]
-instance metric_space.to_uniform_space' : uniform_space α :=
-pseudo_metric_space.to_uniform_space
-
-@[priority 100] -- see Note [lower instance priority]
-instance pseudo_metric_space.to_bornology' {α : Type u} [pseudo_metric_space α] : bornology α :=
-pseudo_metric_space.to_bornology
+attribute [priority 100, instance] pseudo_metric_space.to_uniform_space
+attribute [priority 100, instance] pseudo_metric_space.to_bornology
 
 @[priority 200] -- see Note [lower instance priority]
 instance pseudo_metric_space.to_has_edist : has_edist α := ⟨pseudo_metric_space.edist⟩
@@ -1065,7 +1060,7 @@ by rw [emetric.inseparable_iff, edist_nndist, dist_nndist, ennreal.coe_eq_zero,
 See Note [forgetful inheritance].
 -/
 def pseudo_metric_space.replace_uniformity {α} [U : uniform_space α] (m : pseudo_metric_space α)
-  (H : @uniformity _ U = @uniformity _ pseudo_emetric_space.to_uniform_space') :
+  (H : @uniformity _ U = @uniformity _ pseudo_emetric_space.to_uniform_space) :
   pseudo_metric_space α :=
 { dist               := @dist _ m.to_has_dist,
   dist_self          := dist_self,
@@ -1078,7 +1073,7 @@ def pseudo_metric_space.replace_uniformity {α} [U : uniform_space α] (m : pseu
 
 lemma pseudo_metric_space.replace_uniformity_eq {α} [U : uniform_space α]
   (m : pseudo_metric_space α)
-  (H : @uniformity _ U = @uniformity _ pseudo_emetric_space.to_uniform_space') :
+  (H : @uniformity _ U = @uniformity _ pseudo_emetric_space.to_uniform_space) :
   m.replace_uniformity H = m :=
 by { ext, refl }
 
@@ -1134,15 +1129,15 @@ pseudo_emetric_space.to_pseudo_metric_space_of_dist
 See Note [forgetful inheritance].
 -/
 def pseudo_metric_space.replace_bornology {α} [B : bornology α] (m : pseudo_metric_space α)
-  (H : ∀ s, @is_bounded _ B s ↔ @is_bounded _ pseudo_metric_space.to_bornology' s) :
+  (H : ∀ s, @is_bounded _ B s ↔ @is_bounded _ pseudo_metric_space.to_bornology s) :
   pseudo_metric_space α :=
 { to_bornology := B,
   cobounded_sets := set.ext $ compl_surjective.forall.2 $ λ s, (H s).trans $
     by rw [is_bounded_iff, mem_set_of_eq, compl_compl],
   .. m }
 
 lemma pseudo_metric_space.replace_bornology_eq {α} [m : pseudo_metric_space α] [B : bornology α]
-  (H : ∀ s, @is_bounded _ B s ↔ @is_bounded _ pseudo_metric_space.to_bornology' s) :
+  (H : ∀ s, @is_bounded _ B s ↔ @is_bounded _ pseudo_metric_space.to_bornology s) :
   pseudo_metric_space.replace_bornology _ H = m :=
 by { ext, refl }
 
@@ -1747,7 +1742,7 @@ begin
     from ne_of_lt ((finset.sup_lt_iff bot_lt_top).2 $ λ b hb, edist_lt_top _ _),
   show ↑(sup univ (λ b, nndist (f b) (g b))) = (sup univ (λ b, edist (f b) (g b))).to_real,
     by simp only [edist_nndist, ← ennreal.coe_finset_sup, ennreal.coe_to_real],
-  show (@is_bounded _ pi.bornology s ↔ @is_bounded _ pseudo_metric_space.to_bornology' _),
+  show (@is_bounded _ pi.bornology s ↔ @is_bounded _ pseudo_metric_space.to_bornology _),
   { simp only [← is_bounded_def, is_bounded_iff_eventually, ← forall_is_bounded_image_eval_iff,
       ball_image_iff, ← eventually_all, function.eval_apply, @dist_nndist (π _)],
     refine eventually_congr ((eventually_ge_at_top 0).mono $ λ C hC, _),
@@ -2605,13 +2600,13 @@ end metric
 See Note [forgetful inheritance].
 -/
 def metric_space.replace_uniformity {γ} [U : uniform_space γ] (m : metric_space γ)
-  (H : @uniformity _ U = @uniformity _ emetric_space.to_uniform_space') :
+  (H : @uniformity _ U = @uniformity _ pseudo_emetric_space.to_uniform_space) :
   metric_space γ :=
 { eq_of_dist_eq_zero := @eq_of_dist_eq_zero _ _,
   ..pseudo_metric_space.replace_uniformity m.to_pseudo_metric_space H, }
 
 lemma metric_space.replace_uniformity_eq {γ} [U : uniform_space γ] (m : metric_space γ)
-  (H : @uniformity _ U = @uniformity _ emetric_space.to_uniform_space') :
+  (H : @uniformity _ U = @uniformity _ pseudo_emetric_space.to_uniform_space) :
   m.replace_uniformity H = m :=
 by { ext, refl }
 

src/topology/metric_space/emetric_space.lean

@@ -99,14 +99,12 @@ class pseudo_emetric_space (α : Type u) extends has_edist α : Type u :=
   uniform_space_of_edist edist edist_self edist_comm edist_triangle)
 (uniformity_edist : 𝓤 α = ⨅ ε>0, 𝓟 {p:α×α | edist p.1 p.2 < ε} . control_laws_tac)
 
+attribute [priority 100, instance] pseudo_emetric_space.to_uniform_space
+
 /- Pseudoemetric spaces are less common than metric spaces. Therefore, we work in a dedicated
 namespace, while notions associated to metric spaces are mostly in the root namespace. -/
 variables [pseudo_emetric_space α]
 
-@[priority 100] -- see Note [lower instance priority]
-instance pseudo_emetric_space.to_uniform_space' : uniform_space α :=
-pseudo_emetric_space.to_uniform_space
-
 export pseudo_emetric_space (edist_self edist_comm edist_triangle)
 
 attribute [simp] edist_self
@@ -836,10 +834,6 @@ class emetric_space (α : Type u) extends pseudo_emetric_space α : Type u :=
 
 variables {γ : Type w} [emetric_space γ]
 
-@[priority 100] -- see Note [lower instance priority]
-instance emetric_space.to_uniform_space' : uniform_space γ :=
-pseudo_emetric_space.to_uniform_space
-
 export emetric_space (eq_of_edist_eq_zero)
 
 /-- Characterize the equality of points by the vanishing of their extended distance -/

src/topology/uniform_space/compare_reals.lean

@@ -55,7 +55,7 @@ open set function filter cau_seq uniform_space
 /-- The metric space uniform structure on ℚ (which presupposes the existence
 of real numbers) agrees with the one coming directly from (abs : ℚ → ℚ). -/
 lemma rat.uniform_space_eq :
-  is_absolute_value.uniform_space (abs : ℚ → ℚ) = metric_space.to_uniform_space' :=
+  is_absolute_value.uniform_space (abs : ℚ → ℚ) = pseudo_metric_space.to_uniform_space :=
 begin
   ext s,
   erw [metric.mem_uniformity_dist, is_absolute_value.mem_uniformity],