α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.29986
ι : Sort ?u.29989
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
⊢ ∀ (s : Set γ),
    (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔
      ∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.29986
ι : Sort ?u.29989
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
⊢ map m (f ×ˢ g) = seq (map (fun a b => m (a, b)) f) g
simp [Filter.ext_iff, mem_prod_iff, mem_map_seq_iff]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.29986
ι : Sort ?u.29989
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔
    ∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.29986
ι : Sort ?u.29989
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
⊢ ∀ (s : Set γ),
    (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔
      ∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s
intro s
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.29986
ι : Sort ?u.29989
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s) →
    ∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.29986
ι : Sort ?u.29989
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s) →
    ∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.29986
ι : Sort ?u.29989
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s) ↔
    ∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s
constructor
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.29986
ι : Sort ?u.29989
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s) →
    ∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.29986
ι : Sort ?u.29989
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s) →
    ∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.29986
ι : Sort ?u.29989
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s) →
    ∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s
exact fun ⟨t, ht, s, hs, h⟩ => ⟨s, hs, t, ht, fun x hx y hy => @h ⟨x, y⟩ ⟨hx, hy⟩⟩
no goals
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.29986
ι : Sort ?u.29989
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
m : α × β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ (∃ t, t ∈ g ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), x_1 ∈ x → ∀ (y : β), y ∈ t → m (x_1, y) ∈ s) →
    ∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ m ⁻¹' s
exact fun ⟨s, hs, t, ht, h⟩ => ⟨t, ht, s, hs, fun ⟨x, y⟩ ⟨hx, hy⟩ => h x hx y hy⟩