case refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
f : Filter α
g : Filter β
s : Set (α → α × β)
hs : s ∈ map (fun b a => (a, b)) g
t : Set α
ht : t ∈ f
⊢ Set.seq s t ∈ seq (map Prod.mk f) g

case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
f : Filter α
g : Filter β
s : Set (β → α × β)
hs : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
⊢ Set.seq s t ∈ seq (map (fun b a => (a, b)) g) f
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
f : Filter α
g : Filter β
⊢ seq (map Prod.mk f) g = seq (map (fun b a => (a, b)) g) f
refine' le_antisymm (le_seq fun s hs t ht => _) (le_seq fun s hs t ht => _)
case refine'_1.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
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
⊢ Set.seq s t ∈ seq (map Prod.mk f) g
case refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
f : Filter α
g : Filter β
s : Set (α → α × β)
hs : s ∈ map (fun b a => (a, b)) g
t : Set α
ht : t ∈ f
⊢ Set.seq s t ∈ seq (map Prod.mk f) g
rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩
case refine'_1.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
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
⊢ Set.seq ((fun b a => (a, b)) '' u) t ∈ seq (map Prod.mk f) g
case refine'_1.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
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
⊢ Set.seq s t ∈ seq (map Prod.mk f) g
refine' mem_of_superset _ (Set.seq_mono hs Subset.rfl)
case refine'_1.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
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
⊢ Set.seq (Prod.mk '' t) u ∈ seq (map Prod.mk f) g
case refine'_1.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
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
⊢ Set.seq ((fun b a => (a, b)) '' u) t ∈ seq (map Prod.mk f) g
rw [← Set.prod_image_seq_comm]
no goals
case refine'_1.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
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
⊢ Set.seq (Prod.mk '' t) u ∈ seq (map Prod.mk f) g
exact seq_mem_seq (image_mem_map ht) hu
case refine'_2.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
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
⊢ Set.seq s t ∈ seq (map (fun b a => (a, b)) g) f
case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
f : Filter α
g : Filter β
s : Set (β → α × β)
hs : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
⊢ Set.seq s t ∈ seq (map (fun b a => (a, b)) g) f
rcases mem_map_iff_exists_image.1 hs with ⟨u, hu, hs⟩
case refine'_2.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
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
⊢ Set.seq (Prod.mk '' u) t ∈ seq (map (fun b a => (a, b)) g) f
case refine'_2.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
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
⊢ Set.seq s t ∈ seq (map (fun b a => (a, b)) g) f
refine' mem_of_superset _ (Set.seq_mono hs Subset.rfl)
case refine'_2.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
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
⊢ Set.seq ((fun b a => (a, b)) '' t) u ∈ seq (map (fun b a => (a, b)) g) f
case refine'_2.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
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
⊢ Set.seq (Prod.mk '' u) t ∈ seq (map (fun b a => (a, b)) g) f
rw [Set.prod_image_seq_comm]
no goals
case refine'_2.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.295875
ι : Sort x
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
⊢ Set.seq ((fun b a => (a, b)) '' t) u ∈ seq (map (fun b a => (a, b)) g) f
exact seq_mem_seq (image_mem_map ht) hu