Theorem: volume_ball_le_of_subset (Carleson/HomogeneousType.lean)

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x' x : X
r r' s : ℝ
hs : r' ≤ s * r
hr : ball x' r ⊆ ball x r'
⊢ volume.real (ball x (2 * r)) ≤ Ai A s * volume.real (ball x' r)
Tactic:
sorry
State after:
no goals