ball_covering'

lemma ball_covering' (hO : IsOpen O ∧ O ≠ univ) :    ∃ (U : Set X) (r : X → ℝ), U.Countable ∧ (U.PairwiseDisjoint fun c ↦ ball c (r c)) ∧      ⋃ c ∈ U, ball c (3 * r c) = O ∧ (∀ c ∈ U, ¬Disjoint (ball c (7 * r c)) Oᶜ) ∧      ∀ x ∈ O, {c ∈ U | x ∈ ball c (3 * r c)}.encard ≤ (2 ^ (6 * a) : ℕ) := by  let W : Set (Set X) := {U | U ⊆ O ∧ U.PairwiseDisjoint fun c ↦ ball c ((depth O c).toReal / 6)}  obtain ⟨U, maxU⟩ : ∃ U, Maximal (· ∈ W) U := by    refine zorn_subset _ fun U sU cU ↦ ⟨⋃₀ U, ?_, fun _ ↦ subset_sUnion_of_mem⟩    simp only [W, sUnion_subset_iff, mem_setOf_eq]    exact ⟨fun u hu ↦ (sU hu).1, (pairwiseDisjoint_sUnion cU.directedOn).2 fun u hu ↦ (sU hu).2⟩  have countU : U.Countable := by    refine maxU.1.2.countable_of_isOpen (fun _ _ ↦ isOpen_ball) (fun u mu ↦ ?_)    rw [nonempty_ball]; refine div_pos (toReal_pos ?_ ?_) (by norm_num)    · rw [← EReal.coe_ennreal_pos_iff_ne_zero, EReal.coe_ennreal_pos, depth_pos_iff_mem hO.1]      exact maxU.1.1 mu    · rw [← lt_top_iff_ne_top, depth_lt_top_iff_ne_univ]; exact hO.2  refine ⟨U, fun c ↦ (depth O c).toReal / 6, countU, maxU.1.2, ?_, fun c mc ↦ ?_, fun x mx ↦ ?_⟩  · refine subset_antisymm (fun x mx ↦ ?_) (fun x mx ↦ ?_)    · simp only [mem_iUnion₂] at mx; obtain ⟨c, mc, mx⟩ := mx      refine (le_depth_iff_subset.mp ?_) mx      rw [← mul_comm_div, ENNReal.ofReal_mul (by norm_num),        ENNReal.ofReal_toReal (depth_lt_top_iff_ne_univ.mpr hO.2).ne]      nth_rw 2 [← one_mul (depth O _)]; gcongr; norm_num    · rw [mem_iUnion₂]      by_cases mxU : x ∈ U      · refine ⟨x, mxU, mem_ball_self ?_⟩        simp only [Nat.ofNat_pos, mul_pos_iff_of_pos_left, div_pos_iff_of_pos_right, toReal_pos_iff]        rw [depth_pos_iff_mem hO.1, depth_lt_top_iff_ne_univ]; exact ⟨mx, hO.2⟩      obtain ⟨i, mi, hi⟩ : ∃ i ∈ U,          ¬Disjoint (ball x ((depth O x).toReal / 6)) (ball i ((depth O i).toReal / 6)) := by        by_contra! h; apply absurd maxU; simp_rw [not_maximal_iff maxU.1]        exact ⟨insert x U, ⟨insert_subset mx maxU.1.1, maxU.1.2.insert_of_notMem mxU h⟩,          ssubset_insert mxU⟩      use i, mi, depth_bound_1 hO.2 hi  · rw [← depth_lt_iff_not_disjoint, ← mul_comm_div, ENNReal.ofReal_mul (by norm_num),      ENNReal.ofReal_toReal (depth_lt_top_iff_ne_univ.mpr hO.2).ne]    nth_rw 1 [← one_mul (depth O _)]    have dpos := (depth_pos_iff_mem hO.1).mpr (maxU.1.1 mc)    have dlt := (depth_lt_top_iff_ne_univ (x := c)).mpr hO.2    exact ENNReal.mul_lt_mul_left dpos.ne' dlt.ne (by norm_num)  · exact ball_covering_bounded_intersection hO countU maxU.1.2 mx