no goals
α : Type u_2
β : Type ?u.340750
ι : Type ?u.340753
G : Type ?u.340756
M : Type u_1
N : Type ?u.340762
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
⊢ (∏ᶠ (i : α) (_ : a = i), f i) = f a
simp [@eq_comm _ a]