no goals
α : Type u_1
β : Type u_3
γ : Type u_2
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s✝ : Finset α
a : α
inst✝ : DecidableEq α
g : γ → α
s : Finset γ
H : ∀ (x : γ), x ∈ s → ∀ (y : γ), y ∈ s → g x = g y → x = y
⊢ fold op b f (image g s) = fold op b (f ∘ g) s
simp only [fold, image_val_of_injOn H, Multiset.map_map]