john_nirenberg_aux1

lemma john_nirenberg_aux1 {L : Grid X} (mL : L ∈ Grid.maxCubes (MsetA l k n))    (mx : x ∈ setA (l + 1) k n) (mx₂ : x ∈ L) : 2 ^ (n + 1) ≤    stackSize { q ∈ 𝔐 (X := X) k n | 𝓘 q ≤ L} x := by  classical  -- LHS of equation (5.2.6) is strictly greater than `(l + 1) * 2 ^ (n + 1)`  rw [setA, mem_setOf, ← stackSize_setOf_add_stackSize_setOf_not (P := fun p' ↦ 𝓘 p' ≤ L)] at mx  -- Rewrite second sum of RHS of (5.2.6) so that it sums over tiles `q` satisfying `L < 𝓘 q`  nth_rw 2 [← stackSize_setOf_add_stackSize_setOf_not (P := fun p' ↦ Disjoint (𝓘 p' : Set X) L)]    at mx  simp_rw [mem_setOf_eq, and_assoc] at mx  have mid0 : stackSize { p' ∈ 𝔐 k n | ¬𝓘 p' ≤ L ∧ Disjoint (𝓘 p' : Set X) L} x = 0 := by    simp_rw [stackSize, Finset.sum_eq_zero_iff, indicator_apply_eq_zero, Finset.mem_filter_univ,      show ¬(1 : X → ℕ) x = 0 by simp, imp_false]    rintro y ⟨-, -, dj2⟩    exact disjoint_right.mp dj2 mx₂  rw [mid0, zero_add] at mx  have req :      { p' | p' ∈ 𝔐 k n ∧ ¬𝓘 p' ≤ L ∧ ¬Disjoint (𝓘 p' : Set X) L } =      { p' | p' ∈ 𝔐 k n ∧ L < 𝓘 p' } := by    ext q    simp_rw [mem_setOf_eq, and_congr_right_iff]    refine fun _ ↦ ⟨fun h ↦ ?_, ?_⟩    · apply lt_of_le_of_ne <| (le_or_ge_or_disjoint.resolve_left h.1).resolve_right h.2      by_contra k; subst k; exact absurd le_rfl h.1    · rw [Grid.lt_def, Grid.le_def, not_and_or, not_le]      exact fun h ↦ ⟨Or.inr h.2, not_disjoint_iff.mpr ⟨x, mem_of_mem_of_subset mx₂ h.1, mx₂⟩⟩  rw [req] at mx  -- The new second sum of RHS is at most `l * 2 ^ (n + 1)`  set Q₁ := { q ∈ 𝔐 (X := X) k n | 𝓘 q ≤ L }  set Q₂ := { q ∈ 𝔐 (X := X) k n | L < 𝓘 q }  have Ql : stackSize Q₂ x ≤ l * 2 ^ (n + 1) := by    by_cases h : IsMax L    · rw [Grid.isMax_iff] at h      have : Q₂ = ∅ := by        ext y; simp_rw [Q₂, mem_setOf_eq, Set.notMem_empty, iff_false, not_and, h, Grid.lt_def,          not_and_or, not_lt]        exact fun _ ↦ Or.inr (Grid.le_topCube).2      simp [stackSize, this]    have Lslq : ∀ q ∈ Q₂, L.succ ≤ 𝓘 q := fun q mq ↦ Grid.succ_le_of_lt mq.2    have Lout : ¬(L.succ : Set X) ⊆ setA (X := X) l k n := by      by_contra! hs      rw [Grid.maxCubes, Finset.mem_filter] at mL      apply absurd _ h      exact Grid.max_of_le_succ        (mL.2 L.succ (Finset.mem_filter.mpr ⟨Finset.mem_univ _, hs⟩) Grid.le_succ).symm.le    rw [not_subset_iff_exists_mem_notMem] at Lout    obtain ⟨x', mx', nx'⟩ := Lout    calc      _ = stackSize Q₂ x' := by        refine stackSize_congr fun q mq ↦ ?_        simp_rw [mem_of_mem_of_subset mx₂ (Grid.le_succ.trans (Lslq q mq)).1,          mem_of_mem_of_subset mx' (Lslq q mq).1]      _ ≤ stackSize (𝔐 (X := X) k n) x' := by        refine stackSize_mono <| sep_subset ..      _ ≤ l * 2 ^ (n + 1) := by rwa [setA, mem_setOf_eq, not_lt] at nx'  -- so the (unchanged) first sum of RHS is at least `2 ^ (n + 1)`  rw [add_one_mul] at mx; lia