-- Mathlib/Order/Filter/Map.lean
theorem prod_map_seq_comm (f : Filter α) (g : Filter β) :
    (map Prod.mk f).seq g = seq (map (fun b a => (a, b)) g) f

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs✝ : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ (Prod.mk '' u).seq t ∈ (map (fun b a => (a, b)) g).seq f

Tactic:
rw [Set.prod_image_seq_comm]

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs✝ : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ ((fun b a => (a, b)) '' t).seq u ∈ (map (fun b a => (a, b)) g).seq f

Proof state:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs✝ : s ∈ map (fun b a => (a, b)) g
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun b a => (a, b)) '' u ⊆ s
⊢ ((fun b a => (a, b)) '' u).seq t ∈ (map Prod.mk f).seq g

Tactic:
rw [← Set.prod_image_seq_comm]

Result:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs✝ : s ∈ map (fun b a => (a, b)) g
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun b a => (a, b)) '' u ⊆ s
⊢ (Prod.mk '' t).seq u ∈ (map Prod.mk f).seq g

Proof state:
case refine_2
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
⊢ s.seq t ∈ (map (fun b a => (a, b)) g).seq f

Tactic:
rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs✝ : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ s.seq t ∈ (map (fun b a => (a, b)) g).seq f

Proof state:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs✝ : s ∈ map (fun b a => (a, b)) g
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun b a => (a, b)) '' u ⊆ s
⊢ (Prod.mk '' t).seq u ∈ (map Prod.mk f).seq g

Tactic:
exact seq_mem_seq (image_mem_map ht) hu

Result:
no goals

Proof state:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs✝ : s ∈ map (fun b a => (a, b)) g
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun b a => (a, b)) '' u ⊆ s
⊢ s.seq t ∈ (map Prod.mk f).seq g

Tactic:
refine mem_of_superset ?_ (Set.seq_mono hs Subset.rfl)

Result:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs✝ : s ∈ map (fun b a => (a, b)) g
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun b a => (a, b)) '' u ⊆ s
⊢ ((fun b a => (a, b)) '' u).seq t ∈ (map Prod.mk f).seq g

Proof state:
case refine_1
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs : s ∈ map (fun b a => (a, b)) g
t : Set α
ht : t ∈ f
⊢ s.seq t ∈ (map Prod.mk f).seq g

Tactic:
rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩

Result:
case refine_1.intro.intro
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs✝ : s ∈ map (fun b a => (a, b)) g
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun b a => (a, b)) '' u ⊆ s
⊢ s.seq t ∈ (map Prod.mk f).seq g

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs✝ : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ ((fun b a => (a, b)) '' t).seq u ∈ (map (fun b a => (a, b)) g).seq f

Tactic:
exact seq_mem_seq (image_mem_map ht) hu

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ (map Prod.mk f).seq g = (map (fun b a => (a, b)) g).seq f

Tactic:
refine le_antisymm (le_seq fun s hs t ht => ?_) (le_seq fun s hs t ht => ?_)

Result:
case refine_1
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs : s ∈ map (fun b a => (a, b)) g
t : Set α
ht : t ∈ f
⊢ s.seq t ∈ (map Prod.mk f).seq g

case refine_2
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
⊢ s.seq t ∈ (map (fun b a => (a, b)) g).seq f

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs✝ : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ s.seq t ∈ (map (fun b a => (a, b)) g).seq f

Tactic:
refine mem_of_superset ?_ (Set.seq_mono hs Subset.rfl)

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs✝ : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ (Prod.mk '' u).seq t ∈ (map (fun b a => (a, b)) g).seq f