mathlib3

7f837db4 - feat(data/set/finite): add `multiset.finite_to_set` (#15177)

feat(data/set/finite): add `multiset.finite_to_set` (#15177) * move `finset.finite_to_set` up; * add `multiset.finite_to_set`, `multiset.finite_to_set_to_finset`, and `list.finite_to_set`; * use new lemmas here and there.