refactor(topology/metric_space/emetric_space): add pseudo_emetric (#6694

)

Working on the Liquid Tensor Experiment, we realize we need seminorms ~~pseudonorms~~ (meaning we don't require `∥x∥ = 0 → x = 0`). For this reason I would like to include seminorms, pseudometric and pseudoemetric to mathlib. (We currently have `premetric_space`, my plan is to change the name to `pseudometric_space`, that seems to be the standard terminology.)

I started modifying `emetric_space` since it seems the more fundamental (looking at the structure of the imports). What I did here is to define a new class `pseudo_emetric_space`, generalize almost all the results about `emetric_space` to this case (I mean, all the results that are actually true) and at the end of the file I defined `emetric_space` and prove the remaining results. It is the first time I did a refactor like this, so I probably did something wrong, but at least it compiles on my computer.

I don't know why one proof in `measure_theory/ae_eq_fun_metric.lean` stopped working, the same proof in tactic mode works.

src/measure_theory/ae_eq_fun_metric.lean

@@ -57,8 +57,11 @@ instance : emetric_space (α →ₘ[μ] γ) :=
       measure_theory.lintegral_mono (λ a, edist_triangle (f a) (g a) (h a))
     ... = ∫⁻ a, edist (f a) (g a) ∂μ + ∫⁻ a, edist (g a) (h a) ∂μ :
       lintegral_add' (hf.edist hg) (hg.edist hh),
-  eq_of_edist_eq_zero := λ f g, induction_on₂ f g $ λ f hf g hg H, mk_eq_mk.2 $
-    ((lintegral_eq_zero_iff' (hf.edist hg)).1 H).mono $ λ x, eq_of_edist_eq_zero }
+  eq_of_edist_eq_zero := λ f g,
+  begin
+    exact induction_on₂ f g (λ f hf g hg H, mk_eq_mk.2 (((lintegral_eq_zero_iff'
+      (hf.edist hg)).1 H).mono (λ x, eq_of_edist_eq_zero)))
+  end }
 
 lemma edist_mk_mk {f g : α → γ} (hf hg) :
   edist (mk f hf : α →ₘ[μ] γ) (mk g hg) = ∫⁻ x, edist (f x) (g x) ∂μ :=

src/topology/metric_space/basic.lean

@@ -809,7 +809,7 @@ let m : metric_space α :=
   eq_of_dist_eq_zero := λx y hxy,
     by simpa [h, ennreal.to_real_eq_zero_iff, edist_ne_top x y] using hxy,
   dist_self          := λx, by simp [h],
-  dist_comm          := λx y, by simp [h, emetric_space.edist_comm],
+  dist_comm          := λx y, by simp [h, pseudo_emetric_space.edist_comm],
   dist_triangle      := λx y z, begin
     simp only [h],
     rw [← ennreal.to_real_add (edist_ne_top _ _) (edist_ne_top _ _),