setA_subset_iUnion_𝓒

lemma setA_subset_iUnion_𝓒 {l k n : ℕ} :    setA (X := X) l k n ⊆ ⋃ i ∈ 𝓒 (X := X) k, i := by  classical  intro x mx  simp_rw [setA, mem_setOf, stackSize, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id,    Finset.filter_filter] at mx  replace mx := zero_le.trans_lt mx  rw [Finset.card_pos] at mx  obtain ⟨p, hp⟩ := mx  simp_rw [Finset.mem_filter_univ, 𝔐, mem_setOf, maximal_iff, aux𝔐, mem_setOf, TilesAt,    mem_preimage] at hp  rw [mem_iUnion₂]; use 𝓘 p, hp.1.1.1, hp.2