ι : Type ?u.6108
α : Type u_1
β : Type ?u.6114
γ : Type ?u.6117
inst✝ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
s : Multiset α
⊢ List.prod (toList s) = prod ↑(toList s)
ι : Type ?u.6108
α : Type u_1
β : Type ?u.6114
γ : Type ?u.6117
inst✝ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
s : Multiset α
⊢ List.prod (toList s) = prod s
conv_rhs => rw [← coe_toList s]
no goals
ι : Type ?u.6108
α : Type u_1
β : Type ?u.6114
γ : Type ?u.6117
inst✝ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f g : ι → α
s : Multiset α
⊢ List.prod (toList s) = prod ↑(toList s)
rw [coe_prod]