Theorem: ballsCoverBalls (Carleson/HomogeneousType.lean)

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
r r' s : ℝ
hs : r' ≤ s * r
⊢ BallsCoverBalls X r' r (Np A s)
Tactic:
sorry
State after:
no goals