no goals
ι : Type ?u.8691
α : Type u_1
β : Type ?u.8697
γ : Type ?u.8700
inst✝¹ : CommMonoid α
s t : Multiset α
a : α
m : Multiset ι
f g : ι → α
inst✝ : DecidableEq α
h : a ∈ s
⊢ a * prod (erase s a) = prod s
rw [← s.coe_toList, coe_erase, coe_prod, coe_prod, List.prod_erase (mem_toList.2 h)]