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