α : Type u_2
β : Type u_1
γ : Type ?u.1020
δ : Type ?u.1023
ι : Sort ?u.1026
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ comap Prod.fst f ⊓ comap Prod.snd g ↔ ∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ prod t₁ t₂ ⊆ s
α : Type u_2
β : Type u_1
γ : Type ?u.1020
δ : Type ?u.1023
ι : Sort ?u.1026
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g ↔ ∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ t₁ ×ˢ t₂ ⊆ s
simp only [SProd.sprod, Filter.prod]
case mp
α : Type u_2
β : Type u_1
γ : Type ?u.1020
δ : Type ?u.1023
ι : Sort ?u.1026
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ comap Prod.fst f ⊓ comap Prod.snd g → ∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ prod t₁ t₂ ⊆ s

case mpr
α : Type u_2
β : Type u_1
γ : Type ?u.1020
δ : Type ?u.1023
ι : Sort ?u.1026
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ prod t₁ t₂ ⊆ s) → s ∈ comap Prod.fst f ⊓ comap Prod.snd g
α : Type u_2
β : Type u_1
γ : Type ?u.1020
δ : Type ?u.1023
ι : Sort ?u.1026
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ comap Prod.fst f ⊓ comap Prod.snd g ↔ ∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ prod t₁ t₂ ⊆ s
constructor
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.1020
δ : Type ?u.1023
ι : Sort ?u.1026
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
t₁ : Set (α × β)
s₁ : Set α
hs₁ : s₁ ∈ f
hts₁ : Prod.fst ⁻¹' s₁ ⊆ t₁
t₂ : Set (α × β)
s₂ : Set β
hs₂ : s₂ ∈ g
hts₂ : Prod.snd ⁻¹' s₂ ⊆ t₂
⊢ ∃ t₁_1, t₁_1 ∈ f ∧ ∃ t₂_1, t₂_1 ∈ g ∧ prod t₁_1 t₂_1 ⊆ t₁ ∩ t₂
case mp
α : Type u_2
β : Type u_1
γ : Type ?u.1020
δ : Type ?u.1023
ι : Sort ?u.1026
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ comap Prod.fst f ⊓ comap Prod.snd g → ∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ prod t₁ t₂ ⊆ s
rintro ⟨t₁, ⟨s₁, hs₁, hts₁⟩, t₂, ⟨s₂, hs₂, hts₂⟩, rfl⟩
no goals
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.1020
δ : Type ?u.1023
ι : Sort ?u.1026
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
t₁ : Set (α × β)
s₁ : Set α
hs₁ : s₁ ∈ f
hts₁ : Prod.fst ⁻¹' s₁ ⊆ t₁
t₂ : Set (α × β)
s₂ : Set β
hs₂ : s₂ ∈ g
hts₂ : Prod.snd ⁻¹' s₂ ⊆ t₂
⊢ ∃ t₁_1, t₁_1 ∈ f ∧ ∃ t₂_1, t₂_1 ∈ g ∧ prod t₁_1 t₂_1 ⊆ t₁ ∩ t₂
exact ⟨s₁, hs₁, s₂, hs₂, fun p ⟨h, h'⟩ => ⟨hts₁ h, hts₂ h'⟩⟩
case mpr.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.1020
δ : Type ?u.1023
ι : Sort ?u.1026
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
t₁ : Set α
ht₁ : t₁ ∈ f
t₂ : Set β
ht₂ : t₂ ∈ g
h : prod t₁ t₂ ⊆ s
⊢ s ∈ comap Prod.fst f ⊓ comap Prod.snd g
case mpr
α : Type u_2
β : Type u_1
γ : Type ?u.1020
δ : Type ?u.1023
ι : Sort ?u.1026
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t₁, t₁ ∈ f ∧ ∃ t₂, t₂ ∈ g ∧ prod t₁ t₂ ⊆ s) → s ∈ comap Prod.fst f ⊓ comap Prod.snd g
rintro ⟨t₁, ht₁, t₂, ht₂, h⟩
no goals
case mpr.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.1020
δ : Type ?u.1023
ι : Sort ?u.1026
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
t₁ : Set α
ht₁ : t₁ ∈ f
t₂ : Set β
ht₂ : t₂ ∈ g
h : prod t₁ t₂ ⊆ s
⊢ s ∈ comap Prod.fst f ⊓ comap Prod.snd g
exact mem_inf_of_inter (preimage_mem_comap ht₁) (preimage_mem_comap ht₂) h