no goals
ι : Type ?u.11541
α : Type u_1
β : Type ?u.11547
γ : Type ?u.11550
inst✝ : CommMonoid α
s t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
a : α
⊢ prod {a} = a
simp only [mul_one, prod_cons, ← cons_zero, eq_self_iff_true, prod_zero]