dyadic_union

lemma dyadic_union (hx : x ∈ setA l k n) : ∃ i : Grid X, x ∈ i ∧ (i : Set X) ⊆ setA l k n := by  let M : Finset (𝔓 X) := { p | p ∈ 𝔐 k n ∧ x ∈ 𝓘 p }  simp_rw [setA, mem_setOf, stackSize, indicator_apply, Pi.one_apply, Finset.sum_boole, Nat.cast_id,    Finset.filter_filter] at hx ⊢  obtain ⟨b, memb, minb⟩ := M.exists_min_image 𝔰 (Finset.card_pos.mp (zero_le.trans_lt hx))  simp_rw [M, Finset.mem_filter_univ] at memb minb  use 𝓘 b, memb.2; intro c mc; rw [mem_setOf]  refine hx.trans_le (Finset.card_le_card fun y hy ↦ ?_)  rw [Finset.mem_filter_univ] at hy ⊢  exact ⟨hy.1, mem_of_mem_of_subset mc (le_of_mem_of_mem (minb y hy) memb.2 hy.2).1⟩