Commit 2021-03-09 21:43 be6753ca

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.