Theorem: card_le_of_le_dist (Carleson/HomogeneousType.lean)

State before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r r' s : ℝ
P : Set X
hs : r' ≤ s * r
hP : P ⊆ ball x r'
h2P : ∀ (x y : X), x ∈ P → y ∈ P → x ≠ y → r ≤ dist x y
⊢ P.Finite ∧ Nat.card ↑P ≤ Np A s
Tactic:
sorry
State after:
no goals