frequency_ball_cover

lemma frequency_ball_cover : (SetLike.coe Q.range) ⊆ ⋃ z ∈ 𝓩 I, ball_{I} z C4_2_1 := by  intro θ hθ  classical  obtain ⟨z, hz, hz'⟩ : ∃ z, z ∈ 𝓩 I ∧ ¬Disjoint (ball_{I} z C𝓩) (ball_{I} θ C𝓩) := by    by_contra! h    have hθ' : θ ∉ (𝓩 I : Set (Θ X)) := fun hθ' ↦ by      have := h _ hθ'; norm_num at this    let 𝓩' := insert θ (𝓩 I)    apply absurd (𝓩_max_card (I := I)) _; push Not; refine ⟨𝓩', ?_, ?_⟩    · simp_rw [𝓩', 𝓩_cands, Finset.mem_filter, Finset.mem_powerset, Finset.insert_subset_iff,        Finset.coe_insert, pairwiseDisjoint_insert_of_notMem hθ', Finset.mem_coe]      exact ⟨⟨hθ, 𝓩_subset⟩, 𝓩_pairwiseDisjoint, fun y hy ↦ (h y hy).symm⟩    · rw [Finset.card_insert_of_notMem hθ']; exact lt_add_one _  rw [not_disjoint_iff] at hz'; obtain ⟨z', h₁z', h₂z'⟩ := hz'  simp only [mem_iUnion, mem_ball, exists_prop, C𝓩, C4_2_1] at h₁z' h₂z' ⊢  use z, hz; linarith [dist_triangle_left (α := (WithFunctionDistance (c I) (D ^ s I / 4))) θ z z']