feat(data/multiset): `(s.erase x).map f = (s.map f).erase (f x)` (#8375)
feat(data/multiset): `(s.erase x).map f = (s.map f).erase (f x)` (#8375)

A little lemma that I needed for Dedekind domains.



Co-authored-by: Anne Baanen <839f20e486a83a313cf46ca4094e2de98129fc5d@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib