no goals
ι : Type u_2
α : Type u_1
β : Type ?u.57133
γ : Type ?u.57136
inst✝ : CommMonoid α
s t : Multiset α
a : α
m : Multiset ι
f g : ι → α
⊢ prod (map (fun x => 1) m) = 1
rw [map_const', prod_replicate, one_pow]