Construction.Ω_RFD

lemma Ω_RFD {p q : 𝔓 X} (h𝓘 : 𝓘 p ≤ 𝓘 q) : Disjoint (Ω p) (Ω q) ∨ Ω q ⊆ Ω p := by  by_cases h : 𝔰 q ≤ 𝔰 p  · rw [or_iff_not_imp_left]; intro hi    obtain ⟨I, y⟩ := p    obtain ⟨J, z⟩ := q    have hij : I = J := le_antisymm h𝓘 (Grid.le_dyadic h h𝓘 le_rfl)    have k := Ω_disjoint (p := ⟨I, y⟩) (p' := ⟨J, z⟩)    replace k : (⟨I, y⟩ : 𝔓 X) = ⟨J, z⟩ := by tauto    rw [k]  · obtain ⟨J, sJ, lbJ, ubJ⟩ :=      Grid.exists_sandwiched h𝓘 (𝔰 q - 1) (by change 𝔰 p ≤ _ ∧ _ ≤ 𝔰 q; lia)    have : q.2.1 ∈ ⋃ z ∈ 𝓩 J, ball_{J} z C4_2_1 :=      ((Finset.coe_subset.mpr 𝓩_subset).trans frequency_ball_cover) q.2.2    rw [mem_iUnion₂] at this; obtain ⟨z', mz', dz⟩ := this    have zi' : ball_{J} z' C4_2_1 ⊆ ⋃ z ∈ 𝓩 J, ball_{J} z C4_2_1 :=      subset_iUnion₂_of_subset z' mz' (subset_refl _)    replace zi : ↑q.2 ∈ ⋃ f, Ω₁ ⟨J, f⟩ :=      mem_of_mem_of_subset dz <| zi'.trans iUnion_ball_subset_iUnion_Ω₁    clear! z'    rw [mem_iUnion] at zi; obtain ⟨a, ma⟩ := zi -- Paper's `q'` is `⟨J, a⟩`    have nmaxJ : ¬IsMax J := by      by_contra maxJ; rw [Grid.isMax_iff] at maxJ      rw [maxJ, show s topCube = S from s_topCube (X := X)] at sJ      have : 𝔰 q ≤ S := scale_mem_Icc.2      lia    have succJ : J.succ = q.1 := (Grid.succ_def nmaxJ).mpr ⟨ubJ, by change 𝔰 q = _; lia⟩    have key : Ω q ⊆ Ω ⟨J, a⟩ := by      nth_rw 2 [Ω]; simp only [nmaxJ, dite_false]; intro ϑ mϑ; right; rw [mem_iUnion₂]      refine ⟨q.2, ?_, ?_⟩      · rw [succJ]; exact ⟨q.2.2, ma⟩      · change ϑ ∈ Ω ⟨q.1, q.2⟩ at mϑ; convert! mϑ    let q' : 𝔓 X := ⟨J, a⟩    change 𝓘 p ≤ 𝓘 q' at lbJ    rcases Ω_RFD lbJ with c | c    · exact Or.inl (disjoint_of_subset_right key c)    · exact Or.inr (key.trans c)