TileStructure.Forest.union_𝓙₅

lemma union_𝓙₅ (hu₁ : u₁ ∈ t) (hu₂ : u₂ ∈ t) (hu : u₁ ≠ u₂) (h2u : 𝓘 u₁ ≤ 𝓘 u₂) :    ⋃ J ∈ 𝓙₅ t u₁ u₂, (J : Set X) = 𝓘 u₁ := by  apply Set.Subset.antisymm  · intros x hx    simp only [mem_iUnion] at hx    rcases hx with ⟨cube, ⟨_, interval⟩, h⟩    exact Set.mem_of_mem_of_subset h interval.left  · intros x hx    have existsCube : x ∈ ⋃ J ∈ 𝓙 (t.𝔖₀ u₁ u₂), (J : Set X) := 𝓘_subset_iUnion_𝓙_𝔖₀ hx    simp only [mem_iUnion, exists_prop] at existsCube    rcases existsCube with ⟨cube, cube_in_𝓙, xInCube⟩    simp only [mem_iUnion, exists_prop]    have notDisjoint := Set.not_disjoint_iff.mpr ⟨x, xInCube, hx⟩    have cubeIn𝓙₀ : cube ∈ 𝓙₀ (t.𝔖₀ u₁ u₂) := mem_of_mem_inter_left cube_in_𝓙    cases cubeIn𝓙₀ with    | inl west =>      refine ⟨cube, ?_, xInCube⟩      unfold 𝓙₅      rw [inter_def, mem_setOf_eq]      refine ⟨cube_in_𝓙, ?_⟩      simp only [mem_Iic, Grid.le_def]      have smaller := calc s cube        _ = -S := west        _ ≤ s (𝓘 u₁) := (mem_Icc.mp (scale_mem_Icc (i := 𝓘 u₁))).left      refine ⟨?_, smaller⟩      cases GridStructure.fundamental_dyadic' smaller with      | inl subset => exact subset      | inr disjoint => exact False.elim (notDisjoint disjoint)    | inr east =>      obtain ⟨p, belongs⟩ := t.nonempty' hu₁      by_contra! contr      have white := calc (𝓘 p : Set X)        _ ⊆ 𝓘 u₁ := (𝓘_le_𝓘 t hu₁ belongs).1        _ ⊆ cube := by          apply subset_of_notMem_Iic_of_not_disjoint cube          · have notIn : cube ∉ t.𝓙₅ u₁ u₂ := fun a ↦ contr cube a xInCube            rw [𝓙₅, inter_def, Set.mem_setOf_eq, not_and_or] at notIn            exact Or.resolve_left notIn (Set.not_notMem.mpr cube_in_𝓙)          · exact notDisjoint        _ ⊆ ball (c cube) (4 * D ^ s cube) := by          exact Grid_subset_ball (i := cube)        _ ⊆ ball (c cube) (100 * D ^ (s cube + 1)) := by          intro y xy          rw [ball, mem_setOf_eq] at xy ⊢          exact gt_trans (calculation_16 (X := X) (s := s cube)) xy      have black : ¬↑(𝓘 p) ⊆ ball (c cube) (100 * D ^ (s cube + 1)) := by        have in_𝔖₀ := 𝔗_subset_𝔖₀ (hu₁ := hu₁) (hu₂ := hu₂) (hu := hu) (h2u := h2u)        rw [subset_def] at in_𝔖₀        exact east p (in_𝔖₀ p belongs)      contradiction