no goals
α : Type u_2
β : Type u_3
A : Type u_1
B : Type ?u.102217
M : Type ?u.102220
N : Type ?u.102223
P : Type ?u.102226
R : Type ?u.102229
S : Type ?u.102232
G : Type ?u.102235
M₀ : Type ?u.102238
G₀ : Type ?u.102241
ι : Sort ?u.102244
inst✝² : CommMonoidWithZero A
inst✝¹ : NoZeroDivisors A
inst✝ : Nontrivial A
s : Finset α
f : α → β → A
x : β
⊢ (x ∈ support fun x => ∏ i in s, f i x) ↔ x ∈ ⋂ (i : α) (_ : i ∈ s), support (f i)
simp [support, Ne.def, Finset.prod_eq_zero_iff, mem_setOf_eq, Set.mem_iInter, not_exists]