no goals
α : Type u_1
β : Type ?u.204667
ι : Type ?u.204670
G : Type ?u.204673
M : Type u_2
N : Type ?u.204679
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s : Set α
h : ∀ (x : α), x ∈ s → f x = 1
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i) = 1
simp (config := { contextual := true }) [h]