no goals
α : Type u_2
β : Type ?u.340104
ι : Type ?u.340107
G : Type ?u.340110
M : Type u_1
N : Type ?u.340116
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
⊢ (∏ᶠ (i : α) (_ : i ∈ {a}), f i) = f a
rw [← Finset.coe_singleton, finprod_mem_coe_finset, Finset.prod_singleton]