Bounding ‖⨍_B f - f x‖ by ⨍⁻_B ‖f - f x‖ₑ in Mathlib

To pass from the ℝ≥0∞ Lebesgue-point statement ⨍⁻ y in B, ‖f y - f x‖ₑ → 0 to the Bochner average ⨍ y in B, f y → f x: first prove ⨍ f - f x = ⨍ (f y - f x) as a separate have using setAverage_sub (f := f) (g := fun _ ↦ f x) hf.integrableOn (integrableOn_const (C := f x) hfin) + simp only [Pi.sub_apply] + setAverage_const hpos hfin. Do NOT rw [← setAverage_const ..] in the main goal, because it rewrites every occurrence of f x, including inside the right-hand integrand. Also, integrableOn_const now has an auto-param hC that fails unless you pass (C := ...) explicitly. Then rw [edist_eq_enorm_sub, h1, setAverage_eq, enorm_smul, setLAverage_eq, ENNReal.div_eq_inv_mul], gcongr, and close with Real.enorm_eq_ofReal, measureReal_def, ENNReal.ofReal_inv_of_pos and enorm_integral_le_lintegral_enorm. Squeeze with tendsto_iff_edist_tendsto_0.