feat (data/multiset/powerset): add bind_powerset_len (#15824)

We prove the following result
```lean
lemma multiset.bind_powerset_len {α : Type*} (S : multiset α) :
  bind (multiset.range (S.card + 1)) (λ k, S.powerset_len k) = S.powerset
```

From flt-regular



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/big_operators/basic.lean

@@ -1703,6 +1703,14 @@ begin
     exact add_eq_union_left_of_le (finset.sup_le (λ x hx, le_sum_of_mem (mem_map_of_mem f hx))), },
 end
 
+lemma sup_powerset_len {α : Type*} [decidable_eq α] (x : multiset α) :
+  finset.sup (finset.range (x.card + 1)) (λ k, x.powerset_len k) = x.powerset :=
+begin
+  convert bind_powerset_len x,
+  rw [multiset.bind, multiset.join, ←finset.range_coe, ←finset.sum_eq_multiset_sum],
+  exact eq.symm (finset_sum_eq_sup_iff_disjoint.mpr (λ _ _ _ _ h, disjoint_powerset_len x h)),
+end
+
 @[simp] lemma to_finset_sum_count_eq (s : multiset α) :
   (∑ a in s.to_finset, s.count a) = s.card :=
 multiset.induction_on s rfl

src/data/multiset/antidiagonal.lean

@@ -67,10 +67,23 @@ quotient.induction_on s $ λ l, begin
   {congr; simp}, {simp}
 end
 
+theorem antidiagonal_eq_map_powerset [decidable_eq α] (s : multiset α) :
+  s.antidiagonal = s.powerset.map (λ t, (s - t, t)) :=
+begin
+  induction s using multiset.induction_on with a s hs,
+  { simp only [antidiagonal_zero, powerset_zero, zero_tsub, map_singleton] },
+  { simp_rw [antidiagonal_cons, powerset_cons, map_add, hs, map_map, function.comp, prod.map_mk,
+      id.def, sub_cons, erase_cons_head],
+    rw add_comm,
+    congr' 1,
+    refine multiset.map_congr rfl (λ x hx, _),
+    rw cons_sub_of_le _ (mem_powerset.mp hx) }
+end
+
 @[simp] theorem card_antidiagonal (s : multiset α) :
   card (antidiagonal s) = 2 ^ card s :=
 by have := card_powerset s;
-   rwa [← antidiagonal_map_fst, card_map] at this
+  rwa [← antidiagonal_map_fst, card_map] at this
 
 lemma prod_map_add [comm_semiring β] {s : multiset α} {f g : α → β} :
   prod (s.map (λa, f a + g a)) =

src/data/multiset/basic.lean

@@ -1161,6 +1161,10 @@ multiset.induction_on t (by simp [multiset.sub_zero])
 instance : has_ordered_sub (multiset α) :=
 ⟨λ n m k, multiset.sub_le_iff_le_add⟩
 
+lemma cons_sub_of_le (a : α) {s t : multiset α} (h : t ≤ s) :
+  a ::ₘ s - t = a ::ₘ (s - t) :=
+by rw [←singleton_add, ←singleton_add, add_tsub_assoc_of_le h]
+
 theorem sub_eq_fold_erase (s t : multiset α) : s - t = foldl erase erase_comm s t :=
 quotient.induction_on₂ s t $ λ l₁ l₂,
 show ↑(l₁.diff l₂) = foldl erase erase_comm ↑l₁ ↑l₂,

src/data/multiset/powerset.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import data.multiset.basic
-
+import data.multiset.range
+import data.multiset.bind
 /-!
 # The powerset of a multiset
 -/
@@ -253,4 +254,18 @@ begin
   { cases n; simp [ih, map_comp_cons], },
 end
 
+lemma disjoint_powerset_len (s : multiset α) {i j : ℕ} (h : i ≠ j) :
+  multiset.disjoint (s.powerset_len i) (s.powerset_len j) :=
+λ x hi hj, h (eq.trans (multiset.mem_powerset_len.mp hi).right.symm
+  (multiset.mem_powerset_len.mp hj).right)
+
+lemma bind_powerset_len {α : Type*} (S : multiset α) :
+  bind (multiset.range (S.card + 1)) (λ k, S.powerset_len k) = S.powerset :=
+begin
+  induction S using quotient.induction_on,
+  simp_rw [quot_mk_to_coe, powerset_coe', powerset_len_coe, ←coe_range, coe_bind, ←list.bind_map,
+    coe_card],
+  exact coe_eq_coe.mpr ((list.range_bind_sublists_len_perm S).map _),
+end
+
 end multiset