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

Author: YaelDillies

src/data/finset/basic.lean

@@ -2204,10 +2204,14 @@ lemma map_injective (f : α ↪ β) : injective (map f) := (map_embedding f).inj
 
 @[simp] theorem map_embedding_apply : map_embedding f s = map f s := rfl
 
-theorem map_filter {p : β → Prop} [decidable_pred p] :
+lemma filter_map {p : β → Prop} [decidable_pred p] :
   (s.map f).filter p = (s.filter (p ∘ f)).map f :=
 eq_of_veq (map_filter _ _ _)
 
+lemma map_filter {f : α ≃ β} {p : α → Prop} [decidable_pred p] :
+  (s.filter p).map f.to_embedding = (s.map f.to_embedding).filter (p ∘ f.symm) :=
+by simp only [filter_map, function.comp, equiv.to_embedding_apply, equiv.symm_apply_apply]
+
 @[simp] lemma disjoint_map {s t : finset α} (f : α ↪ β) :
   disjoint (s.map f) (t.map f) ↔ disjoint s t :=
 begin

src/data/finset/nat_antidiagonal.lean

@@ -114,7 +114,7 @@ begin
   have : (λ (x : ℕ × ℕ), x.snd = m) ∘ prod.swap = (λ (x : ℕ × ℕ), x.fst = m),
   { ext, simp },
   rw ←map_swap_antidiagonal,
-  simp [map_filter, this, filter_fst_eq_antidiagonal, apply_ite (finset.map _)]
+  simp [filter_map, this, filter_fst_eq_antidiagonal, apply_ite (finset.map _)]
 end
 
 section equiv_prod

src/data/fintype/fin.lean

@@ -50,7 +50,7 @@ end
 lemma card_filter_univ_succ' (p : fin (n + 1) → Prop) [decidable_pred p] :
   (univ.filter p).card = (ite (p 0) 1 0) + (univ.filter (p ∘ fin.succ)).card :=
 begin
-  rw [fin.univ_succ, filter_cons, card_disj_union, map_filter, card_map],
+  rw [fin.univ_succ, filter_cons, card_disj_union, filter_map, card_map],
   split_ifs; simp,
 end
 

src/data/nat/count.lean

@@ -63,7 +63,7 @@ begin
     rintro x hx ⟨c, _, rfl⟩,
     exact (self_le_add_right _ _).not_lt hx },
   simp_rw [count_eq_card_filter_range, range_add, filter_union, card_disjoint_union this,
-    map_filter, add_left_embedding, card_map], refl,
+    filter_map, add_left_embedding, card_map], refl,
 end
 
 lemma count_add' (a b : ℕ) : count p (a + b) = count (λ k, p (k + b)) a + count p b :=