no goals
α : Type u_1
β : Type ?u.221292
ι : Type ?u.221295
G : Type ?u.221298
M : Type u_2
N : Type ?u.221304
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s✝ t s : Set α
⊢ (∏ᶠ (i : α) (_ : i ∈ s), 1) = 1
simp