mathlib3

7bd19b32 - chore(data/finset, data/multiset): split into smaller files (#3256)

chore(data/finset, data/multiset): split into smaller files (#3256) This follows on from #2341, which split the second half of `data.list.basic` into separate files. This now does the same (trying to follow a similar split) for `data.multiset` and `data.finset`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>