feat(data/{fin,multi}set/powerset): add some lemmas about powerset_len (#10866)

For both multisets and finsets

From flt-regular

Author: alexjbest

src/data/finset/powerset.lean

@@ -241,5 +241,14 @@ begin
       { rwa [card_erase_of_mem hx, nat.lt_pred_iff] } } }
 end
 
+@[simp]
+lemma powerset_len_card_add (s : finset α) {i : ℕ} (hi : 0 < i) :
+  s.powerset_len (s.card + i) = ∅ :=
+finset.powerset_len_empty _ (lt_add_of_pos_right (finset.card s) hi)
+
+@[simp] theorem map_val_val_powerset_len (s : finset α) (i : ℕ) :
+  (s.powerset_len i).val.map finset.val = s.1.powerset_len i :=
+by simp [finset.powerset_len, map_pmap, pmap_eq_map, map_id']
+
 end powerset_len
 end finset

src/data/multiset/powerset.lean

@@ -210,7 +210,7 @@ congr_arg coe powerset_len_aux_eq_map_coe
   powerset_len 0 s = {0} :=
 quotient.induction_on s $ λ l, by simp [powerset_len_coe']; refl
 
-@[simp] theorem powerset_len_zero_right (n : ℕ) :
+theorem powerset_len_zero_right (n : ℕ) :
   @powerset_len α (n + 1) 0 = 0 := rfl
 
 @[simp] theorem powerset_len_cons (n : ℕ) (a : α) (s) :
@@ -236,4 +236,21 @@ theorem powerset_len_mono (n : ℕ) {s t : multiset α} (h : s ≤ t) :
 le_induction_on h $ λ l₁ l₂ h, by simp [powerset_len_coe]; exact
   ((sublists_len_sublist_of_sublist _ h).map _).subperm
 
+@[simp] theorem powerset_len_empty {α : Type*} (n : ℕ) {s : multiset α} (h : s.card < n) :
+  powerset_len n s = 0 :=
+card_eq_zero.mp (nat.choose_eq_zero_of_lt h ▸ card_powerset_len _ _)
+
+@[simp]
+lemma powerset_len_card_add (s : multiset α) {i : ℕ} (hi : 0 < i) :
+  s.powerset_len (s.card + i) = 0 :=
+powerset_len_empty _ (lt_add_of_pos_right (card s) hi)
+
+theorem powerset_len_map {β : Type*} (f : α → β) (n : ℕ) (s : multiset α) :
+  powerset_len n (s.map f) = (powerset_len n s).map (map f) :=
+begin
+  induction s using multiset.induction with t s ih generalizing n,
+  { cases n; simp [powerset_len_zero_left, powerset_len_zero_right], },
+  { cases n; simp [ih], },
+end
+
 end multiset