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>
