mathlib3

bc1f1459 - feat(data/multiset): `<` on multisets is well-founded (#8319)

feat(data/multiset): `<` on multisets is well-founded (#8319) This is vaguely related to #5783, in that it tries to solve a similar goal of finding a minimal multiset with some property.