no goals
ι : Type ?u.263261
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : IsEmpty α
s : Finset α
⊢ ∏ i in s, f i = 1
rw [eq_empty_of_isEmpty s, prod_empty]