refactor(analysis/normed_space/pi_Lp): golf some instances (#14339)

* drop `pi_Lp.emetric_aux`;
* use `T₀` to get `(e)metric_space` from `pseudo_(e)metric_space`;
* restate `pi_Lp.(anti)lipschitz_with_equiv` with correct `pseudo_emetric_space` instances; while they're defeq, it's better not to leak auxiliary instances unless necessary.

Author: urkud

src/analysis/normed_space/pi_Lp.lean

@@ -101,56 +101,40 @@ from the edistance (which is equal to it, but not defeq). See Note [forgetful in
 explaining why having definitionally the right uniformity is often important.
 -/
 
-variables [Π i, emetric_space (α i)] [Π i, pseudo_emetric_space (β i)] [fintype ι]
+variables [Π i, pseudo_metric_space (α i)] [Π i, pseudo_emetric_space (β i)] [fintype ι]
+
 include fact_one_le_p
 
+private lemma pos : 0 < p := zero_lt_one.trans_le fact_one_le_p.out
+
 /-- Endowing the space `pi_Lp p β` with the `L^p` pseudoedistance. This definition is not
 satisfactory, as it does not register the fact that the topology and the uniform structure coincide
 with the product one. Therefore, we do not register it as an instance. Using this as a temporary
 pseudoemetric space instance, we will show that the uniform structure is equal (but not defeq) to
 the product one, and then register an instance in which we replace the uniform structure by the
 product one using this pseudoemetric space and `pseudo_emetric_space.replace_uniformity`. -/
 def pseudo_emetric_aux : pseudo_emetric_space (pi_Lp p β) :=
-have pos : 0 < p := lt_of_lt_of_le zero_lt_one fact_one_le_p.out,
 { edist          := λ f g, (∑ i, edist (f i) (g i) ^ p) ^ (1/p),
-  edist_self     := λ f, by simp [edist, ennreal.zero_rpow_of_pos pos,
-                                  ennreal.zero_rpow_of_pos (inv_pos.2 pos)],
+  edist_self     := λ f, by simp [edist, ennreal.zero_rpow_of_pos (pos p),
+    ennreal.zero_rpow_of_pos (inv_pos.2 $ pos p)],
   edist_comm     := λ f g, by simp [edist, edist_comm],
   edist_triangle := λ f g h, calc
     (∑ i, edist (f i) (h i) ^ p) ^ (1 / p) ≤
     (∑ i, (edist (f i) (g i) + edist (g i) (h i)) ^ p) ^ (1 / p) :
     begin
-      apply ennreal.rpow_le_rpow _ (one_div_nonneg.2 $ le_of_lt pos),
+      apply ennreal.rpow_le_rpow _ (one_div_nonneg.2 (pos p).le),
       refine finset.sum_le_sum (λ i hi, _),
-      exact ennreal.rpow_le_rpow (edist_triangle _ _ _) (le_trans zero_le_one fact_one_le_p.out)
+      exact ennreal.rpow_le_rpow (edist_triangle _ _ _) (pos p).le
     end
     ... ≤
     (∑ i, edist (f i) (g i) ^ p) ^ (1 / p) + (∑ i, edist (g i) (h i) ^ p) ^ (1 / p) :
       ennreal.Lp_add_le _ _ _ fact_one_le_p.out }
 
-/-- Endowing the space `pi_Lp p α` with the `L^p` edistance. This definition is not satisfactory,
-as it does not register the fact that the topology and the uniform structure coincide with the
-product one. Therefore, we do not register it as an instance. Using this as a temporary emetric
-space instance, we will show that the uniform structure is equal (but not defeq) to the product
-one, and then register an instance in which we replace the uniform structure by the product one
-using this emetric space and `emetric_space.replace_uniformity`. -/
-def emetric_aux : emetric_space (pi_Lp p α) :=
-{ eq_of_edist_eq_zero := λ f g hfg,
-  begin
-    have pos : 0 < p := lt_of_lt_of_le zero_lt_one fact_one_le_p.out,
-    letI h := pseudo_emetric_aux p α,
-    have h : edist f g = (∑ i, (edist (f i) (g i)) ^ p) ^ (1/p) := rfl,
-    simp [h, ennreal.rpow_eq_zero_iff, pos, asymm pos, finset.sum_eq_zero_iff_of_nonneg] at hfg,
-    exact funext hfg
-  end,
-  ..pseudo_emetric_aux p α }
-
-local attribute [instance] pi_Lp.emetric_aux pi_Lp.pseudo_emetric_aux
+local attribute [instance] pi_Lp.pseudo_emetric_aux
 
-lemma lipschitz_with_equiv : lipschitz_with 1 (pi_Lp.equiv p β) :=
+lemma lipschitz_with_equiv_aux : lipschitz_with 1 (pi_Lp.equiv p β) :=
 begin
-  have pos : 0 < p := lt_of_lt_of_le zero_lt_one fact_one_le_p.out,
-  have cancel : p * (1/p) = 1 := mul_div_cancel' 1 (ne_of_gt pos),
+  have cancel : p * (1/p) = 1 := mul_div_cancel' 1 (pos p).ne',
   assume x y,
   simp only [edist, forall_prop_of_true, one_mul, finset.mem_univ, finset.sup_le_iff,
              ennreal.coe_one],
@@ -160,12 +144,12 @@ begin
     by simp [← ennreal.rpow_mul, cancel, -one_div]
   ... ≤ (∑ i, edist (x i) (y i) ^ p) ^ (1 / p) :
   begin
-    apply ennreal.rpow_le_rpow _ (one_div_nonneg.2 $ le_of_lt pos),
+    apply ennreal.rpow_le_rpow _ (one_div_nonneg.2 $ (pos p).le),
     exact finset.single_le_sum (λ i hi, (bot_le : (0 : ℝ≥0∞) ≤ _)) (finset.mem_univ i)
   end
 end
 
-lemma antilipschitz_with_equiv :
+lemma antilipschitz_with_equiv_aux :
   antilipschitz_with ((fintype.card ι : ℝ≥0) ^ (1/p)) (pi_Lp.equiv p β) :=
 begin
   have pos : 0 < p := lt_of_lt_of_le zero_lt_one fact_one_le_p.out,
@@ -196,8 +180,8 @@ lemma aux_uniformity_eq :
   𝓤 (pi_Lp p β) = @uniformity _ (Pi.uniform_space _) :=
 begin
   have A : uniform_inducing (pi_Lp.equiv p β) :=
-    (antilipschitz_with_equiv p β).uniform_inducing
-    (lipschitz_with_equiv p β).uniform_continuous,
+    (antilipschitz_with_equiv_aux p β).uniform_inducing
+    (lipschitz_with_equiv_aux p β).uniform_continuous,
   have : (λ (x : pi_Lp p β × pi_Lp p β),
     ((pi_Lp.equiv p β) x.fst, (pi_Lp.equiv p β) x.snd)) = id,
     by ext i; refl,
@@ -222,49 +206,30 @@ instance [Π i, pseudo_emetric_space (β i)] : pseudo_emetric_space (pi_Lp p β)
 /-- emetric space instance on the product of finitely many emetric spaces, using the `L^p`
 edistance, and having as uniformity the product uniformity. -/
 instance [Π i, emetric_space (α i)] : emetric_space (pi_Lp p α) :=
-(emetric_aux p α).replace_uniformity (aux_uniformity_eq p α).symm
+@emetric.of_t0_pseudo_emetric_space _ _ $
+  -- TODO: add `Pi.t0_space`
+  by { haveI : t2_space (pi_Lp p α) := Pi.t2_space, apply_instance }
 
-omit fact_one_le_p
-lemma edist_eq {p : ℝ} [fact (1 ≤ p)] {β : ι → Type*}
-  [Π i, pseudo_emetric_space (β i)] (x y : pi_Lp p β) :
+variables {p β}
+lemma edist_eq [Π i, pseudo_emetric_space (β i)] (x y : pi_Lp p β) :
   edist x y = (∑ i, edist (x i) (y i) ^ p) ^ (1/p) := rfl
-include fact_one_le_p
+variables (p β)
 
 /-- pseudometric space instance on the product of finitely many psuedometric spaces, using the
 `L^p` distance, and having as uniformity the product uniformity. -/
 instance [Π i, pseudo_metric_space (β i)] : pseudo_metric_space (pi_Lp p β) :=
-begin
-  /- we construct the instance from the pseudo emetric space instance to avoid checking again that
-  the uniformity is the same as the product uniformity, but we register nevertheless a nice formula
-  for the distance -/
-  have pos : 0 < p := lt_of_lt_of_le zero_lt_one fact_one_le_p.out,
-  refine pseudo_emetric_space.to_pseudo_metric_space_of_dist
-    (λf g, (∑ i, dist (f i) (g i) ^ p) ^ (1/p)) (λ f g, _) (λ f g, _),
-  { simp [pi_Lp.edist_eq, ennreal.rpow_eq_top_iff, asymm pos, pos,
-          ennreal.sum_eq_top_iff, edist_ne_top] },
-  { have A : ∀ (i : ι), i ∈ (finset.univ : finset ι) → edist (f i) (g i) ^ p ≠ ⊤ :=
-      λ i hi, by simp [lt_top_iff_ne_top, edist_ne_top, le_of_lt pos],
-    simp [dist, -one_div, pi_Lp.edist_eq, ← ennreal.to_real_rpow,
-          ennreal.to_real_sum A, dist_edist] }
-end
+pseudo_emetric_space.to_pseudo_metric_space_of_dist
+  (λ f g, (∑ i, dist (f i) (g i) ^ p) ^ (1/p))
+  (λ f g, ennreal.rpow_ne_top_of_nonneg (one_div_nonneg.2 (pos p).le) $ ne_of_lt $
+    (ennreal.sum_lt_top $ λ i hi, ennreal.rpow_ne_top_of_nonneg (pos p).le (edist_ne_top _ _)))
+  (λ f g,
+    have A : ∀ i, edist (f i) (g i) ^ p ≠ ⊤,
+      from λ i, ennreal.rpow_ne_top_of_nonneg (pos p).le (edist_ne_top _ _),
+    by simp only [edist_eq, dist_edist, ennreal.to_real_rpow, ← ennreal.to_real_sum (λ i _, A i)])
 
 /-- metric space instance on the product of finitely many metric spaces, using the `L^p` distance,
 and having as uniformity the product uniformity. -/
-instance [Π i, metric_space (α i)] : metric_space (pi_Lp p α) :=
-begin
-  /- we construct the instance from the emetric space instance to avoid checking again that the
-  uniformity is the same as the product uniformity, but we register nevertheless a nice formula
-  for the distance -/
-  have pos : 0 < p := lt_of_lt_of_le zero_lt_one fact_one_le_p.out,
-  refine emetric_space.to_metric_space_of_dist
-    (λf g, (∑ i, dist (f i) (g i) ^ p) ^ (1/p)) (λ f g, _) (λ f g, _),
-  { simp [pi_Lp.edist_eq, ennreal.rpow_eq_top_iff, asymm pos, pos,
-          ennreal.sum_eq_top_iff, edist_ne_top] },
-  { have A : ∀ (i : ι), i ∈ (finset.univ : finset ι) → edist (f i) (g i) ^ p ≠ ⊤ :=
-      λ i hi, by simp [edist_ne_top, pos.le],
-    simp [dist, -one_div, pi_Lp.edist_eq, ← ennreal.to_real_rpow,
-          ennreal.to_real_sum A, dist_edist] }
-end
+instance [Π i, metric_space (α i)] : metric_space (pi_Lp p α) := metric.of_t0_pseudo_metric_space _
 
 omit fact_one_le_p
 lemma dist_eq {p : ℝ} [fact (1 ≤ p)] {β : ι → Type*}
@@ -278,6 +243,14 @@ subtype.ext $ by { push_cast, exact dist_eq _ _ }
 
 include fact_one_le_p
 
+lemma lipschitz_with_equiv [Π i, pseudo_emetric_space (β i)] :
+  lipschitz_with 1 (pi_Lp.equiv p β) :=
+lipschitz_with_equiv_aux p β
+
+lemma antilipschitz_with_equiv [Π i, pseudo_emetric_space (β i)] :
+  antilipschitz_with ((fintype.card ι : ℝ≥0) ^ (1/p)) (pi_Lp.equiv p β) :=
+antilipschitz_with_equiv_aux p β
+
 /-- seminormed group instance on the product of finitely many normed groups, using the `L^p`
 norm. -/
 instance semi_normed_group [Π i, semi_normed_group (β i)] : semi_normed_group (pi_Lp p β) :=