ball_covering_bounded_intersection

lemma ball_covering_bounded_intersection    (hO : IsOpen O ∧ O ≠ univ) {U : Set X} (countU : U.Countable)    (pdU : U.PairwiseDisjoint fun c ↦ ball c ((depth O c).toReal / 6)) {x : X} (mx : x ∈ O) :    {c ∈ U | x ∈ ball c (3 * ((depth O c).toReal / 6))}.encard ≤ (2 ^ (6 * a) : ℕ) := by  set V := {c ∈ U | x ∈ ball c (3 * ((depth O c).toReal / 6))}  have vbpos : 0 < volume (ball x ((depth O x).toReal / 6)) := by    refine measure_ball_pos volume x (div_pos ?_ (by norm_num))    rw [toReal_pos_iff, depth_pos_iff_mem hO.1, depth_lt_top_iff_ne_univ]; exact ⟨mx, hO.2⟩  have vbnt : volume (ball x ((depth O x).toReal / 6)) ≠ ⊤ := by finiteness  rw [← ENat.toENNReal_le, Nat.cast_pow, Nat.cast_ofNat, ENat.toENNReal_pow, ENat.toENNReal_ofNat,    ← ENNReal.mul_le_mul_iff_left vbpos.ne' vbnt]  have Aeq : (2 : ℝ≥0∞) ^ (3 * a) = defaultA a ^ 3 := by    rw [defaultA, Nat.cast_pow, Nat.cast_ofNat, ← pow_mul, mul_comm]  calc    _ = ∑' c : V, volume (ball x ((depth O x).toReal / 6)) := (ENNReal.tsum_set_const _ _).symm    _ ≤ ∑' c : V, volume (ball c.1 (8 * (depth O c.1).toReal / 6)) :=      ENNReal.tsum_le_tsum fun ⟨u, mu, xu⟩ ↦        measure_mono (ball_subset_ball' (depth_bound_2 hO.2 xu))    _ ≤ 2 ^ (3 * a) * ∑' v : V, volume (ball v.1 ((depth O v.1).toReal / 6)) := by      rw [← ENNReal.tsum_mul_left]; refine ENNReal.tsum_le_tsum fun ⟨u, mu, xu⟩ ↦ ?_      rw [mul_div_assoc, show (8 : ℝ) = 2 ^ 3 by norm_num, Aeq]      apply measure_ball_two_le_same_iterate    _ = 2 ^ (3 * a) * volume (⋃ v : V, ball v.1 ((depth O v.1).toReal / 6)) := by      have VsU : V ⊆ U := sep_subset ..      haveI : Countable V := by rw [countable_coe_iff]; exact countU.mono VsU      congr 1      refine (measure_iUnion (fun ⟨v₁, mv₁⟩ ⟨v₂, mv₂⟩ hn ↦ ?_) (fun _ ↦ measurableSet_ball)).symm      rw [ne_eq, Subtype.mk.injEq] at hn      exact pdU (VsU mv₁) (VsU mv₂) hn    _ ≤ 2 ^ (3 * a) * volume (ball x (8 * (depth O x).toReal / 6)) := by      gcongr; exact iUnion_subset fun ⟨u, mu, xu⟩ ↦ ball_subset_ball' (depth_bound_3 hO.2 xu)    _ ≤ _ := by      rw [show 6 * a = 3 * a + 3 * a by lia, pow_add, mul_assoc]; gcongr      rw [mul_div_assoc, show (8 : ℝ) = 2 ^ 3 by norm_num, Aeq]      apply measure_ball_two_le_same_iterate