ι : Type ?u.552476
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
s : Multiset α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
l : List α
⊢ Multiset.prod (Multiset.map f (Quot.mk Setoid.r l)) =
    ∏ m in Multiset.toFinset (Quot.mk Setoid.r l), f m ^ Multiset.count m (Quot.mk Setoid.r l)
ι : Type ?u.552476
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
s : Multiset α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
⊢ Multiset.prod (Multiset.map f s) = ∏ m in Multiset.toFinset s, f m ^ Multiset.count m s
refine' Quot.induction_on s fun l => _
no goals
ι : Type ?u.552476
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
s : Multiset α
M : Type u_1
inst✝ : CommMonoid M
f : α → M
l : List α
⊢ Multiset.prod (Multiset.map f (Quot.mk Setoid.r l)) =
    ∏ m in Multiset.toFinset (Quot.mk Setoid.r l), f m ^ Multiset.count m (Quot.mk Setoid.r l)
simp [prod_list_map_count l f]