ball_covering

theorem ball_covering (hO : IsOpen O ∧ O ≠ univ) :    ∃ (c : ℕ → X) (r : ℕ → ℝ), (univ.PairwiseDisjoint fun i ↦ ball (c i) (r i)) ∧      ⋃ i, ball (c i) (3 * r i) = O ∧ (∀ i, 0 < r i → ¬Disjoint (ball (c i) (7 * r i)) Oᶜ) ∧      ∀ x ∈ O, {i | x ∈ ball (c i) (3 * r i)}.encard ≤ (2 ^ (6 * a) : ℕ) := by  obtain ⟨U, r', countU, pdU, U₃, U₇, Ubi⟩ := ball_covering' hO  obtain fU | iU := U.finite_or_infinite  · exact ball_covering_finite hO fU pdU U₃ U₇ Ubi  · let e := (countable_infinite_iff_nonempty_denumerable.mp ⟨countU, iU⟩).some.eqv    let c (i : ℕ) : X := (e.symm i).1    let r (i : ℕ) : ℝ := r' (c i)    refine ⟨c, r, fun i mi j mj hn ↦ ?_, ?_, fun i hi ↦ ?_, fun x mx ↦ ?_⟩    · have hic : c i ∈ U := by simp [c]      have hjc : c j ∈ U := by simp [c]      apply pdU hic hjc; simp_rw [c]; contrapose! hn      rwa [SetCoe.ext_iff, e.symm.apply_eq_iff_eq] at hn    · rw [← U₃]; apply subset_antisymm      · refine iUnion_subset fun i ↦ ?_        unfold r; convert subset_iUnion₂ (c i) _        · rfl        · simp_rw [c, Subtype.coe_prop]      · refine iUnion₂_subset fun x mx ↦ ?_        let i := e ⟨x, mx⟩; convert subset_iUnion _ i        simp_rw [r, c, i, Equiv.symm_apply_apply]    · unfold r at hi ⊢      have mi : c i ∈ U := by simp_rw [c, Subtype.coe_prop]      exact U₇ _ mi    · calc        _ = {u ∈ U | x ∈ ball u (3 * r' u)}.encard := by          set A := {i | x ∈ ball (c i) (3 * r i)}          set B := {u ∈ U | x ∈ ball u (3 * r' u)}          let f (i : A) : B := ⟨e.symm i, by            refine ⟨Subtype.coe_prop _, ?_⟩            have := i.2; simp_rw [A, mem_setOf_eq, r, c] at this; exact this⟩          let g (u : B) : A := ⟨e ⟨u.1, u.2.1⟩, by            simp_rw [A, r, c, mem_setOf_eq, Equiv.symm_apply_apply, u.2.2]⟩          let eqv : A ≃ B := ⟨f, g, fun i ↦ by simp [f, g], fun u ↦ by simp [f, g]⟩          exact encard_congr eqv        _ ≤ _ := Ubi x mx