no goals
α : Type u_2
β : Type ?u.210357
ι : Type ?u.210360
G : Type ?u.210363
M : Type u_1
N : Type ?u.210369
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g : α → M
a b : α
s t : Set α
f : α → M
h : ∀ (x : α), f x = 1
⊢ (∏ᶠ (i : α), f i) = 1
simp (config := { contextual := true }) [h]