feat(Normed/Group): add nndist_one_right etc (#17954)

Add

- `nndist_one_right`, `nndist_zero_right`, `nndist_one_left`, `nndist_zero_left`;
- `edist_one_right`, `edist_zero_right`, `edist_one_left`, `edist_zero_left`.

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -635,6 +635,13 @@ theorem nndist_eq_nnnorm_div (a b : E) : nndist a b = ‖a / b‖₊ :=
 
 alias nndist_eq_nnnorm := nndist_eq_nnnorm_sub
 
+@[to_additive (attr := simp)]
+theorem nndist_one_right (a : E) : nndist a 1 = ‖a‖₊ := by simp [nndist_eq_nnnorm_div]
+
+@[to_additive (attr := simp)]
+theorem edist_one_right (a : E) : edist a 1 = ‖a‖₊ := by
+  rw [edist_nndist, nndist_one_right]
+
 @[to_additive (attr := simp) nnnorm_zero]
 theorem nnnorm_one' : ‖(1 : E)‖₊ = 0 :=
   NNReal.eq norm_one'
@@ -653,6 +660,13 @@ theorem nnnorm_mul_le' (a b : E) : ‖a * b‖₊ ≤ ‖a‖₊ + ‖b‖₊ :=
 theorem nnnorm_inv' (a : E) : ‖a⁻¹‖₊ = ‖a‖₊ :=
   NNReal.eq <| norm_inv' a
 
+@[to_additive (attr := simp)]
+theorem nndist_one_left (a : E) : nndist 1 a = ‖a‖₊ := by simp [nndist_eq_nnnorm_div]
+
+@[to_additive (attr := simp)]
+theorem edist_one_left (a : E) : edist 1 a = ‖a‖₊ := by
+  rw [edist_nndist, nndist_one_left]
+
 open scoped symmDiff in
 @[to_additive]
 theorem nndist_mulIndicator (s t : Set α) (f : α → E) (x : α) :

Mathlib/MeasureTheory/Function/L1Space.lean

@@ -1375,12 +1375,10 @@ theorem edist_toL1_toL1 (f g : α → β) (hf : Integrable f μ) (hg : Integrabl
     ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self, ite_false]
   simp [edist_eq_coe_nnnorm_sub]
 
-@[simp]
 theorem edist_toL1_zero (f : α → β) (hf : Integrable f μ) :
     edist (hf.toL1 f) 0 = ∫⁻ a, edist (f a) 0 ∂μ := by
-  simp only [toL1, Lp.edist_toLp_zero, eLpNorm, one_ne_zero, eLpNorm', one_toReal, ENNReal.rpow_one,
-    ne_eq, not_false_eq_true, div_self, ite_false]
-  simp [edist_eq_coe_nnnorm]
+  simp only [edist_zero_right, Lp.nnnorm_coe_ennreal, toL1_eq_mk, eLpNorm_aeeqFun]
+  apply eLpNorm_one_eq_lintegral_nnnorm
 
 variable {𝕜 : Type*} [NormedRing 𝕜] [Module 𝕜 β] [BoundedSMul 𝕜 β]