Antichain.I_p_subset_union_L

lemma I_p_subset_union_L (p : 𝔄' 𝔄 ϑ N) : (𝓘 (p : 𝔓 X) : Set X) ⊆ ⋃ (L ∈ 𝓛 𝔄 ϑ N), L := by  calc (𝓘 (p : 𝔓 X) : Set X)    _ ⊆ ⋃ (I ∈ {I : Grid X | s I = -S ∧ I ≤ 𝓘 (p : 𝔓 X)}), I := by      intro x hx      -- Apply (2.0.7)      obtain ⟨I, hI, hxI⟩ := Grid.exists_containing_subcube (i := 𝓘 (p : 𝔓 X)) (-S)        (by simp [mem_Icc, scale_mem_Icc.1]) hx      have hsI : s I ≤ s (𝓘 (p : 𝔓 X)) := hI ▸ scale_mem_Icc.1      simp only [Grid.le_def, mem_setOf_eq, mem_iUnion, exists_prop]      exact ⟨I, ⟨hI, Or.resolve_right (GridStructure.fundamental_dyadic' hsI)        (not_disjoint_iff.mpr ⟨x, hxI, hx⟩), hsI⟩, hxI⟩    _ ⊆ ⋃ (L ∈ 𝓛 𝔄 ϑ N), L := by      intro x hx      simp only [mem_iUnion] at hx ⊢      obtain ⟨I, ⟨hsI, hI⟩, hxI⟩ := hx      simp only [𝓛, Subtype.exists, exists_prop, Subtype.forall]      exact ⟨I, ⟨⟨p, p.2, hI⟩, fun _ _ hqI ↦ le_antisymm (hsI ▸ hqI.2) scale_mem_Icc.1⟩, hxI⟩