feat(data/finset): sup_eq_bind (#5717)
`finset.sup s f` is equal to `finset.bind s f` when `f : α → finset β` is an indexed family of finite sets. This is a proof of that with a couple supporting lemmas. (There might be a more direct proof through the definitions of `sup` and `bind`, which are eventually in terms of `multiset.foldr`.)
I also moved `finset.mem_sup` to `multiset.mem_sup` and gave a new `finset.mem_sup` for indexed families of `finset`, where the old one was for indexed families of `multiset`.
