no goals
α : Type u_1
β : Type ?u.17525
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
b₁ b₂ : α
⊢ op (fold op b₁ (s₁ ∪ s₂)) (fold op b₂ (s₁ ∩ s₂)) = op (fold op b₁ s₁) (fold op b₂ s₂)
rw [← fold_add op, union_add_inter, fold_add op]