Commit 2022-11-20 15:51 6c17afb9
View on Github →feat(data/finset/basic): Map finset.filter under an equiv (#17513)
Rename finset.map_filter to finset.filter_map. This unfortunately means it doesn't match the multiset and list lemmas. Prove the true finset.map_filter.