Abs ball Average sub six Ball Average le

lemma abs_ballAverage_sub_sixBallAverage_le    {u : E → ℝ} {x₀ : E} {r M : ℝ} (hr : 0 < r)    (hu_int : IntegrableOn u (Metric.ball x₀ (6 * r)) volume)    (hu_bmo : (⨍ x in Metric.ball x₀ (6 * r),      ‖u x - ⨍ y in Metric.ball x₀ (6 * r), u y ∂volume‖ ∂volume) ≤ M) :    |⨍ x in Metric.ball x₀ r, u x ∂volume -      ⨍ x in Metric.ball x₀ (6 * r), u x ∂volume| ≤ 6 ^ d * M := by  have h6r : 0 < 6 * r := by linarith  have hsub : Metric.ball x₀ r ⊆ Metric.ball x₀ (6 * r) :=    Metric.ball_subset_ball (by linarith)  have hle := abs_subballAverage_sub_ballAverage_le h6r hr hsub (hu_int)  have hratio : (6 * r / r) ^ d = (6 : ℝ) ^ d := by    rw [mul_div_cancel_of_imp]    exact fun h => absurd h (ne_of_gt hr)  calc |⨍ x in Metric.ball x₀ r, u x ∂volume - ⨍ x in Metric.ball x₀ (6 * r), u x ∂volume|        ≤ (6 * r / r) ^ d * (⨍ z in Metric.ball x₀ (6 * r), ‖u z - ⨍ w in Metric.ball x₀ (6 * r), u w ∂volume‖ ∂volume) := hle      _ = 6 ^ d * (⨍ z in Metric.ball x₀ (6 * r), ‖u z - ⨍ w in Metric.ball x₀ (6 * r), u w ∂volume‖ ∂volume) := by rw [hratio]      _ ≤ 6 ^ d * M := by exact mul_le_mul_of_nonneg_left hu_bmo (by positivity)