cover_big_ball

lemma cover_big_ball (k : ℤ) : ball o (4 * D ^ S - D ^ k) ⊆ ⋃ y ∈ Yk X k, ball y (2 * D ^ k) := by  intro y hy  have : ∃ z ∈ Yk X k, ¬Disjoint (ball y (D^k:ℝ)) (ball z (D^k:ℝ)) := by    by_contra hcon    apply hcon    push Not at hcon    suffices hmem : y ∈ Yk X k by      use y, hmem      rw [disjoint_self, bot_eq_empty, ball_eq_empty, not_le]      positivity [by exact_mod_cast realD_pos a]    suffices (Yk X k) ∪ {y} = Yk X k by      rwa [union_singleton, insert_eq_self] at this    apply Yk_maximal    · rw [union_subset_iff, singleton_subset_iff]      use Yk_subset k    · rw [pairwiseDisjoint_union]      use Yk_pairwise k      simpa using fun z hz _ ↦ (hcon z hz).symm    · exact subset_union_left    intro h    rw [h]    left    exact o_mem_Yk_S  obtain ⟨z,hz,hz'⟩ := this  push _ ∈ _  use z, hz  rw [Set.not_disjoint_iff] at hz'  obtain ⟨x,hx,hx'⟩ := hz'  rw [mem_ball, dist_comm] at hx  rw [two_mul]  exact (dist_triangle y x z).trans_lt (add_lt_add hx hx')