no goals
α : Type u_1
β : Type u_2
γ : Type ?u.6291
δ : Type ?u.6294
ι : Sort ?u.6297
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
p : α × β → Prop
f : Filter α
g : Filter β
⊢ (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔
    ∃ pa, (∀ᶠ (x : α) in f, pa x) ∧ ∃ pb, (∀ᶠ (y : β) in g, pb y) ∧ ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
simpa only [Set.prod_subset_iff] using @mem_prod_iff α β p f g