feat(Data/Finset/Powerset): add results about powersetCard (#39541)

These are useful for set family combinatorics

Author: b-mehta

Mathlib/Data/Finset/Powerset.lean

@@ -332,6 +332,26 @@ theorem powersetCard_sup [DecidableEq α] (u : Finset α) (n : ℕ) (hn : n < u.
     rw [← insert_erase hx, powersetCard_succ_insert (notMem_erase _ _)]
     exact mem_union_right _ (mem_image_of_mem _ ht)
 
+/-- The union of all `r`-element subsets of `s` is `s`, provided `1 ≤ r ≤ #s`. -/
+lemma powersetCard_biUnion [DecidableEq α] {r : ℕ} (hr : r ≠ 0) (hrs : r ≤ #s) :
+    (s.powersetCard r).biUnion id = s := by
+  obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hr
+  rw [← sup_eq_biUnion]
+  exact powersetCard_sup _ _ hrs
+
+/-- If two finsets of equal cardinality have the same `r`-element subsets for some `1 ≤ r ≤ #a`,
+they are equal. -/
+lemma eq_of_powersetCard_eq {a b : Finset α} {r : ℕ}
+    (hab : #a = #b) (hr₀ : r ≠ 0) (hra : r ≤ #a)
+    (h : a.powersetCard r = b.powersetCard r) : a = b := by
+  classical
+  simpa [powersetCard_biUnion hr₀, ← hab, hra] using congr(($h).biUnion id)
+
+/-- For `1 ≤ r ≤ q`, the map `powersetCard r` is injective on the finsets of cardinality `q`. -/
+lemma powersetCard_injOn {q r : ℕ} (hr₀ : r ≠ 0) (hrq : r ≤ q) :
+    Set.InjOn (fun a ↦ a.powersetCard r) {a : Finset α | #a = q}
+  | _, rfl, _, hbq, h => eq_of_powersetCard_eq hbq.symm hr₀ hrq h
+
 theorem powersetCard_map {β : Type*} (f : α ↪ β) (n : ℕ) (s : Finset α) :
     powersetCard n (s.map f) = (powersetCard n s).map (mapEmbedding f).toEmbedding :=
   ext fun t => by