α : Type u_1
β : Type u_2
γ : Type ?u.4116
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
α : Type u_1
β : Type u_2
γ : Type ?u.4116
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ fold op b f (insert a s) = op (f a) (fold op b f s)
unfold fold
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.4116
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ Multiset.fold op b (Multiset.map f (insert a s).val) = op (f a) (Multiset.fold op b (Multiset.map f s.val))
rw [insert_val, ndinsert_of_not_mem h, Multiset.map_cons, fold_cons_left]