no goals
ι : Type ?u.12245
α : Type u_1
β : Type ?u.12251
γ : Type ?u.12254
inst✝ : CommMonoid α
s t : Multiset α
a✝ : α
m : Multiset ι
f g : ι → α
a b : α
⊢ prod {a, b} = a * b
rw [insert_eq_cons, prod_cons, prod_singleton]