feat(data/finset): missing fold_map lemma (#794)

Author: kim-em

src/data/finset.lean

@@ -1247,6 +1247,10 @@ by unfold fold; rw [insert_val, ndinsert_of_not_mem h, map_cons, fold_cons_left]
 
 @[simp] theorem fold_singleton : (singleton a).fold op b f = f a * b := rfl
 
+@[simp] theorem fold_map [decidable_eq α] {g : γ ↪ α} {s : finset γ} :
+  (s.map g).fold op b f = s.fold op b (f ∘ g) :=
+by simp only [fold, map, multiset.map_map]
+
 @[simp] theorem fold_image [decidable_eq α] {g : γ → α} {s : finset γ}
   (H : ∀ (x ∈ s) (y ∈ s), g x = g y → x = y) : (s.image g).fold op b f = s.fold op b (f ∘ g) :=
 by simp only [fold, image_val_of_inj_on H, multiset.map_map]