mathlib

6c17afb9 - feat(data/finset/basic): Map `finset.filter` under an `equiv` (#17513)

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`.