iUnion_𝔘₄

lemma iUnion_𝔘₄ (hkn : k ≤ n) : ⋃ l ∈ Iio (4 * n + 12), 𝔘₄ (X := X) k n j l = 𝔘₃ k n j := by  have : ⋃ l ∈ Iio (4 * n + 12), 𝔘₄ (X := X) k n j l =      ⋃ i < (4 * n + 12) * 2 ^ n, iteratedMaximalSubfamily (𝔘₃ k n j) i := by    apply Subset.antisymm    · simp only [mem_Iio, 𝔘₄, mem_Ico, biUnion_and', iUnion_subset_iff]      intro l i hi hl h'i      apply subset_biUnion_of_mem      change i + 1 ≤ (4 * n + 12) * 2 ^ n      suffices i < (4 * n + 12) * 2 ^ n by lia      exact h'i.trans_le (mul_le_mul' (by lia) le_rfl)    · simp only [𝔘₄, iUnion_subset_iff]      intro i hi      let l := i / 2 ^ n      have : iteratedMaximalSubfamily (𝔘₃ k n j) i ⊆ ⋃ i ∈ Ico (l * 2 ^ n) ((l + 1) * 2 ^ n),          iteratedMaximalSubfamily (X := X) (𝔘₃ k n j) i := by        apply subset_biUnion_of_mem        refine ⟨Nat.div_mul_le_self _ _, ?_⟩        rw [← Nat.div_lt_iff_lt_mul (Nat.two_pow_pos n)]        exact lt_add_one _      apply this.trans      apply subset_biUnion_of_mem (u := fun l ↦        ⋃ i ∈ Ico (l * 2 ^ n) ((l + 1) * 2 ^ n), iteratedMaximalSubfamily (𝔘₃ k n j) i)      simp only [mem_Iio, l]      rwa [Nat.div_lt_iff_lt_mul (Nat.two_pow_pos n)]  rw [this, eq_comm]  apply eq_biUnion_iteratedMaximalSubfamily  intro x  apply forest_stacking x hkn