forest_stacking

lemma forest_stacking (x : X) (hkn : k ≤ n) : stackSize (𝔘₃ (X := X) k n j) x ≤ C5_4_8 n := by  classical  by_contra! h  let C : Finset (𝔓 X) := { u | u ∈ 𝔘₃ (X := X) k n j ∧ x ∈ 𝓘 u }  have Cc : C.card = stackSize (𝔘₃ k n j) x := by    simp_rw [stackSize, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id,      C, Grid.mem_def, Finset.filter_filter]  have Cn : C.Nonempty := by    by_contra! Ce    simp_rw [← Cc, Ce, Finset.card_empty, not_lt_zero] at h  let C' : Finset (Grid X) := C.image 𝓘  have C'n : C'.Nonempty := by rwa [Finset.image_nonempty]  obtain ⟨i, mi, li⟩ := C'.exists_minimal C'n  simp_rw [C', Finset.mem_image, C, Finset.mem_filter_univ] at mi  obtain ⟨u, ⟨mu, mx⟩, uei⟩ := mi; subst uei  have uA : (𝓘 u : Set X) ⊆ setA (2 * n + 6) k n := fun y my ↦    calc      _ = (4 * n + 12) * 2 ^ n := by ring      _ < stackSize (𝔘₃ k n j) x := h      _ ≤ stackSize (𝔘₃ k n j) y := by        simp_rw [stackSize, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id]        apply Finset.card_le_card fun v mv ↦ ?_        simp_rw [Finset.filter_filter, Finset.mem_filter_univ] at mv ⊢        have mvC' : 𝓘 v ∈ C' := by          simp_rw [C', Finset.mem_image]; use v          simp_rw [C, Finset.mem_filter_univ, and_true]; exact mv        specialize li mvC'        have inc := (or_assoc.mpr (le_or_ge_or_disjoint (i := 𝓘 u) (j := 𝓘 v))).resolve_right          (not_disjoint_iff.mpr ⟨_, mx, mv.2⟩)        replace inc : 𝓘 u ≤ 𝓘 v := by tauto        exact ⟨mv.1, inc.1 my⟩      _ ≤ _ := stackSize_𝔘₃_le_𝔐 _  refine absurd (disjoint_left.mpr fun v mv ↦ ?_) (𝔘₃_subset_𝔘₂ mu).2  rw [𝔗₁, mem_setOf] at mv; rw [ℭ₆, mem_setOf, not_and, not_not]  refine fun _ ↦ (mv.2.2.1).1.trans ?_  calc    _ ⊆ setA (2 * n + 6) k n := uA    _ ⊆ G₂ := subset_iUnion₂_of_subset n k (subset_iUnion_of_subset hkn subset_rfl)    _ ⊆ _ := subset_union_of_subset_left subset_union_right G₃