no goals
ι : Type ?u.876223
β✝ : Type u
α✝ : Type v
γ : Type w
s✝ s₁ s₂ : Finset α✝
a : α✝
f✝ g : α✝ → β✝
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid β
inst✝ : Unique α
s : Finset α
f : α → β
h : Finset.Nonempty s
⊢ ∏ x in s, f x = f default
rw [h.eq_singleton_default, Finset.prod_singleton]