ι : Type ?u.92899
β : Type u
α : Type v
γ : Type w
inst✝² : CommMonoid β
inst✝¹ : CommMonoid γ
G : Type u_1
inst✝ : MonoidHomClass G β γ
g : G
f : α → β
s : Finset α
⊢ Multiset.prod (Multiset.map ((fun x => ↑g x) ∘ fun x => f x) s.val) =
    Multiset.prod (Multiset.map (fun x => ↑g (f x)) s.val)
ι : Type ?u.92899
β : Type u
α : Type v
γ : Type w
inst✝² : CommMonoid β
inst✝¹ : CommMonoid γ
G : Type u_1
inst✝ : MonoidHomClass G β γ
g : G
f : α → β
s : Finset α
⊢ ↑g (∏ x in s, f x) = ∏ x in s, ↑g (f x)
simp only [Finset.prod_eq_multiset_prod, map_multiset_prod, Multiset.map_map]
no goals
ι : Type ?u.92899
β : Type u
α : Type v
γ : Type w
inst✝² : CommMonoid β
inst✝¹ : CommMonoid γ
G : Type u_1
inst✝ : MonoidHomClass G β γ
g : G
f : α → β
s : Finset α
⊢ Multiset.prod (Multiset.map ((fun x => ↑g x) ∘ fun x => f x) s.val) =
    Multiset.prod (Multiset.map (fun x => ↑g (f x)) s.val)
rfl