feat: Finset/Multiset.powersetCard 1 (#9137)

for [#9130](https://github.com/leanprover-community/mathlib4/pull/9130/files#r1429368677)



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/Data/Finset/Powerset.lean

@@ -218,14 +218,24 @@ theorem card_powersetCard (n : ℕ) (s : Finset α) :
 #align finset.card_powerset_len Finset.card_powersetCard
 
 @[simp]
-theorem powersetCard_zero (s : Finset α) : Finset.powersetCard 0 s = {∅} := by
+theorem powersetCard_zero (s : Finset α) : s.powersetCard 0 = {∅} := by
   ext; rw [mem_powersetCard, mem_singleton, card_eq_zero]
   refine'
     ⟨fun h => h.2, fun h => by
       rw [h]
       exact ⟨empty_subset s, rfl⟩⟩
 #align finset.powerset_len_zero Finset.powersetCard_zero
 
+@[simp]
+theorem map_val_val_powersetCard (s : Finset α) (i : ℕ) :
+    (s.powersetCard i).val.map Finset.val = s.1.powersetCard i := by
+  simp [Finset.powersetCard, map_pmap, pmap_eq_map, map_id']
+#align finset.map_val_val_powerset_len Finset.map_val_val_powersetCard
+
+theorem powersetCard_one (s : Finset α) :
+    s.powersetCard 1 = s.map ⟨_, Finset.singleton_injective⟩ :=
+  eq_of_veq <| Multiset.map_injective val_injective <| by simp [Multiset.powersetCard_one]
+
 @[simp]
 theorem powersetCard_empty (n : ℕ) {s : Finset α} (h : s.card < n) : powersetCard n s = ∅ :=
   Finset.card_eq_zero.mp (by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h])
@@ -324,12 +334,6 @@ theorem powersetCard_card_add (s : Finset α) {i : ℕ} (hi : 0 < i) :
   Finset.powersetCard_empty _ (lt_add_of_pos_right (Finset.card s) hi)
 #align finset.powerset_len_card_add Finset.powersetCard_card_add
 
-@[simp]
-theorem map_val_val_powersetCard (s : Finset α) (i : ℕ) :
-    (s.powersetCard i).val.map Finset.val = s.1.powersetCard i := by
-  simp [Finset.powersetCard, map_pmap, pmap_eq_map, map_id']
-#align finset.map_val_val_powerset_len Finset.map_val_val_powersetCard
-
 theorem powersetCard_map {β : Type*} (f : α ↪ β) (n : ℕ) (s : Finset α) :
     powersetCard n (s.map f) = (powersetCard n s).map (mapEmbedding f).toEmbedding :=
   ext <| fun t => by

Mathlib/Data/List/Sublists.lean

@@ -274,6 +274,10 @@ theorem sublistsLen_succ_cons {α : Type*} (n) (a : α) (l) :
       append_nil]; rfl
 #align list.sublists_len_succ_cons List.sublistsLen_succ_cons
 
+theorem sublistsLen_one {α : Type*} (l : List α) : sublistsLen 1 l = l.reverse.map ([·]) :=
+  l.rec (by rw [sublistsLen_succ_nil, reverse_nil, map_nil]) fun a s ih ↦ by
+    rw [sublistsLen_succ_cons, ih, reverse_cons, map_append, sublistsLen_zero]; rfl
+
 @[simp]
 theorem length_sublistsLen {α : Type*} :
     ∀ (n) (l : List α), length (sublistsLen n l) = Nat.choose (length l) n

Mathlib/Data/Multiset/Powerset.lean

@@ -258,6 +258,10 @@ theorem powersetCard_cons (n : ℕ) (a : α) (s) :
   Quotient.inductionOn s fun l => by simp [powersetCard_coe']
 #align multiset.powerset_len_cons Multiset.powersetCard_cons
 
+theorem powersetCard_one (s : Multiset α) : powersetCard 1 s = s.map singleton :=
+  Quotient.inductionOn s fun l ↦ by
+    simp [powersetCard_coe, sublistsLen_one, map_reverse, Function.comp]
+
 @[simp]
 theorem mem_powersetCard {n : ℕ} {s t : Multiset α} : s ∈ powersetCard n t ↔ s ≤ t ∧ card s = n :=
   Quotient.inductionOn t fun l => by simp [powersetCard_coe']