no goals
α : Type u_2
β : Type u_1
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
f g : β → α
u₁ u₂ : α
s : Multiset β
⊢ fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) 0) = op (fold op u₁ (map f 0)) (fold op u₂ (map g 0))
simp
no goals
α : Type u_2
β : Type u_1
op : α → α → α
hc : IsCommutative α op
ha : IsAssociative α op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ fold op (op u₁ u₂) (map (fun x => op (f x) (g x)) (a ::ₘ b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
rw [map_cons, fold_cons_left, h, map_cons, fold_cons_left, map_cons,
  fold_cons_right, ha.assoc, ← ha.assoc (g a), hc.comm (g a),
  ha.assoc, hc.comm (g a), ha.assoc]