no goals
α : Type u_2
β : Type u_3
γ : Type u_1
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
g : γ ↪ α
s : Finset γ
⊢ fold op b f (map g s) = fold op b (f ∘ ↑g) s
simp only [fold, map, Multiset.map_map]