no goals
α : Type u_2
β : Type u_1
γ : Type ?u.9400
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f✝ : α → β
b : β
s : Finset α
a : α
f g : α → β
b₁ b₂ : β
⊢ fold op (op b₁ b₂) (fun x => op (f x) (g x)) s = op (fold op b₁ f s) (fold op b₂ g s)
simp only [fold, fold_distrib]