eq_biUnion_iteratedMaximalSubfamily

lemma eq_biUnion_iteratedMaximalSubfamily (A : Set (𝔓 X)) {N : ℕ} (hN : ∀ x, stackSize A x ≤ N) :    A = ⋃ n < N, iteratedMaximalSubfamily A n := by  apply Subset.antisymm; swap  · simp [iUnion_subset_iff, iteratedMaximalSubfamily_subset]  -- we show that after `N` steps the maximal subfamilies cover everything. Otherwise, say some  -- `p` is left. Then `𝓘 p` is contained in an element of each of the previous subfamilies.  -- This gives `N+1` different elements containing any element of `𝓘 p`, a contradiction with  -- the maximal stack size.  intro p hp  contrapose! hN  simp only [mem_iUnion, exists_prop, not_exists, not_and] at hN  have E n (hn : n < N) : ∃ u ∈ iteratedMaximalSubfamily A n, (𝓘 p : Set X) ⊆ (𝓘 u : Set X) := by    rw [iteratedMaximalSubfamily]    apply (exists_maximal_disjoint_covering_subfamily _).choose_spec.2.2    simp only [coe_setOf, mem_setOf_eq, mem_sdiff, hp,      mem_iUnion, Subtype.exists, exists_prop, not_exists, not_and, true_and]    intro i hi    exact hN i (hi.trans hn)  choose! u hu h'u using E  obtain ⟨x, hxp⟩ : ∃ x, x ∈ (𝓘 p : Set X) := ⟨_, Grid.c_mem_Grid⟩  use x  have : stackSize {q ∈ A | q = p} x + stackSize {q ∈ A | q ≠ p} x = stackSize A x :=    stackSize_setOf_add_stackSize_setOf_not  have : 1 = stackSize {q ∈ A | q = p} x := by    have : 1 = ∑ q ∈ {p}, (𝓘 q : Set X).indicator 1 x := by simp [hxp]    rw [this]    congr    ext    simp (config := {contextual := true}) [hp]  classical  have : ∑ p with p ∈ u '' (Iio N), (𝓘 p : Set X).indicator 1 x      ≤ stackSize {q | q ∈ A ∧ q ≠ p} x := by    apply Finset.sum_le_sum_of_subset    rintro p hp    simp only [Finset.mem_filter_univ, mem_image, mem_Iio] at hp    rcases hp with ⟨n, hn, rfl⟩    simp only [ne_eq, mem_setOf_eq, Finset.mem_filter,      Finset.mem_univ, iteratedMaximalSubfamily_subset _ _ (hu n hn), true_and]    rintro rfl    exact hN n hn (hu n hn)  have : ∑ p with p ∈ u '' (Iio N), (𝓘 p : Set X).indicator 1 x      = ∑ p with p ∈ u '' (Iio N), 1 := by    apply Finset.sum_congr rfl (fun p hp ↦ ?_)    simp only [Finset.mem_filter_univ, mem_image, mem_Iio] at hp    rcases hp with ⟨n, hn, rfl⟩    have : x ∈ (𝓘 (u n) : Set X) := h'u n hn hxp    simp [this]  have : ∑ p with p ∈ u '' (Iio N), 1 = N := by    have : Finset.filter (fun p ↦ p ∈ u '' Iio N) Finset.univ = Finset.image u (Finset.Iio N) := by      ext p; simp    simp only [Finset.sum_const, smul_eq_mul, mul_one, this]    rw [Finset.card_image_of_injOn, Nat.card_Iio N]    intro a ha b hb hab    contrapose! hab    simp only [Finset.coe_Iio, mem_Iio] at ha hb    have := pairwiseDisjoint_iteratedMaximalSubfamily A (mem_univ a) (mem_univ b) hab    exact disjoint_iff_forall_ne.1 this (hu a ha) (hu b hb)  lia