case h.e'_2.h.e'_3
ι : Type u_2
α : Type u_4
β : Type u_1
γ : Type ?u.42625
inst✝² : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f✝ g✝ : ι → α
inst✝¹ : CommMonoid β
s : Multiset ι
F : Type u_3
inst✝ : MonoidHomClass F α β
f : F
g : ι → α
⊢ map (fun i => ↑f (g i)) s = map (↑f) (map g s)
ι : Type u_2
α : Type u_4
β : Type u_1
γ : Type ?u.42625
inst✝² : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f✝ g✝ : ι → α
inst✝¹ : CommMonoid β
s : Multiset ι
F : Type u_3
inst✝ : MonoidHomClass F α β
f : F
g : ι → α
⊢ prod (map (fun i => ↑f (g i)) s) = ↑f (prod (map g s))
convert (s.map g).prod_hom f
no goals
case h.e'_2.h.e'_3
ι : Type u_2
α : Type u_4
β : Type u_1
γ : Type ?u.42625
inst✝² : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f✝ g✝ : ι → α
inst✝¹ : CommMonoid β
s : Multiset ι
F : Type u_3
inst✝ : MonoidHomClass F α β
f : F
g : ι → α
⊢ map (fun i => ↑f (g i)) s = map (↑f) (map g s)
exact (map_map _ _ _).symm