Construction.ball_subset_Ω₁

lemma ball_subset_Ω₁ (p : 𝔓 X) : ball_(p) (𝒬 p) C𝓩 ⊆ Ω₁ p := by  rw [Ω₁, Ω₁_aux]; set z := p.2  simp_rw [Fin.eta, Equiv.symm_apply_apply]  set k := (Finite.equivFin ↑(𝓩 p.1)) z with h'k  simp_rw [k.2, dite_true]  change ball_{p.1} z.1 C𝓩 ⊆ _ \ ⋃ i < k.1, Ω₁_aux p.1 i  refine subset_sdiff.mpr ⟨subset_sdiff.mpr ⟨ball_subset_ball (by norm_num), ?_⟩, ?_⟩  · rw [disjoint_iUnion₂_right]; intro i hi; rw [mem_sdiff_singleton] at hi    exact 𝓩_pairwiseDisjoint z.coe_prop hi.1 hi.2.symm  · rw [disjoint_iUnion₂_right]; intro i hi    let z' := (Finite.equivFin ↑(𝓩 p.1)).symm ⟨i, by lia⟩    have zn : z ≠ z' := by simp only [ne_eq, Equiv.eq_symm_apply, z']; exact Fin.ne_of_gt hi    simpa [z'] using disjoint_ball_Ω₁_aux p.1 z'.2 z.2 (Subtype.coe_ne_coe.mpr zn.symm)