α : Type u_1
β : Type u_2
γ : Type ?u.2996
δ : Type ?u.2999
ι : Sort ?u.3002
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ 𝓟 t ∧ t₁ ×ˢ t₂ ⊆ s) ↔ ∃ t_1, t_1 ∈ f ∧ t_1 ⊆ {a | ∀ (b : β), b ∈ t → (a, b) ∈ s}
α : Type u_1
β : Type u_2
γ : Type ?u.2996
δ : Type ?u.2999
ι : Sort ?u.3002
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
⊢ s ∈ f ×ˢ 𝓟 t ↔ {a | ∀ (b : β), b ∈ t → (a, b) ∈ s} ∈ f
rw [← @exists_mem_subset_iff _ f, mem_prod_iff]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.2996
δ : Type ?u.2999
ι : Sort ?u.3002
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
u : Set α
⊢ (∃ t₂, t₂ ∈ 𝓟 t ∧ u ×ˢ t₂ ⊆ s) → u ⊆ {a | ∀ (b : β), b ∈ t → (a, b) ∈ s}

case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.2996
δ : Type ?u.2999
ι : Sort ?u.3002
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
u : Set α
h : u ⊆ {a | ∀ (b : β), b ∈ t → (a, b) ∈ s}
⊢ u ×ˢ t ⊆ s
α : Type u_1
β : Type u_2
γ : Type ?u.2996
δ : Type ?u.2999
ι : Sort ?u.3002
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ 𝓟 t ∧ t₁ ×ˢ t₂ ⊆ s) ↔ ∃ t_1, t_1 ∈ f ∧ t_1 ⊆ {a | ∀ (b : β), b ∈ t → (a, b) ∈ s}
refine' exists_congr fun u => Iff.rfl.and ⟨_, fun h => ⟨t, mem_principal_self t, _⟩⟩
case refine'_1.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.2996
δ : Type ?u.2999
ι : Sort ?u.3002
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
u : Set α
v : Set β
v_in : v ∈ 𝓟 t
hv : u ×ˢ v ⊆ s
a : α
a_in : a ∈ u
b : β
b_in : b ∈ t
⊢ (a, b) ∈ s
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.2996
δ : Type ?u.2999
ι : Sort ?u.3002
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
u : Set α
⊢ (∃ t₂, t₂ ∈ 𝓟 t ∧ u ×ˢ t₂ ⊆ s) → u ⊆ {a | ∀ (b : β), b ∈ t → (a, b) ∈ s}
rintro ⟨v, v_in, hv⟩ a a_in b b_in
no goals
case refine'_1.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.2996
δ : Type ?u.2999
ι : Sort ?u.3002
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
u : Set α
v : Set β
v_in : v ∈ 𝓟 t
hv : u ×ˢ v ⊆ s
a : α
a_in : a ∈ u
b : β
b_in : b ∈ t
⊢ (a, b) ∈ s
exact hv (mk_mem_prod a_in <| v_in b_in)
case refine'_2.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.2996
δ : Type ?u.2999
ι : Sort ?u.3002
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
u : Set α
h : u ⊆ {a | ∀ (b : β), b ∈ t → (a, b) ∈ s}
x : α
y : β
hx : (x, y).fst ∈ u
hy : (x, y).snd ∈ t
⊢ (x, y) ∈ s
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.2996
δ : Type ?u.2999
ι : Sort ?u.3002
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
u : Set α
h : u ⊆ {a | ∀ (b : β), b ∈ t → (a, b) ∈ s}
⊢ u ×ˢ t ⊆ s
rintro ⟨x, y⟩ ⟨hx, hy⟩
no goals
case refine'_2.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.2996
δ : Type ?u.2999
ι : Sort ?u.3002
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
t : Set β
u : Set α
h : u ⊆ {a | ∀ (b : β), b ∈ t → (a, b) ∈ s}
x : α
y : β
hx : (x, y).fst ∈ u
hy : (x, y).snd ∈ t
⊢ (x, y) ∈ s
exact h hx y hy