α : Type u_2
β : Type u_3
γ : Type u_1
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
op' : γ → γ → γ
inst✝¹ : IsCommutative γ op'
inst✝ : IsAssociative γ op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x => m (f x)) s.val) = Multiset.fold op' (m b) (Multiset.map (m ∘ f) s.val)
α : Type u_2
β : Type u_3
γ : Type u_1
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
op' : γ → γ → γ
inst✝¹ : IsCommutative γ op'
inst✝ : IsAssociative γ op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ fold op' (m b) (fun x => m (f x)) s = m (fold op b f s)
rw [fold, fold, ← Multiset.fold_hom op hm, Multiset.map_map]
no goals
α : Type u_2
β : Type u_3
γ : Type u_1
op : β → β → β
hc : IsCommutative β op
ha : IsAssociative β op
f : α → β
b : β
s : Finset α
a : α
op' : γ → γ → γ
inst✝¹ : IsCommutative γ op'
inst✝ : IsAssociative γ op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x => m (f x)) s.val) = Multiset.fold op' (m b) (Multiset.map (m ∘ f) s.val)
simp only [Function.comp_apply]