[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
simp only [SProd.sprod, Filter.prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
rintro ⟨t₁, ⟨s₁, hs₁, hts₁⟩, t₂, ⟨s₂, hs₂, hts₂⟩, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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₂
[PROOFSTEP]
exact ⟨s₁, hs₁, s₂, hs₂, fun p ⟨h, h'⟩ => ⟨hts₁ h, hts₂ h'⟩⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
rintro ⟨t₁, ht₁, t₂, ht₂, h⟩
[GOAL]
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
exact mem_inf_of_inter (preimage_mem_comap ht₁) (preimage_mem_comap ht₂) h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
rw [← @exists_mem_subset_iff _ f, mem_prod_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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}
[PROOFSTEP]
refine' exists_congr fun u => Iff.rfl.and ⟨_, fun h => ⟨t, mem_principal_self t, _⟩⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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}
[PROOFSTEP]
rintro ⟨v, v_in, hv⟩ a a_in b b_in
[GOAL]
case refine'_1.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
exact hv (mk_mem_prod a_in <| v_in b_in)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
rintro ⟨x, y⟩ ⟨hx, hy⟩
[GOAL]
case refine'_2.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
exact h hx y hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
⊢ s ∈ f ×ˢ ⊤ ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f
[PROOFSTEP]
rw [← principal_univ, mem_prod_principal]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
s : Set (α × β)
⊢ {a | ∀ (b : β), b ∈ univ → (a, b) ∈ s} ∈ f ↔ {a | ∀ (b : β), (a, b) ∈ s} ∈ f
[PROOFSTEP]
simp only [mem_univ, forall_true_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f : Filter α
g : Filter β
p : α × β → Prop
s : Set β
⊢ (∀ᶠ (x : α × β) in f ×ˢ 𝓟 s, p x) ↔ ∀ᶠ (x : α) in f, ∀ (y : β), y ∈ s → p (x, y)
[PROOFSTEP]
rw [eventually_iff, eventually_iff, mem_prod_principal]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f : Filter α
g : Filter β
p : α × β → Prop
s : Set β
⊢ {a | ∀ (b : β), b ∈ s → (a, b) ∈ {x | p x}} ∈ f ↔ {x | ∀ (y : β), y ∈ s → p (x, y)} ∈ f
[PROOFSTEP]
simp only [mem_setOf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α → β × γ
b : Filter β
c : Filter γ
⊢ comap f (b ×ˢ c) = comap (Prod.fst ∘ f) b ⊓ comap (Prod.snd ∘ f) c
[PROOFSTEP]
erw [comap_inf, Filter.comap_comap, Filter.comap_comap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
⊢ f ×ˢ ⊤ = comap Prod.fst f
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
⊢ Filter.prod f ⊤ = comap Prod.fst f
[PROOFSTEP]
rw [Filter.prod, comap_top, inf_top_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g✝ : Filter β
f₁ f₂ : Filter α
g : Filter β
⊢ (f₁ ⊔ f₂) ×ˢ g = f₁ ×ˢ g ⊔ f₂ ×ˢ g
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g✝ : Filter β
f₁ f₂ : Filter α
g : Filter β
⊢ Filter.prod (f₁ ⊔ f₂) g = Filter.prod f₁ g ⊔ Filter.prod f₂ g
[PROOFSTEP]
rw [Filter.prod, comap_sup, inf_sup_right, ← Filter.prod, ← Filter.prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊔ g₂) = f ×ˢ g₁ ⊔ f ×ˢ g₂
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
g₁ g₂ : Filter β
⊢ Filter.prod f (g₁ ⊔ g₂) = Filter.prod f g₁ ⊔ Filter.prod f g₂
[PROOFSTEP]
rw [Filter.prod, comap_sup, inf_sup_left, ← Filter.prod, ← Filter.prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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)
[PROOFSTEP]
simpa only [Set.prod_subset_iff] using @mem_prod_iff α β p f g
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
la : Filter α
lb : Filter β
p : α × β → Prop
h : ∀ᶠ (x : α × β) in la ×ˢ lb, p x
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
[PROOFSTEP]
rcases eventually_prod_iff.1 h with ⟨pa, ha, pb, hb, h⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
la : Filter α
lb : Filter β
p : α × β → Prop
h✝ : ∀ᶠ (x : α × β) in la ×ˢ lb, p x
pa : α → Prop
ha : ∀ᶠ (x : α) in la, pa x
pb : β → Prop
hb : ∀ᶠ (y : β) in lb, pb y
h : ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
⊢ ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
[PROOFSTEP]
exact ha.mono fun a ha => hb.mono fun b hb => h ha hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
p : α × α → Prop
h : ∀ᶠ (i : α × α) in f ×ˢ f, p i
⊢ ∀ᶠ (i : α) in f, p (i, i)
[PROOFSTEP]
obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
p : α × α → Prop
h : ∀ᶠ (i : α × α) in f ×ˢ f, p i
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : α → Prop
hs : ∀ᶠ (y : α) in f, s y
hst : ∀ {x : α}, t x → ∀ {y : α}, s y → p (x, y)
⊢ ∀ᶠ (i : α) in f, p (i, i)
[PROOFSTEP]
apply (ht.and hs).mono fun x hx => hst hx.1 hx.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
⊢ (∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.fst, x.fst), x.snd)
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
h : ∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.fst, x.fst), x.snd)
[PROOFSTEP]
obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
h : ∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x
t : α × α → Prop
ht : ∀ᶠ (x : α × α) in f ×ˢ f, t x
s : γ → Prop
hs : ∀ᶠ (y : γ) in g, s y
hst : ∀ {x : α × α}, t x → ∀ {y : γ}, s y → p (x, y)
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.fst, x.fst), x.snd)
[PROOFSTEP]
refine' (ht.diag_of_prod.prod_mk hs).mono fun x hx => by simp only [hst hx.1 hx.2, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : (α × α) × γ → Prop
h : ∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x
t : α × α → Prop
ht : ∀ᶠ (x : α × α) in f ×ˢ f, t x
s : γ → Prop
hs : ∀ᶠ (y : γ) in g, s y
hst : ∀ {x : α × α}, t x → ∀ {y : γ}, s y → p (x, y)
x : α × γ
hx : t (x.fst, x.fst) ∧ s x.snd
⊢ p ((x.fst, x.fst), x.snd)
[PROOFSTEP]
simp only [hst hx.1 hx.2, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
⊢ (∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.fst, x.snd, x.snd)
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.fst, x.snd, x.snd)
[PROOFSTEP]
obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : γ × γ → Prop
hs : ∀ᶠ (y : γ × γ) in g ×ˢ g, s y
hst : ∀ {x : α}, t x → ∀ {y : γ × γ}, s y → p (x, y)
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.fst, x.snd, x.snd)
[PROOFSTEP]
refine' (ht.prod_mk hs.diag_of_prod).mono fun x hx => by simp only [hst hx.1 hx.2, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : γ × γ → Prop
hs : ∀ᶠ (y : γ × γ) in g ×ˢ g, s y
hst : ∀ {x : α}, t x → ∀ {y : γ × γ}, s y → p (x, y)
x : α × γ
hx : t x.fst ∧ s (x.snd, x.snd)
⊢ p (x.fst, x.snd, x.snd)
[PROOFSTEP]
simp only [hst hx.1 hx.2, Prod.mk.eta]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ (⨅ (i : ι), f i) ×ˢ g = ⨅ (i : ι), f i ×ˢ g
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ Filter.prod (⨅ (i : ι), f i) g = ⨅ (i : ι), Filter.prod (f i) g
[PROOFSTEP]
rw [Filter.prod, comap_iInf, iInf_inf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ ⨅ (x : ι), comap Prod.fst (f x) ⊓ comap Prod.snd g = ⨅ (i : ι), Filter.prod (f i) g
[PROOFSTEP]
simp only [Filter.prod, eq_self_iff_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : Filter α
g : ι → Filter β
⊢ f ×ˢ ⨅ (i : ι), g i = ⨅ (i : ι), f ×ˢ g i
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : Filter α
g : ι → Filter β
⊢ Filter.prod f (⨅ (i : ι), g i) = ⨅ (i : ι), Filter.prod f (g i)
[PROOFSTEP]
rw [Filter.prod, comap_iInf, inf_iInf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
inst✝ : Nonempty ι
f : Filter α
g : ι → Filter β
⊢ ⨅ (x : ι), comap Prod.fst f ⊓ comap Prod.snd (g x) = ⨅ (i : ι), Filter.prod f (g i)
[PROOFSTEP]
simp only [Filter.prod, eq_self_iff_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : β₁ → α₁
m₂ : β₂ → α₂
⊢ comap m₁ f₁ ×ˢ comap m₂ f₂ = comap (fun p => (m₁ p.fst, m₂ p.snd)) (f₁ ×ˢ f₂)
[PROOFSTEP]
simp only [SProd.sprod, Filter.prod, comap_comap, comap_inf, (· ∘ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
⊢ f ×ˢ g = comap Prod.swap (g ×ˢ f)
[PROOFSTEP]
simp only [SProd.sprod, Filter.prod, comap_comap, (· ∘ ·), inf_comm, Prod.swap, comap_inf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
⊢ f ×ˢ g = map (fun p => (p.snd, p.fst)) (g ×ˢ f)
[PROOFSTEP]
rw [prod_comm', ← map_swap_eq_comap_swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
⊢ Prod.swap <$> (g ×ˢ f) = map (fun p => (p.snd, p.fst)) (g ×ˢ f)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
simp only [mem_prod_iff, prod_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
refine exists_congr fun _ => Iff.rfl.and <| Iff.trans ?_ exists_mem_subset_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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}
[PROOFSTEP]
exact exists_congr fun _ => Iff.rfl.and forall₂_swap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ f ×ˢ g ↔ ∃ t, t ∈ g ∧ ∀ᶠ (x : α) in f, ∀ (y : β), y ∈ t → (x, y) ∈ s
[PROOFSTEP]
rw [prod_comm, mem_map, mem_prod_iff_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ (∃ t, t ∈ g ∧ ∀ᶠ (y : α) in f, ∀ (x : β), x ∈ t → (x, y) ∈ (fun p => (p.snd, p.fst)) ⁻¹' s) ↔
    ∃ t, t ∈ g ∧ ∀ᶠ (x : α) in f, ∀ (y : β), y ∈ t → (x, y) ∈ s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
inst✝ : NeBot g
⊢ map Prod.fst (f ×ˢ g) = f
[PROOFSTEP]
ext s
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
inst✝ : NeBot g
s : Set α
⊢ s ∈ map Prod.fst (f ×ˢ g) ↔ s ∈ f
[PROOFSTEP]
simp only [mem_map, mem_prod_iff_left, mem_preimage, eventually_const, ← subset_def, exists_mem_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
inst✝ : NeBot f
⊢ map Prod.snd (f ×ˢ g) = g
[PROOFSTEP]
rw [prod_comm, map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
inst✝ : NeBot f
⊢ map (Prod.snd ∘ fun p => (p.snd, p.fst)) (g ×ˢ f) = g
[PROOFSTEP]
apply map_fst_prod
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
⊢ f₁ ×ˢ g₁ = f₂ ×ˢ g₂ ↔ f₁ = f₂ ∧ g₁ = g₂
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.1 ▸ h.2 ▸ rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂
[PROOFSTEP]
have hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂ := prod_le_prod.1 h.le
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
⊢ f₁ = f₂ ∧ g₁ = g₂
[PROOFSTEP]
haveI := neBot_of_le hle.1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this : NeBot f₂
⊢ f₁ = f₂ ∧ g₁ = g₂
[PROOFSTEP]
haveI := neBot_of_le hle.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
inst✝¹ : NeBot f₁
inst✝ : NeBot g₁
h : f₁ ×ˢ g₁ = f₂ ×ˢ g₂
hle : f₁ ≤ f₂ ∧ g₁ ≤ g₂
this✝ : NeBot f₂
this : NeBot g₂
⊢ f₁ = f₂ ∧ g₁ = g₂
[PROOFSTEP]
exact ⟨hle.1.antisymm <| (prod_le_prod.1 h.ge).1, hle.2.antisymm <| (prod_le_prod.1 h.ge).2⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p (Prod.swap y)
[PROOFSTEP]
rw [prod_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in map (fun p => (p.snd, p.fst)) (g ×ˢ f), p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p (Prod.swap y)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
h : Filter γ
⊢ map (↑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h
[PROOFSTEP]
simp_rw [← comap_equiv_symm, SProd.sprod, Filter.prod, comap_inf, comap_comap, inf_assoc, (· ∘ ·),
  Equiv.prodAssoc_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
h : Filter γ
⊢ map (↑(Equiv.prodAssoc α β γ).symm) (f ×ˢ g ×ˢ h) = (f ×ˢ g) ×ˢ h
[PROOFSTEP]
simp_rw [map_equiv_symm, SProd.sprod, Filter.prod, comap_inf, comap_comap, inf_assoc, Function.comp,
  Equiv.prodAssoc_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ map (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ((f ×ˢ g) ×ˢ h ×ˢ k) = (f ×ˢ h) ×ˢ g ×ˢ k
[PROOFSTEP]
simp_rw [map_swap4_eq_comap, SProd.sprod, Filter.prod, comap_inf, comap_comap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
h : Filter γ
k : Filter δ
⊢ comap ((Prod.fst ∘ Prod.fst) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) f ⊓
        comap ((Prod.snd ∘ Prod.fst) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) g ⊓
      (comap ((Prod.fst ∘ Prod.snd) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) h ⊓
        comap ((Prod.snd ∘ Prod.snd) ∘ fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) k) =
    comap (Prod.fst ∘ Prod.fst) f ⊓ comap (Prod.snd ∘ Prod.fst) h ⊓
      (comap (Prod.fst ∘ Prod.snd) g ⊓ comap (Prod.snd ∘ Prod.snd) k)
[PROOFSTEP]
ac_rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
hs : (fun p => (m₁ p.fst, m₂ p.snd)) ⁻¹' s ∈ f₁ ×ˢ f₂
s₁ : Set α₁
hs₁ : s₁ ∈ f₁
s₂ : Set α₂
hs₂ : s₂ ∈ f₂
h : s₁ ×ˢ s₂ ⊆ (fun p => (m₁ p.fst, m₂ p.snd)) ⁻¹' s
⊢ (m₁ '' s₁) ×ˢ (m₂ '' s₂) ⊆ s
[PROOFSTEP]
rwa [prod_image_image_eq, image_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α → β
F : Filter α
G : Filter γ
⊢ map f F ×ˢ G = map (Prod.map f id) (F ×ˢ G)
[PROOFSTEP]
rw [← prod_map_map_eq', map_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : β → γ
F : Filter α
G : Filter β
⊢ F ×ˢ map f G = map (Prod.map id f) (F ×ˢ G)
[PROOFSTEP]
rw [← prod_map_map_eq', map_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ✝ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)
[PROOFSTEP]
erw [Tendsto, ← prod_map_map_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ✝ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
δ : Type u_6
f : α → γ
g : β → δ
a : Filter α
b : Filter β
c : Filter γ
d : Filter δ
hf : Tendsto f a c
hg : Tendsto g b d
⊢ map f a ×ˢ map g b ≤ c ×ˢ d
[PROOFSTEP]
exact Filter.prod_mono hf hg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
simp [Filter.ext_iff, mem_prod_iff, mem_map_seq_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
intro s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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_4
ι : Sort u_5
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
[PROOFSTEP]
exact fun ⟨t, ht, s, hs, h⟩ => ⟨s, hs, t, ht, fun x hx y hy => @h ⟨x, y⟩ ⟨hx, hy⟩⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
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
[PROOFSTEP]
exact fun ⟨s, hs, t, ht, h⟩ => ⟨t, ht, s, hs, fun ⟨x, y⟩ ⟨hx, hy⟩ => h x hx y hy⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
⊢ f ×ˢ g = seq (map Prod.mk f) g
[PROOFSTEP]
have h := f.map_prod id g
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
h : map id (f ×ˢ g) = seq (map (fun a b => id (a, b)) f) g
⊢ f ×ˢ g = seq (map Prod.mk f) g
[PROOFSTEP]
rwa [map_id] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
f₁ f₂ : Filter α
g₁ g₂ : Filter β
⊢ f₁ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂)
[PROOFSTEP]
simp only [SProd.sprod, Filter.prod, comap_inf, inf_comm, inf_assoc, inf_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g✝ : Filter β
f₁ f₂ : Filter α
g : Filter β
⊢ (f₁ ⊓ f₂) ×ˢ g = f₁ ×ˢ g ⊓ f₂ ×ˢ g
[PROOFSTEP]
rw [prod_inf_prod, inf_idem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
g₁ g₂ : Filter β
⊢ f ×ˢ (g₁ ⊓ g₂) = f ×ˢ g₁ ⊓ f ×ˢ g₂
[PROOFSTEP]
rw [prod_inf_prod, inf_idem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f : Filter α
g : Filter β
s : Set α
t : Set β
⊢ 𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t)
[PROOFSTEP]
simp only [SProd.sprod, Filter.prod, comap_principal, principal_eq_iff_eq, comap_principal, inf_principal]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t✝ : Set β
f : Filter α
g : Filter β
s : Set α
t : Set β
⊢ Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t = prod s t
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
a : α
f : Filter β
⊢ pure a ×ˢ f = map (Prod.mk a) f
[PROOFSTEP]
rw [prod_eq, map_pure, pure_seq_eq_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (pure a ×ˢ B) = map (f a) B
[PROOFSTEP]
rw [Filter.pure_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (map (Prod.mk a) B) = map (f a) B
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
b : β
⊢ f ×ˢ pure b = map (fun a => (a, b)) f
[PROOFSTEP]
rw [prod_eq, seq_pure, map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
b : β
⊢ map ((fun g => g b) ∘ Prod.mk) f = map (fun a => (a, b)) f
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f : Filter α
g : Filter β
a : α
b : β
⊢ pure a ×ˢ pure b = pure (a, b)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
⊢ f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥
[PROOFSTEP]
simp_rw [← empty_mem_iff_bot, mem_prod_iff, subset_empty_iff, prod_eq_empty_iff, ← exists_prop, Subtype.exists',
  exists_or, exists_const, Subtype.exists, exists_prop, exists_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
⊢ NeBot (f ×ˢ g) ↔ NeBot f ∧ NeBot g
[PROOFSTEP]
simp only [neBot_iff, Ne, prod_eq_bot, not_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α × β → γ
x : Filter α
y : Filter β
z : Filter γ
⊢ Tendsto f (x ×ˢ y) z ↔
    ∀ (W : Set γ), W ∈ z → ∃ U, U ∈ x ∧ ∃ V, V ∈ y ∧ ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W
[PROOFSTEP]
simp only [tendsto_def, mem_prod_iff, prod_sub_preimage_iff, exists_prop, iff_self_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter (α × β)
g : Filter α
g' : Filter β
⊢ f ≤ g ×ˢ g' ↔ Tendsto Prod.fst f g ∧ Tendsto Prod.snd f g'
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter (α × β)
g : Filter α
g' : Filter β
⊢ f ≤ Filter.prod g g' ↔ Tendsto Prod.fst f g ∧ Tendsto Prod.snd f g'
[PROOFSTEP]
unfold Filter.prod
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter (α × β)
g : Filter α
g' : Filter β
⊢ f ≤ comap Prod.fst g ⊓ comap Prod.snd g' ↔ Tendsto Prod.fst f g ∧ Tendsto Prod.snd f g'
[PROOFSTEP]
simp only [le_inf_iff, ← map_le_iff_le_comap, Tendsto]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
g' : Filter γ
s : α → β × γ
⊢ Tendsto s f (g ×ˢ g') ↔ Tendsto (fun n => (s n).fst) f g ∧ Tendsto (fun n => (s n).snd) f g'
[PROOFSTEP]
dsimp only [SProd.sprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
g' : Filter γ
s : α → β × γ
⊢ Tendsto s f (Filter.prod g g') ↔ Tendsto (fun n => (s n).fst) f g ∧ Tendsto (fun n => (s n).snd) f g'
[PROOFSTEP]
unfold Filter.prod
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
g' : Filter γ
s : α → β × γ
⊢ Tendsto s f (comap Prod.fst g ⊓ comap Prod.snd g') ↔
    Tendsto (fun n => (s n).fst) f g ∧ Tendsto (fun n => (s n).snd) f g'
[PROOFSTEP]
simp only [tendsto_inf, tendsto_comap_iff, (· ∘ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f✝ : Filter α
g✝ : Filter β
s : Set (α × β)
f : Filter α
g : Filter β
⊢ s ∈ Filter.coprod f g ↔ (∃ t₁, t₁ ∈ f ∧ Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂, t₂ ∈ g ∧ Prod.snd ⁻¹' t₂ ⊆ s
[PROOFSTEP]
simp [Filter.coprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g l : Filter β
⊢ Filter.coprod ⊥ l = comap Prod.snd l
[PROOFSTEP]
simp [Filter.coprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
l : Filter α
⊢ Filter.coprod l ⊥ = comap Prod.fst l
[PROOFSTEP]
simp [Filter.coprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
⊢ Filter.coprod ⊥ ⊥ = ⊥
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
s : Set (α × β)
la : Filter α
lb : Filter β
⊢ sᶜ ∈ Filter.coprod la lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb
[PROOFSTEP]
simp only [Filter.coprod, mem_sup, compl_mem_comap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
⊢ NeBot (Filter.coprod f g) ↔ NeBot f ∧ Nonempty β ∨ Nonempty α ∧ NeBot g
[PROOFSTEP]
simp [Filter.coprod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
s : Set α
t : Set β
⊢ Filter.coprod (𝓟 s) (𝓟 t) = 𝓟 (sᶜ ×ˢ tᶜ)ᶜ
[PROOFSTEP]
rw [Filter.coprod, comap_principal, comap_principal, sup_principal, Set.prod_eq, compl_inter, preimage_compl,
  preimage_compl, compl_compl, compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
⊢ map (Prod.map m₁ m₂) (Filter.coprod f₁ f₂) ≤ Filter.coprod (map m₁ f₁) (map m₂ f₂)
[PROOFSTEP]
intro s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
⊢ s ∈ Filter.coprod (map m₁ f₁) (map m₂ f₂) → s ∈ map (Prod.map m₁ m₂) (Filter.coprod f₁ f₂)
[PROOFSTEP]
simp only [mem_map, mem_coprod_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
⊢ ((∃ t₁, m₁ ⁻¹' t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂, m₂ ⁻¹' t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ s) →
    (∃ t₁, t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂, t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s
[PROOFSTEP]
rintro ⟨⟨u₁, hu₁, h₁⟩, u₂, hu₂, h₂⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
⊢ (∃ t₁, t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂, t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s
[PROOFSTEP]
refine' ⟨⟨m₁ ⁻¹' u₁, hu₁, fun _ hx => h₁ _⟩, ⟨m₂ ⁻¹' u₂, hu₂, fun _ hx => h₂ _⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
x✝ : α₁ × α₂
hx : x✝ ∈ Prod.fst ⁻¹' (m₁ ⁻¹' u₁)
⊢ Prod.map m₁ m₂ x✝ ∈ Prod.fst ⁻¹' u₁
[PROOFSTEP]
convert hx
[GOAL]
case intro.intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
u₁ : Set β₁
hu₁ : m₁ ⁻¹' u₁ ∈ f₁
h₁ : Prod.fst ⁻¹' u₁ ⊆ s
u₂ : Set β₂
hu₂ : m₂ ⁻¹' u₂ ∈ f₂
h₂ : Prod.snd ⁻¹' u₂ ⊆ s
x✝ : α₁ × α₂
hx : x✝ ∈ Prod.snd ⁻¹' (m₂ ⁻¹' u₂)
⊢ Prod.map m₁ m₂ x✝ ∈ Prod.snd ⁻¹' u₂
[PROOFSTEP]
convert hx
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ Filter.coprod (map (fun x => b) (𝓟 {a})) (map id (𝓟 {i})) = 𝓟 ({b} ×ˢ univ ∪ univ ×ˢ {i})
[PROOFSTEP]
simp only [map_principal, Filter.coprod, comap_principal, sup_principal, image_singleton, image_id, prod_univ,
  univ_prod, id]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ map (Prod.map (fun x => b) id) (Filter.coprod (𝓟 {a}) (𝓟 {i})) = 𝓟 ({b} ×ˢ univ)
[PROOFSTEP]
rw [principal_coprod_principal, map_principal]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ 𝓟 (Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ) = 𝓟 ({b} ×ˢ univ)
[PROOFSTEP]
congr
[GOAL]
case e_s
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
⊢ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ = {b} ×ˢ univ
[PROOFSTEP]
ext ⟨b', i'⟩
[GOAL]
case e_s.h.mk
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ↔ (b', i') ∈ {b} ×ˢ univ
[PROOFSTEP]
constructor
[GOAL]
case e_s.h.mk.mp
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ → (b', i') ∈ {b} ×ˢ univ
[PROOFSTEP]
rintro ⟨⟨a'', i''⟩, _, h₂, h₃⟩
[GOAL]
case e_s.h.mk.mp.intro.mk.intro.refl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
a'' : α
i'' : ι
left✝ : (a'', i'') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
⊢ ((fun x => b) a'', id i'') ∈ {b} ×ˢ univ
[PROOFSTEP]
simp
[GOAL]
case e_s.h.mk.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
⊢ (b', i') ∈ {b} ×ˢ univ → (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
[PROOFSTEP]
rintro ⟨h₁, _⟩
[GOAL]
case e_s.h.mk.mpr.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').fst ∈ {b}
right✝ : (b', i').snd ∈ univ
⊢ (b', i') ∈ Prod.map (fun x => b) id '' ({a}ᶜ ×ˢ {i}ᶜ)ᶜ
[PROOFSTEP]
use(a, i')
[GOAL]
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
ι✝ : Sort u_5
f : Filter α✝
g : Filter β✝
α : Type u_6
β : Type u_7
ι : Type u_8
a : α
b : β
i : ι
b' : β
i' : ι
h₁ : (b', i').fst ∈ {b}
right✝ : (b', i').snd ∈ univ
⊢ (a, i') ∈ ({a}ᶜ ×ˢ {i}ᶜ)ᶜ ∧ Prod.map (fun x => b) id (a, i') = (b', i')
[PROOFSTEP]
simpa using h₁.symm
