Prove bind_powerset_len using #15834

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
 -/
@@ -258,4 +259,21 @@ lemma disjoint_powerset_len (s : multiset α) {i j : ℕ} (h : i ≠ j) :
 by exact λ 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.perm.map _ (list.range_bind_sublists_len S)),
+end
+
+-- lemma sup_powerset_len {α : Type*} [decidable_eq α] (S : multiset α) :
+--  finset.sup (finset.range (S.card + 1)) (λ k, S.powerset_len k) = S.powerset :=
+-- begin
+--  convert (sum_powerset_len S),
+--  apply eq.symm,
+--  exact (finset_sum_eq_sup_iff_disjoint.mpr (λ _ _ _ _ h, disjoint_powerset_len S h)),
+-- end
+
 end multiset

src/data/nat/choose/sum.lean

@@ -178,32 +178,3 @@ begin
 end
 
 end finset
-
-namespace multiset
-
-lemma sum_powerset_len {α : Type*} (S : multiset α) :
-  ∑ k in finset.range (S.card + 1), (S.powerset_len k) = S.powerset :=
-begin
-  classical,
-  apply eq_of_le_of_card_le,
-  suffices : finset.sup (finset.range (S.card + 1)) (λ k, S.powerset_len k) ≤ S.powerset,
-  { apply eq.trans_le _ this,
-    exact finset_sum_eq_sup_iff_disjoint.mpr (λ _ _ _ _ hxny _ htx hty,
-      hxny $ eq.trans (mem_powerset_len.mp htx).right.symm
-      (mem_powerset_len.mp hty).right), },
-  { rw finset.sup_le_iff,
-    exact λ b _, powerset_len_le_powerset b S, },
-  { rw [card_powerset, map_sum card],
-    simp_rw card_powerset_len,
-    exact eq.le (nat.sum_range_choose S.card).symm, },
-end
-
-lemma sup_powerset_len {α : Type*} [decidable_eq α] (S : multiset α) :
-  finset.sup (finset.range (S.card + 1)) (λ k, S.powerset_len k) = S.powerset :=
-begin
-  convert (sum_powerset_len S),
-  apply eq.symm,
-  exact (finset_sum_eq_sup_iff_disjoint.mpr (λ _ _ _ _ h, disjoint_powerset_len S h)),
-end
-
-end multiset