feat(Data/Finset/Powerset): add biUnion_id_subset_iff_subset_powerset (#39535)

Author: b-mehta

Mathlib/Data/Finset/Powerset.lean

@@ -78,6 +78,11 @@ theorem image_injOn_powerset_of_injOn {β : Type*} [DecidableEq β] {f : α →
   have {z a} (_ : z ⊆ s) (_ : a ∈ s) : a ∈ z ↔ f a ∈ z.image f := by grind [H.eq_iff]
   exact fun _ _ _ _ _ => by grind
 
+/-- `s.biUnion id ⊆ t` iff every member of `s` is a subset of `t`, i.e. `s ⊆ t.powerset`. -/
+lemma biUnion_id_subset_iff_subset_powerset [DecidableEq α] {s : Finset (Finset α)} :
+    s.biUnion id ⊆ t ↔ s ⊆ t.powerset := by
+  aesop (add simp subset_iff)
+
 theorem image_surjOn_powerset {β : Type*} [DecidableEq β] {f : α → β} :
     Set.SurjOn (α := Finset α) (·.image f) s.powerset (s.image f).powerset :=
   fun t ht => ⟨{ x ∈ s | f x ∈ t}, by grind⟩