Construction.iUnion_ball_subset_iUnion_Ω₁

lemma iUnion_ball_subset_iUnion_Ω₁ : ⋃ z ∈ 𝓩 I, ball_{I} z C4_2_1 ⊆ ⋃ f : 𝓩 I, Ω₁ ⟨I, f⟩ := by  rw [iUnion₂_subset_iff]; intro z mz (ϑ : Θ X) mϑ  set f := Finite.equivFin (𝓩 I) with hf  by_cases h : ∃ y ∈ 𝓩 I, ϑ ∈ ball_{I} y C𝓩  · obtain ⟨z', mz', hz'⟩ := h    exact subset_iUnion_of_subset _ subset_rfl (ball_subset_Ω₁ ⟨I, ⟨z', mz'⟩⟩ hz')  · let L := {k : Fin (Nat.card (𝓩 I)) | ϑ ∈ ball_{I} (f.symm k).1 C4_2_1}    have Ln : L.Nonempty := by use f ⟨z, mz⟩; rwa [mem_setOf, Equiv.symm_apply_apply]    obtain ⟨k, mem_k, hk⟩ := L.exists_min_image id L.toFinite Ln    simp_rw [L, mem_setOf_eq] at mem_k    simp only [id_eq] at hk    have q : ∀ i < k, ϑ ∉ Ω₁_aux I i := by      by_contra! h; obtain ⟨i, li, hi⟩ := h      have := Ω₁_subset_ball ⟨I, f.symm i⟩      simp_rw [Ω₁, ← hf, Equiv.apply_symm_apply] at this      replace this : ϑ ∈ ball_{I} (f.symm i).1 C4_2_1 := this hi      replace this : i ∈ L := by simp only [L, mem_setOf_eq, this]      exact absurd (hk i this) (not_le.mpr li)    rw [mem_iUnion]; use f.symm k; rw [Ω₁, Ω₁_aux]; dsimp only    rw [Equiv.apply_symm_apply]; simp_rw [k.2]; rw [dite_true, mem_sdiff, mem_sdiff]    refine ⟨⟨mem_k, ?_⟩, ?_⟩    · rw [mem_iUnion₂]; push Not at h ⊢; exact fun i mi ↦ h i mi.1    · rw [mem_iUnion₂]; push Not; exact fun i mi ↦ q ⟨i, mi.trans k.2⟩ mi