MeasureTheory.measureReal_ball_le_same

lemma measureReal_ball_le_same (x : X) {r s r' : ℝ} (hsp : 0 < s) (hs : r' ≤ s * r) :    μ.real (ball x r') ≤ As A s * μ.real (ball x r) := by  have hz := measure_ball_le_same (μ := μ) x hsp hs  have hbr': μ (ball x r') ≠ ⊤ := by finiteness  have hbr: μ (ball x r) ≠ ⊤ := by finiteness  have hAs : (As A s: ℝ≥0∞) ≠ ⊤ := by finiteness  rw [← ENNReal.ofReal_toReal hbr, ← ENNReal.ofReal_toReal hbr',    ← ENNReal.ofReal_toReal hAs, ← ENNReal.ofReal_mul] at hz  · simp only [coe_toReal] at hz    rw [← ENNReal.ofReal_le_ofReal_iff]    · exact hz    positivity  · simp only [coe_toReal, zero_le_coe]