no goals
ι : Type ?u.36621
α : Type u_1
β : Type ?u.36627
γ : Type ?u.36630
inst✝¹ : CommMonoid α
s t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
inst✝ : DecidableEq α
a : α
⊢ a ^ count a s = prod (filter (Eq a) s)
rw [filter_eq, prod_replicate]