ball_covering_finite

lemma ball_covering_finite (hO : IsOpen O ∧ O ≠ univ) {U : Set X} {r' : X → ℝ} (fU : U.Finite)    (pdU : U.PairwiseDisjoint fun c ↦ ball c (r' c)) (U₃ : ⋃ c ∈ U, ball c (3 * r' c) = O)    (U₇ : ∀ c ∈ U, ¬Disjoint (ball c (7 * r' c)) Oᶜ)    (Ubi : ∀ x ∈ O, {c ∈ U | x ∈ ball c (3 * r' c)}.encard ≤ (2 ^ (6 * a) : ℕ)) :    ∃ (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  lift U to Finset X using fU  obtain ⟨p, -⟩ := (ne_univ_iff_exists_notMem _).mp hO.2  let e := U.equivFin  let c (i : ℕ) : X := if hi : i < U.card then (e.symm ⟨_, hi⟩).1 else p  let r (i : ℕ) : ℝ := if hi : i < U.card then r' (c i) else 0  refine ⟨c, r, fun i mi j mj hn ↦ ?_, ?_, fun i hi ↦ ?_, fun x mx ↦ ?_⟩  · change Disjoint (ball _ _) (ball _ _)    by_cases hi : i < U.card; swap    · simp_rw [r, hi, dite_false, ball_zero, empty_disjoint]    have hic : c i ∈ U := by simp [c, hi]    by_cases hj : j < U.card; swap    · simp_rw [r, hj, dite_false, ball_zero, disjoint_empty]    have hjc : c j ∈ U := by simp [c, hj]    simp_rw [r, hi, hj, dite_true]; apply pdU hic hjc    simp_rw [c, hi, hj, dite_true]; contrapose! hn    rwa [SetCoe.ext_iff, e.symm.apply_eq_iff_eq, Fin.mk.injEq] at hn  · rw [← U₃]; apply subset_antisymm    · refine iUnion_subset fun i ↦ ?_      unfold r; split_ifs with hi      · convert subset_iUnion₂ (c i) _        · rfl        · simp_rw [c, hi, dite_true, Subtype.coe_prop]      · simp    · refine iUnion₂_subset fun x mx ↦ ?_      let i := e ⟨x, mx⟩; convert subset_iUnion _ i.1      simp_rw [r, c, i.2, dite_true, i, Fin.eta, Equiv.symm_apply_apply]  · unfold r at hi ⊢; split_ifs with hi'    · simp_rw [Finset.mem_coe] at U₇      have mi : c i ∈ U := by simp_rw [c, hi', dite_true]; exact Finset.coe_mem _      exact U₇ _ mi    · simp_rw [hi', dite_false, lt_self_iff_false] at hi  · calc      _ = {i | ¬i < U.card ∧ x ∈ ball (c i) (3 * r i)}.encard +          {i | i < U.card ∧ x ∈ ball (c i) (3 * r i)}.encard := by        have : {i | x ∈ ball (c i) (3 * r i)} =            {i | ¬ i < U.card ∧ x ∈ ball (c i) (3 * r i)} ∪                {i | i < U.card ∧ x ∈ ball (c i) (3 * r i)} := by          ext i; refine ⟨fun hx ↦ ?_, fun h ↦ ?_⟩          · by_cases hi : i < U.card            exacts [Or.inr ⟨hi, hx⟩, Or.inl ⟨hi, hx⟩]          · rcases h with ⟨_, hx⟩ | ⟨_, hx⟩ <;> exact hx        rw [← encard_union_eq]        · congr        · exact disjoint_left.mpr fun i mi₁ mi₂ ↦ mi₁.1 mi₂.1      _ = 0 + {u ∈ SetLike.coe U | x ∈ ball u (3 * r' u)}.encard := by        congr        · simp_rw [encard_eq_zero, eq_empty_iff_forall_notMem, mem_setOf_eq, not_and]; intro i hi          simp [r, hi]        · set A := {i | i < U.card ∧ x ∈ ball (c i) (3 * r i)}          set B := {u ∈ SetLike.coe U | x ∈ ball u (3 * r' u)}          let f (i : A) : B := ⟨e.symm ⟨i.1, i.2.1⟩, by            refine ⟨Subtype.coe_prop _, ?_⟩            have := i.2.2; simp_rw [r, c, i.2.1, dite_true] at this; exact this⟩          let g (u : B) : A := ⟨e ⟨u.1, u.2.1⟩, by            simp_rw [A, r, c, mem_setOf_eq, Fin.is_lt, dite_true, Fin.eta, Equiv.symm_apply_apply,              u.2.2, true_and]⟩          let eqv : A ≃ B := ⟨f, g, fun i ↦ by simp [f, g], fun u ↦ by simp [f, g]⟩          exact encard_congr eqv      _ ≤ _ := by rw [zero_add]; exact Ubi x mx