Construction.Ω_biUnion

lemma Ω_biUnion {I : Grid X} : SetLike.coe Q.range ⊆ ⋃ p ∈ 𝓘 ⁻¹' ({I} : Set (Grid X)), Ω p := by  induction I using Grid.induction with  | base I maxI =>    intro ϑ mϑ; push _ ∈ _    have l := ((frequency_ball_cover (I := I)).trans iUnion_ball_subset_iUnion_Ω₁) mϑ    rw [mem_iUnion] at l; obtain ⟨z, mz⟩ := l; use ⟨I, z⟩    exact ⟨rfl, by rw [Ω]; simp only [maxI, dite_true, mz]⟩  | ind I nmaxI ih =>    intro ϑ mϑ    replace ih := ih mϑ    push _ ∈ _ at ih ⊢    obtain ⟨⟨J, z⟩, (rfl : J = I.succ), h⟩ := ih    have : z.1 ∈ ⋃ z ∈ 𝓩 I, ball_{I} z C4_2_1 :=      ((Finset.coe_subset.mpr 𝓩_subset).trans frequency_ball_cover) z.2    rw [mem_iUnion₂] at this; obtain ⟨z', mz', dz⟩ := this    have zi : ball_{I} z' C4_2_1 ⊆ ⋃ z ∈ 𝓩 I, ball_{I} z C4_2_1 :=      subset_iUnion₂_of_subset z' mz' (subset_refl _)    replace zi : ↑z ∈ ⋃ f, Ω₁ ⟨I, f⟩ :=      mem_of_mem_of_subset dz <| zi.trans iUnion_ball_subset_iUnion_Ω₁    rw [mem_iUnion] at zi; obtain ⟨z'', mz''⟩ := zi    use ⟨I, z''⟩, rfl    rw [Ω]; simp only [nmaxI, dite_false, mem_union]; right    rw [mem_iUnion₂]; use z.1, ⟨z.2, mz''⟩, h