Theorem: volume_ball_le_of_dist_le (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 d : ℝ
hs : r' ≤ s * r
hd : dist x x' ≤ d * r
⊢ volume.real (ball x' r') ≤ Ad A s d * volume.real (ball x r)
Tactic:
sorry
State after:
no goals