α : Type u_2
β : Type ?u.223974
ι : Type ?u.223977
G : Type ?u.223980
M : Type u_1
N : Type ?u.223986
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : (∏ᶠ (i : α) (_ : i ∈ s), f i) ≠ 1
h' : ∀ (x : α), x ∈ s → f x = 1
⊢ False
α : Type u_2
β : Type ?u.223974
ι : Type ?u.223977
G : Type ?u.223980
M : Type u_1
N : Type ?u.223986
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : (∏ᶠ (i : α) (_ : i ∈ s), f i) ≠ 1
⊢ ∃ x, x ∈ s ∧ f x ≠ 1
by_contra' h'
no goals
α : Type u_2
β : Type ?u.223974
ι : Type ?u.223977
G : Type ?u.223980
M : Type u_1
N : Type ?u.223986
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : (∏ᶠ (i : α) (_ : i ∈ s), f i) ≠ 1
h' : ∀ (x : α), x ∈ s → f x = 1
⊢ False
exact h (finprod_mem_of_eqOn_one h')