refactor(topology/metric_space): drop dist_setoid (#18502)

Use `uniform_space.separation_setoid` instead.

src/topology/constructions.lean

@@ -757,9 +757,13 @@ lemma nhds_inl (x : α) : 𝓝 (inl x : α ⊕ β) = map inl (𝓝 x) :=
 lemma nhds_inr (x : β) : 𝓝 (inr x : α ⊕ β) = map inr (𝓝 x) :=
 (open_embedding_inr.map_nhds_eq _).symm
 
+theorem continuous_sum_dom {f : α ⊕ β → γ} :
+    continuous f ↔ continuous (f ∘ sum.inl) ∧ continuous (f ∘ sum.inr) :=
+by simp only [continuous_sup_dom, continuous_coinduced_dom]
+
 lemma continuous_sum_elim {f : α → γ} {g : β → γ} :
   continuous (sum.elim f g) ↔ continuous f ∧ continuous g :=
-by simp only [continuous_sup_dom, continuous_coinduced_dom, sum.elim_comp_inl, sum.elim_comp_inr]
+continuous_sum_dom
 
 @[continuity] lemma continuous.sum_elim {f : α → γ} {g : β → γ}
   (hf : continuous f) (hg : continuous g) : continuous (sum.elim f g) :=

src/topology/metric_space/basic.lean

@@ -2962,61 +2962,20 @@ end metric
 
 section eq_rel
 
-/-- The canonical equivalence relation on a pseudometric space. -/
-def pseudo_metric.dist_setoid (α : Type u) [pseudo_metric_space α] : setoid α :=
-setoid.mk (λx y, dist x y = 0)
-begin
-  unfold equivalence,
-  repeat { split },
-  { exact pseudo_metric_space.dist_self },
-  { assume x y h, rwa pseudo_metric_space.dist_comm },
-  { assume x y z hxy hyz,
-    refine le_antisymm _ dist_nonneg,
-    calc dist x z ≤ dist x y + dist y z : pseudo_metric_space.dist_triangle _ _ _
-         ... = 0 + 0 : by rw [hxy, hyz]
-         ... = 0 : by simp }
-end
-
-local attribute [instance] pseudo_metric.dist_setoid
-
-/-- The canonical quotient of a pseudometric space, identifying points at distance `0`. -/
-@[reducible] definition pseudo_metric_quot (α : Type u) [pseudo_metric_space α] : Type* :=
-quotient (pseudo_metric.dist_setoid α)
-
-instance has_dist_metric_quot {α : Type u} [pseudo_metric_space α] :
-  has_dist (pseudo_metric_quot α) :=
-{ dist := quotient.lift₂ (λp q : α, dist p q)
-begin
-  assume x y x' y' hxx' hyy',
-  have Hxx' : dist x x' = 0 := hxx',
-  have Hyy' : dist y y' = 0 := hyy',
-  have A : dist x y ≤ dist x' y' := calc
-    dist x y ≤ dist x x' + dist x' y : pseudo_metric_space.dist_triangle _ _ _
-    ... = dist x' y : by simp [Hxx']
-    ... ≤ dist x' y' + dist y' y : pseudo_metric_space.dist_triangle _ _ _
-    ... = dist x' y' : by simp [pseudo_metric_space.dist_comm, Hyy'],
-  have B : dist x' y' ≤ dist x y := calc
-    dist x' y' ≤ dist x' x + dist x y' : pseudo_metric_space.dist_triangle _ _ _
-    ... = dist x y' : by simp [pseudo_metric_space.dist_comm, Hxx']
-    ... ≤ dist x y + dist y y' : pseudo_metric_space.dist_triangle _ _ _
-    ... = dist x y : by simp [Hyy'],
-  exact le_antisymm A B
-end }
-
-lemma pseudo_metric_quot_dist_eq {α : Type u} [pseudo_metric_space α] (p q : α) :
-  dist ⟦p⟧ ⟦q⟧ = dist p q := rfl
-
-instance metric_space_quot {α : Type u} [pseudo_metric_space α] :
-  metric_space (pseudo_metric_quot α) :=
-{ dist_self := begin
-    refine quotient.ind (λy, _),
-    exact pseudo_metric_space.dist_self _
-  end,
-  eq_of_dist_eq_zero := λxc yc, by exact quotient.induction_on₂ xc yc (λx y H, quotient.sound H),
-  dist_comm :=
-    λxc yc, quotient.induction_on₂ xc yc (λx y, pseudo_metric_space.dist_comm _ _),
-  dist_triangle :=
-    λxc yc zc, quotient.induction_on₃ xc yc zc (λx y z, pseudo_metric_space.dist_triangle _ _ _) }
+instance {α : Type u} [pseudo_metric_space α] :
+  has_dist (uniform_space.separation_quotient α) :=
+{ dist := λ p q, quotient.lift_on₂' p q dist $ λ x y x' y' hx hy,
+    by rw [dist_edist, dist_edist, ← uniform_space.separation_quotient.edist_mk x,
+      ← uniform_space.separation_quotient.edist_mk x', quot.sound hx, quot.sound hy] }
+
+lemma uniform_space.separation_quotient.dist_mk {α : Type u} [pseudo_metric_space α] (p q : α) :
+  @dist (uniform_space.separation_quotient α) _ (quot.mk _ p) (quot.mk _ q) = dist p q :=
+rfl
+
+instance {α : Type u} [pseudo_metric_space α] :
+  metric_space (uniform_space.separation_quotient α) :=
+emetric_space.to_metric_space_of_dist dist (λ x y, quotient.induction_on₂' x y edist_ne_top) $
+  λ x y, quotient.induction_on₂' x y dist_edist
 
 end eq_rel
 

src/topology/metric_space/emetric_space.lean

@@ -1062,6 +1062,37 @@ end diam
 
 end emetric
 
+/-!
+### Separation quotient
+-/
+
+instance [pseudo_emetric_space X] : has_edist (uniform_space.separation_quotient X) :=
+⟨λ x y, quotient.lift_on₂' x y edist $ λ x y x' y' hx hy,
+  calc edist x y = edist x' y : edist_congr_right $
+    emetric.inseparable_iff.1 $ separation_rel_iff_inseparable.1 hx
+  ... = edist x' y' : edist_congr_left $
+    emetric.inseparable_iff.1 $ separation_rel_iff_inseparable.1 hy⟩
+
+@[simp] theorem uniform_space.separation_quotient.edist_mk [pseudo_emetric_space X] (x y : X) :
+  @edist (uniform_space.separation_quotient X) _ (quot.mk _ x) (quot.mk _ y) = edist x y :=
+rfl
+
+instance [pseudo_emetric_space X] : emetric_space (uniform_space.separation_quotient X) :=
+@emetric.of_t0_pseudo_emetric_space (uniform_space.separation_quotient X)
+  { edist_self := λ x, quotient.induction_on' x edist_self,
+    edist_comm := λ x y, quotient.induction_on₂' x y edist_comm,
+    edist_triangle := λ x y z, quotient.induction_on₃' x y z edist_triangle,
+    to_uniform_space := infer_instance,
+    uniformity_edist := (uniformity_basis_edist.map _).eq_binfi.trans $ infi_congr $ λ ε,
+      infi_congr $ λ hε, congr_arg 𝓟
+      begin
+        ext ⟨⟨x⟩, ⟨y⟩⟩,
+        refine ⟨_, λ h, ⟨(x, y), h, rfl⟩⟩,
+        rintro ⟨⟨x', y'⟩, h', h⟩,
+        simp only [prod.ext_iff] at h,
+        rwa [← h.1, ← h.2]
+      end } _
+
 /-!
 ### `additive`, `multiplicative`
 

src/topology/metric_space/gluing.lean

@@ -514,7 +514,7 @@ variables {X : Type u} {Y : Type v} {Z : Type w}
 variables [nonempty Z] [metric_space Z] [metric_space X] [metric_space Y]
           {Φ : Z → X} {Ψ : Z → Y} {ε : ℝ}
 open _root_.sum (inl inr)
-local attribute [instance] pseudo_metric.dist_setoid
+local attribute [instance] uniform_space.separation_setoid
 
 /-- Given two isometric embeddings `Φ : Z → X` and `Ψ : Z → Y`, we define a pseudo metric space
 structure on `X ⊕ Y` by declaring that `Φ x` and `Ψ x` are at distance `0`. -/
@@ -526,20 +526,15 @@ def glue_premetric (hΦ : isometry Φ) (hΨ : isometry Ψ) : pseudo_metric_space
 
 /-- Given two isometric embeddings `Φ : Z → X` and `Ψ : Z → Y`, we define a
 space  `glue_space hΦ hΨ` by identifying in `X ⊕ Y` the points `Φ x` and `Ψ x`. -/
+@[derive metric_space]
 def glue_space (hΦ : isometry Φ) (hΨ : isometry Ψ) : Type* :=
-@pseudo_metric_quot _ (glue_premetric hΦ hΨ)
-
-instance metric_space_glue_space (hΦ : isometry Φ) (hΨ : isometry Ψ) :
-  metric_space (glue_space hΦ hΨ) :=
-@metric_space_quot _ (glue_premetric hΦ hΨ)
+@uniform_space.separation_quotient _ (glue_premetric hΦ hΨ).to_uniform_space
 
 /-- The canonical map from `X` to the space obtained by gluing isometric subsets in `X` and `Y`. -/
-def to_glue_l (hΦ : isometry Φ) (hΨ : isometry Ψ) (x : X) : glue_space hΦ hΨ :=
-by letI : pseudo_metric_space (X ⊕ Y) := glue_premetric hΦ hΨ; exact ⟦inl x⟧
+def to_glue_l (hΦ : isometry Φ) (hΨ : isometry Ψ) (x : X) : glue_space hΦ hΨ := quotient.mk' (inl x)
 
 /-- The canonical map from `Y` to the space obtained by gluing isometric subsets in `X` and `Y`. -/
-def to_glue_r (hΦ : isometry Φ) (hΨ : isometry Ψ) (y : Y) : glue_space hΦ hΨ :=
-by letI : pseudo_metric_space (X ⊕ Y) := glue_premetric hΦ hΨ; exact ⟦inr y⟧
+def to_glue_r (hΦ : isometry Φ) (hΨ : isometry Ψ) (y : Y) : glue_space hΦ hΨ := quotient.mk' (inr y)
 
 instance inhabited_left (hΦ : isometry Φ) (hΨ : isometry Ψ) [inhabited X] :
   inhabited (glue_space hΦ hΨ) :=
@@ -552,9 +547,11 @@ instance inhabited_right (hΦ : isometry Φ) (hΨ : isometry Ψ) [inhabited Y] :
 lemma to_glue_commute (hΦ : isometry Φ) (hΨ : isometry Ψ) :
   (to_glue_l hΦ hΨ) ∘ Φ = (to_glue_r hΦ hΨ) ∘ Ψ :=
 begin
-  letI : pseudo_metric_space (X ⊕ Y) := glue_premetric hΦ hΨ,
+  letI i : pseudo_metric_space (X ⊕ Y) := glue_premetric hΦ hΨ,
+  letI := i.to_uniform_space,
   funext,
-  simp only [comp, to_glue_l, to_glue_r, quotient.eq],
+  simp only [comp, to_glue_l, to_glue_r],
+  refine uniform_space.separation_quotient.mk_eq_mk.2 (metric.inseparable_iff.2 _),
   exact glue_dist_glued_points Φ Ψ 0 x
 end
 
@@ -636,20 +633,15 @@ def inductive_premetric (I : ∀ n, isometry (f n)) :
                 inductive_limit_dist_eq_dist I y z m hy hz]
   end }
 
-local attribute [instance] inductive_premetric pseudo_metric.dist_setoid
+local attribute [instance] inductive_premetric uniform_space.separation_setoid
 
 /-- The type giving the inductive limit in a metric space context. -/
-def inductive_limit (I : ∀ n, isometry (f n)) : Type* :=
-@pseudo_metric_quot _ (inductive_premetric I)
-
-/-- Metric space structure on the inductive limit. -/
-instance metric_space_inductive_limit (I : ∀ n, isometry (f n)) :
-  metric_space (inductive_limit I) :=
-@metric_space_quot _ (inductive_premetric I)
+@[derive metric_space] def inductive_limit (I : ∀ n, isometry (f n)) : Type* :=
+@uniform_space.separation_quotient _ (inductive_premetric I).to_uniform_space
 
 /-- Mapping each `X n` to the inductive limit. -/
 def to_inductive_limit (I : ∀ n, isometry (f n)) (n : ℕ) (x : X n) : metric.inductive_limit I :=
-by letI : pseudo_metric_space (Σ n, X n) := inductive_premetric I; exact ⟦sigma.mk n x⟧
+quotient.mk' (sigma.mk n x)
 
 instance (I : ∀ n, isometry (f n)) [inhabited (X 0)] : inhabited (inductive_limit I) :=
 ⟨to_inductive_limit _ 0 default⟩
@@ -667,8 +659,10 @@ end
 lemma to_inductive_limit_commute (I : ∀ n, isometry (f n)) (n : ℕ) :
   (to_inductive_limit I n.succ) ∘ (f n) = to_inductive_limit I n :=
 begin
+  letI := inductive_premetric I,
   funext,
-  simp only [comp, to_inductive_limit, quotient.eq],
+  simp only [comp, to_inductive_limit],
+  refine uniform_space.separation_quotient.mk_eq_mk.2 (metric.inseparable_iff.2 _),
   show inductive_limit_dist f ⟨n.succ, f n x⟩ ⟨n, x⟩ = 0,
   { rw [inductive_limit_dist_eq_dist I ⟨n.succ, f n x⟩ ⟨n, x⟩ n.succ,
         le_rec_on_self, le_rec_on_succ, le_rec_on_self, dist_self],

src/topology/metric_space/gromov_hausdorff.lean

@@ -429,7 +429,6 @@ instance : metric_space GH_space :=
     let Ψ : Y → γ2 := optimal_GH_injl Y Z,
     have hΨ : isometry Ψ := isometry_optimal_GH_injl Y Z,
     let γ := glue_space hΦ hΨ,
-    letI : metric_space γ := metric.metric_space_glue_space hΦ hΨ,
     have Comm : (to_glue_l hΦ hΨ) ∘ (optimal_GH_injr X Y) =
       (to_glue_r hΦ hΨ) ∘ (optimal_GH_injl Y Z) := to_glue_commute hΦ hΨ,
     calc dist x z = dist (to_GH_space X) (to_GH_space Z) :
@@ -918,6 +917,8 @@ structure aux_gluing_struct (A : Type) [metric_space A] : Type 1 :=
 (embed  : A → space)
 (isom   : isometry embed)
 
+local attribute [instance] aux_gluing_struct.metric
+
 instance (A : Type) [metric_space A] : inhabited (aux_gluing_struct A) :=
 ⟨{ space := A,
   metric := by apply_instance,
@@ -927,17 +928,13 @@ instance (A : Type) [metric_space A] : inhabited (aux_gluing_struct A) :=
 /-- Auxiliary sequence of metric spaces, containing copies of `X 0`, ..., `X n`, where each
 `X i` is glued to `X (i+1)` in an optimal way. The space at step `n+1` is obtained from the space
 at step `n` by adding `X (n+1)`, glued in an optimal way to the `X n` already sitting there. -/
-def aux_gluing (n : ℕ) : aux_gluing_struct (X n) := nat.rec_on n
-  { space  := X 0,
-    metric := by apply_instance,
-    embed  := id,
-    isom   := λ x y, rfl }
-(λ n Y, by letI : metric_space Y.space := Y.metric; exact
+def aux_gluing (n : ℕ) : aux_gluing_struct (X n) :=
+nat.rec_on n default $ λ n Y,
   { space  := glue_space Y.isom (isometry_optimal_GH_injl (X n) (X (n+1))),
     metric := by apply_instance,
     embed  := (to_glue_r Y.isom (isometry_optimal_GH_injl (X n) (X (n+1))))
               ∘ (optimal_GH_injr (X n) (X (n+1))),
-    isom   := (to_glue_r_isometry _ _).comp (isometry_optimal_GH_injr (X n) (X (n+1))) })
+    isom   := (to_glue_r_isometry _ _).comp (isometry_optimal_GH_injr (X n) (X (n+1))) }
 
 /-- The Gromov-Hausdorff space is complete. -/
 instance : complete_space GH_space :=
@@ -949,20 +946,16 @@ begin
   let X := λ n, (u n).rep,
   -- glue them together successively in an optimal way, getting a sequence of metric spaces `Y n`
   let Y := aux_gluing X,
-  letI : ∀ n, metric_space (Y n).space := λ n, (Y n).metric,
+  -- this equality is true by definition but Lean unfolds some defs in the wrong order
   have E : ∀ n : ℕ,
-    glue_space (Y n).isom (isometry_optimal_GH_injl (X n) (X n.succ)) = (Y n.succ).space :=
-    λ n, by { simp only [Y, aux_gluing], refl },
+    glue_space (Y n).isom (isometry_optimal_GH_injl (X n) (X (n + 1))) = (Y (n + 1)).space :=
+    λ n, by { dsimp only [Y, aux_gluing], refl },
   let c := λ n, cast (E n),
-  have ic : ∀ n, isometry (c n) := λ n x y, rfl,
+  have ic : ∀ n, isometry (c n) := λ n x y, by { dsimp only [Y, aux_gluing], exact rfl },
   -- there is a canonical embedding of `Y n` in `Y (n+1)`, by construction
-  let f : Πn, (Y n).space → (Y n.succ).space :=
-    λ n, (c n) ∘ (to_glue_l (aux_gluing X n).isom (isometry_optimal_GH_injl (X n) (X n.succ))),
-  have I : ∀ n, isometry (f n),
-  { assume n,
-    apply isometry.comp,
-    { assume x y, refl },
-    { apply to_glue_l_isometry } },
+  let f : Π n, (Y n).space → (Y (n + 1)).space :=
+    λ n, c n ∘ to_glue_l (Y n).isom (isometry_optimal_GH_injl (X n) (X n.succ)),
+  have I : ∀ n, isometry (f n) := λ n, (ic n).comp (to_glue_l_isometry _ _),
   -- consider the inductive limit `Z0` of the `Y n`, and then its completion `Z`
   let Z0 := metric.inductive_limit I,
   let Z := uniform_space.completion Z0,