α : Type u_2
β : Type u_1
γ : Type ?u.15041
δ : Type ?u.15044
ι : Sort ?u.15047
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ ∀ (x : α), x ∈ t₁ → ∀ (y : β), y ∈ t₂ → (x, y) ∈ s) ↔
    ∃ t, t ∈ f ∧ ∀ᶠ (y : β) in g, ∀ (x : α), x ∈ t → (x, y) ∈ s
α : Type u_2
β : Type u_1
γ : Type ?u.15041
δ : Type ?u.15044
ι : Sort ?u.15047
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g ↔ ∃ t, t ∈ f ∧ ∀ᶠ (y : β) in g, ∀ (x : α), x ∈ t → (x, y) ∈ s
simp only [mem_prod_iff, prod_subset_iff]
α : Type u_2
β : Type u_1
γ : Type ?u.15041
δ : Type ?u.15044
ι : Sort ?u.15047
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
x✝ : Set α
⊢ (∃ t₂, t₂ ∈ g ∧ ∀ (x : α), x ∈ x✝ → ∀ (y : β), y ∈ t₂ → (x, y) ∈ s) ↔
    ∃ t, t ∈ g ∧ t ⊆ {x | (fun y => ∀ (x : α), x ∈ x✝ → (x, y) ∈ s) x}
α : Type u_2
β : Type u_1
γ : Type ?u.15041
δ : Type ?u.15044
ι : Sort ?u.15047
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ ∀ (x : α), x ∈ t₁ → ∀ (y : β), y ∈ t₂ → (x, y) ∈ s) ↔
    ∃ t, t ∈ f ∧ ∀ᶠ (y : β) in g, ∀ (x : α), x ∈ t → (x, y) ∈ s
refine exists_congr fun _ => Iff.rfl.and <| Iff.trans ?_ exists_mem_subset_iff
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.15041
δ : Type ?u.15044
ι : Sort ?u.15047
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
x✝ : Set α
⊢ (∃ t₂, t₂ ∈ g ∧ ∀ (x : α), x ∈ x✝ → ∀ (y : β), y ∈ t₂ → (x, y) ∈ s) ↔
    ∃ t, t ∈ g ∧ t ⊆ {x | (fun y => ∀ (x : α), x ∈ x✝ → (x, y) ∈ s) x}
exact exists_congr fun _ => Iff.rfl.and forall₂_swap