card_𝔒

lemma card_𝔒 (p' : 𝔓 X) {l : ℝ≥0} (hl : 2 ≤ l) : (𝔒 p' l).card ≤ ⌊2 ^ (4 * a) * l ^ a⌋₊ := by  have djO : PairwiseDisjoint (SetLike.coe (𝔒 p' l)) fun p'' ↦ ball_(p') (𝒬 p'') 5⁻¹ :=    fun p₁ mp₁ p₂ mp₂ hn ↦ by      simp_rw [𝔒, Finset.coe_filter, mem_setOf, Finset.mem_univ, true_and] at mp₁ mp₂      change Disjoint (ball_{𝓘 p'} (𝒬 p₁) 5⁻¹) (ball_{𝓘 p'} (𝒬 p₂) 5⁻¹)      conv => enter [1]; rw [← mp₁.1]      conv => enter [2]; rw [← mp₂.1]      exact cball_disjoint hn (mp₁.1.trans mp₂.1.symm)  have tO : ∀ p'' ∈ 𝔒 p' l,      ball_(p') (𝒬 p'') 5⁻¹ ⊆ ball_(p') (𝒬 p') (l + 6 / 5) := fun p'' mp'' ↦ by    apply ball_subset_ball'    simp_rw [𝔒, Finset.mem_filter_univ] at mp''    obtain ⟨x, mx₁, mx₂⟩ := not_disjoint_iff.mp mp''.2    replace mx₂ := _root_.subset_cball mx₂    rw [@mem_ball] at mx₁    calc      _ ≤ 5⁻¹ + (dist_{𝓘 p'} x (𝒬 p'') + dist_{𝓘 p'} x (𝒬 p')) :=        add_le_add_right (dist_triangle_left ..) _      _ ≤ 5⁻¹ + (1 + l) := by        gcongr        · rw [← mp''.1]; exact mx₂.le        · exact mx₁.le      _ = _ := by rw [inv_eq_one_div, ← add_assoc, add_comm _ l.toReal]; norm_num  have vO : CoveredByBalls (ball_(p') (𝒬 p') (l + 6 / 5)) ⌊2 ^ (4 * a) * l ^ a⌋₊ 5⁻¹ := by    apply (ballsCoverBalls_iterate (show 0 < 5⁻¹ by positivity) (𝒬 p')).mono_nat    calc      _ ≤ (defaultA a) ^ ⌊4 + Real.logb 2 l⌋₊ :=        pow_le_pow_right₀ Nat.one_le_two_pow (ceil_log2_le_floor_four_add_log2 hl)      _ ≤ ⌊(defaultA a : ℝ) ^ (4 + Real.logb 2 l)⌋₊ := by        apply Nat.le_floor; rw [Nat.cast_pow, ← Real.rpow_natCast]        refine Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast Nat.one_le_two_pow)          (Nat.floor_le ?_)        calc          _ ≥ 4 + Real.logb 2 2 :=            add_le_add_right (Real.logb_le_logb_of_le one_lt_two zero_lt_two hl) _          _ ≥ _ := by rw [Real.logb_self_eq_one one_lt_two]; norm_num      _ = _ := by        rw [Nat.cast_pow, Nat.cast_ofNat, ← Real.rpow_natCast, ← Real.rpow_mul zero_le_two,          mul_comm, add_mul, Real.rpow_add zero_lt_two, show (4 : ℝ) * a = (4 * a : ℕ) by simp,          Real.rpow_natCast, Real.rpow_mul zero_le_two, Real.rpow_natCast,          Real.rpow_logb zero_lt_two one_lt_two.ne' (by positivity)]        rfl  obtain ⟨(T : Finset (Θ X)), cT, uT⟩ := vO  refine (Finset.card_le_card_of_forall_subsingleton (fun p'' t ↦ 𝒬 p'' ∈ ball_(p') t 5⁻¹)      (fun p'' mp'' ↦ ?_) (fun t _ o₁ mo₁ o₂ mo₂ ↦ ?_)).trans cT  · have := (tO _ mp'').trans uT (mem_ball_self (by positivity))    rwa [mem_iUnion₂, bex_def] at this  · simp_rw [mem_setOf_eq] at mo₁ mo₂    exact djO.elim mo₁.1 mo₂.1 (not_disjoint_iff.mpr ⟨t, mem_ball_comm.mp mo₁.2, mem_ball_comm.mp mo₂.2⟩)