feat(data/{finset,finsupp,multiset}): more assorted lemmas (#4006)
Another grab bag of facts from the Witt vector branch.
Coauthored by: Johan Commelin <johan@commelin.net>
<!-- put comments you want to keep out of the PR commit here -->
Co-authored-by: Johan Commelin <johan@commelin.net>