no goals
ι : Type ?u.271647
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : CommMonoid β
⊢ ∏ _x in s, 1 = 1
simp only [Finset.prod, Multiset.map_const', Multiset.prod_replicate, one_pow]