TileStructure.Forest.union_𝓙₆

lemma union_𝓙₆ (hu₁ : u₁ ∈ t) : ⋃ J ∈ 𝓙₆ t u₁, (J : Set X) = 𝓘 u₁ := by  refine subset_antisymm ?_ fun x hx ↦ ?_  · refine iUnion₂_subset_iff.mpr <| fun _ hJ ↦ hJ.2.1  · have existsCube : x ∈ ⋃ J ∈ 𝓙 (t u₁), (J : Set X) := by      suffices (𝓘 u₁ : Set X) ⊆ ⋃ J ∈ 𝓙 (t u₁), (J : Set X) from this hx      rw [biUnion_𝓙 (𝔖 := t u₁)]      apply subset_iUnion_of_subset (𝓘 u₁)      rfl    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₁) := 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₁ := 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          unfold ball          intro y xy          rw [mem_setOf_eq] at xy ⊢          have numbers : 4 * (D : ℝ) ^ s cube < 100 * D ^ (s cube + 1) := by            gcongr            · linarith            · exact one_lt_realD X            · linarith          exact gt_trans numbers xy      have black : ¬↑(𝓘 p) ⊆ ball (c cube) (100 * ↑D ^ (s cube + 1)) := by        refine east p belongs      contradiction