MeasureTheory.measureReal_ball_le_same'

lemma measureReal_ball_le_same' (x : X) {r t : ℝ} (ht : 0 < t) (h't : t ≤ 1) :    μ.real (ball x r) ≤ A * t ^ (- Real.logb 2 A) * μ.real (ball x (t * r)) := by  rcases lt_or_ge A 1 with hA | hA  · simp [eq_zero_of_isDoubling_lt_one μ hA]  have : r = t⁻¹ * (t * r) := (eq_inv_mul_iff_mul_eq₀ ht.ne').mpr rfl  apply (measureReal_ball_le_same x (inv_pos_of_pos ht) this.le).trans  gcongr  simp only [As, Real.logb_inv, NNReal.coe_pow]  have : t = 2 ^ (Real.logb 2 t) := by rw [Real.rpow_logb (by norm_num) (by norm_num) ht]  conv_rhs => rw [this]  have : (A : ℝ) = 2 ^ (Real.logb 2 (A : ℝ)) := by    rw [Real.rpow_logb (by norm_num) (by norm_num)]    apply zero_lt_one.trans_le hA  nth_rewrite 1 2 [this]  rw [← Real.rpow_mul zero_le_two, ← Real.rpow_natCast, ← Real.rpow_mul zero_le_two,    ← Real.rpow_add zero_lt_two]  apply (Real.rpow_le_rpow_left_iff one_lt_two).2  have : (⌈-Real.logb 2 t⌉₊ : ℝ) < -Real.logb 2 t + 1 := by    apply Nat.ceil_lt_add_one    simp only [Left.nonneg_neg_iff]    rw [Real.logb_nonpos_iff one_lt_two ht]    exact h't  calc  Real.logb 2 ↑A * ↑⌈-Real.logb 2 t⌉₊  _ ≤ Real.logb 2 ↑A * (-Real.logb 2 t + 1) := by    gcongr    exact Real.logb_nonneg one_lt_two hA  _ = _ := by ring