TileStructure.Forest.biUnion_𝓛

@[simp]lemma biUnion_𝓛 : ⋃ J ∈ 𝓛 𝔖, J = ⋃ I : Grid X, (I : Set X) := by  classical  refine subset_antisymm (iUnion₂_subset_iUnion ..) fun x mx ↦ ?_  simp_rw [mem_iUnion] at mx ⊢; obtain ⟨I, mI⟩ := mx  obtain ⟨J, sJ, mJ⟩ :=    Grid.exists_containing_subcube _ ⟨le_rfl, scale_mem_Icc.1⟩ mI  have : J ∈ (𝓛₀ 𝔖).toFinset := by rw [mem_toFinset]; left; exact sJ  obtain ⟨M, lM, maxM⟩ := (𝓛₀ 𝔖).toFinset.exists_le_maximal this  simp_rw [mem_toFinset] at maxM  use M, maxM, (Grid.le_def.mp lM).1 mJ