stackSize_𝔘₄_le

lemma stackSize_𝔘₄_le (x : X) : stackSize (𝔘₄ (X := X) k n j l) x ≤ 2 ^ n := by classical calc  stackSize (𝔘₄ (X := X) k n j l) x  _ = ∑ i ∈ Finset.Ico (l * 2 ^ n) ((l + 1) * 2 ^ n),        stackSize (iteratedMaximalSubfamily (𝔘₃ k n j) i) x := by    simp only [stackSize, 𝔘₄]    rw [← Finset.sum_biUnion]; swap    · intro a ha b hb hab      apply Finset.disjoint_coe.1      apply disjoint_iff_forall_ne.2 (fun p hp q hq ↦ ?_)      simp only [Finset.coe_filter, Finset.mem_univ, true_and, setOf_mem_eq] at hp hq      have := pairwiseDisjoint_iteratedMaximalSubfamily (𝔘₃ (X := X) k n j)        (mem_univ a) (mem_univ b) hab      exact disjoint_iff_forall_ne.1 this hp hq    congr    ext p    simp_rw [Finset.mem_biUnion, Finset.mem_filter_univ, mem_Ico, Finset.mem_Ico, mem_iUnion,      exists_prop]  _ ≤ ∑ i ∈ Finset.Ico (l * 2 ^ n) ((l + 1) * 2 ^ n), 1 := by    gcongr with i hi    apply stackSize_le_one_of_pairwiseDisjoint    apply pairwiseDisjoint_iteratedMaximalSubfamily_image  _ = 2 ^ n := by simp [add_mul]