feat(data/{list,multiset,finset}): map_filter (#6600)
This renames `list.filter_of_map` to `list.map_filter`, which unifies the name of the `map_filter` lemmas for lists and finsets, and adds a corresponding lemma for multisets.
Unfortunately, the name `list.filter_map` is already used for a definition.
