[Merged by Bors] - feat (data/multiset/powerset): add bind_powerset_len

src/data/multiset/antidiagonal.lean

@@ -67,6 +67,19 @@ 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;

src/data/multiset/basic.lean

@@ -1159,6 +1159,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/nat/choose/sum.lean

@@ -178,3 +178,35 @@ 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,
+  apply finset_sum_eq_sup_iff_disjoint.mpr,
+  exact λ _ _ _ _ hxy _ hx hy,
+    hxy (eq.trans (multiset.mem_powerset_len.mp hx).right.symm
+    (multiset.mem_powerset_len.mp hy).right),
+end
+
+end multiset