iUnion_L0'

lemma iUnion_L0' : ⋃ (l < n), 𝔏₀' (X := X) k n l = 𝔏₀ k n := by  classical  refine iUnion_lt_minLayer_iff_bounded_series.mpr fun p ↦ ?_  suffices ¬∃ s : LTSeries (𝔏₀ (X := X) k n), s.length = n by    rcases lt_or_ge p.length n with c | c    · exact c    · exact absurd ⟨p.take ⟨n, by lia⟩, by rw [RelSeries.take_length]⟩ this  by_contra h; obtain ⟨s, hs⟩ := h; let sl := s.last; have dsl := sl.2.1.2.1  simp_rw [dens', lt_iSup_iff, mem_singleton_iff, exists_prop, exists_eq_left] at dsl  obtain ⟨l, hl, p', mp', sp', qp'⟩ := dsl  obtain ⟨b, mb, qb⟩ := exists_𝔒_with_le_quotient hl qp'  have 𝓘p'b : 𝓘 p' = 𝓘 b := by rw [𝔒, Finset.mem_filter] at mb; exact mb.2.1.symm  replace qb := ENNReal.mul_lt_of_lt_div qb  have mba : b ∈ (aux𝔐 k n).toFinset := by    simp_rw [mem_toFinset, aux𝔐, mem_setOf, qb, and_true]; rw [TilesAt, mem_preimage] at mp' ⊢    exact 𝓘p'b ▸ mp'  obtain ⟨m, lm, maxm⟩ := (aux𝔐 k n).toFinset.exists_le_maximal mba  replace maxm : m ∈ 𝔐 k n := by simpa only [mem_toFinset] using! maxm  -- We will now show a contradiction. As a member of `𝔏₀ k n` the _first_ element `s₀` of the  -- `LTSeries s` satisfies `𝔅 k n s₀ = ∅`. But we will show that `m ∈ 𝔅 k n s₀`,  -- i.e. `smul 100 s₀ ≤ smul 1 m`.  let s₀ := s.head; apply absurd s₀.2.2; rw [← ne_eq, ← nonempty_iff_ne_empty]; use m, maxm  constructor  · have l1 : 𝓘 s₀.1 ≤ 𝓘 sl.1 := s.head_le_last.1    have l2 : 𝓘 sl.1 ≤ 𝓘 b := 𝓘p'b ▸ sp'.1    exact (l1.trans l2).trans lm.1  change ball_(m) (𝒬 m) 1 ⊆ ball_(s₀.1) (𝒬 s₀.1) 100; intro (θ : Θ X) mθ; rw [mem_ball] at mθ  have aux : dist_(sl.1) (𝒬 sl.1) θ < 2 * l + 3 :=    calc      _ ≤ dist_(sl.1) (𝒬 sl.1) (𝒬 p') + dist_(sl.1) (𝒬 p') θ := dist_triangle ..      _ < l + dist_(sl.1) (𝒬 p') θ := by        apply add_lt_add_left        have : 𝒬 p' ∈ ball_(p') (𝒬 p') l := by convert! mem_ball_self (zero_lt_two.trans_le hl)        exact mem_ball'.mp (sp'.2 this)      _ ≤ l + dist_(p') (𝒬 p') θ := add_le_add_right (Grid.dist_mono sp'.1) _      _ ≤ l + dist_(p') (𝒬 p') (𝒬 b) + dist_(p') (𝒬 b) θ := by        rw [add_assoc]; apply add_le_add_right; exact dist_triangle ..      _ ≤ l + (l + 1) + dist_(b) (𝒬 b) θ := by        gcongr        · rw [𝔒, Finset.mem_filter] at mb          obtain ⟨(x : Θ X), x₁, x₂⟩ := not_disjoint_iff.mp mb.2.2          calc            _ ≤ dist_(p') x (𝒬 p') + dist_(p') x (𝒬 b) := dist_triangle_left ..            _ ≤ _ := by              apply add_le_add x₁.le              change dist_{𝓘 p'} x (𝒬 b) ≤ 1; rw [𝓘p'b]              exact (_root_.subset_cball x₂).le        · change dist_{𝓘 p'} (𝒬 b) θ ≤ dist_{𝓘 b} (𝒬 b) θ; rw [𝓘p'b]      _ ≤ l + (l + 1) + (dist_(b) (𝒬 m) (𝒬 b) + dist_(b) (𝒬 m) θ) :=        add_le_add_right (dist_triangle_left ..) _      _ ≤ l + (l + 1) + (1 + dist_(m) (𝒬 m) θ) := by        gcongr        · exact (dist_𝒬_lt_one_of_le lm).le        · exact Grid.dist_mono lm.1      _ < l + (l + 1) + (1 + 1) := by gcongr; exact mem_ball'.mp mθ      _ = _ := by ring  calc    _ ≤ dist_(s₀.1) (𝒬 sl.1) θ + dist_(s₀.1) (𝒬 sl.1) (𝒬 s₀.1) := dist_triangle_left ..    _ < 1 + dist_(s₀.1) (𝒬 sl.1) θ := by      rw [add_comm]; exact add_lt_add_left (dist_𝒬_lt_one_of_le s.head_le_last) _    _ ≤ 1 + C2_1_2 a ^ n * dist_(sl.1) (𝒬 sl.1) θ := add_le_add_right (dist_LTSeries hs) _    _ < 1 + C2_1_2 a ^ n * (2 * l + 3) := by gcongr; rw [C2_1_2]; positivity    _ ≤ 1 + (1 / 256) ^ n * (2 * 2 ^ n + 3) := by      gcongr      · rw [C2_1_2]; positivity      · exact C2_1_2_le_inv_256 X      · exact_mod_cast (l_upper_bound hl qp').le    _ = 1 + 2 * (2 / 256) ^ n + (1 / 256) ^ n * 3 := by      simp [div_pow]; ring    _ ≤ 1 + 2 * (2 / 256) ^ 0 + (1 / 256) ^ 0 * 3 := by      gcongr 1 + 2 * ?_ + ?_ * 3 <;>        exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (by lia)    _ < _ := by norm_num