no goals
α : Type u_1
β : Type u_2
γ : Type ?u.8657
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
g : α → β
H : ∀ (x : α), x ∈ s → f x = g x
⊢ fold op b f s = fold op b g s
rw [fold, fold, map_congr rfl H]