case refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs : s ∈ seq (map (fun x x_1 => x ∘ x_1) h) g
t : Set α
ht : t ∈ x
⊢ Set.seq s t ∈ seq h (seq g x)

case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht : t ∈ seq g x
⊢ Set.seq s t ∈ seq (seq (map (fun x x_1 => x ∘ x_1) h) g) x
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
⊢ seq h (seq g x) = seq (seq (map (fun x x_1 => x ∘ x_1) h) g) x
refine' le_antisymm (le_seq fun s hs t ht => _) (le_seq fun s hs t ht => _)
case refine'_1.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ seq (map (fun x x_1 => x ∘ x_1) h) g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu : u ∈ map (fun x x_1 => x ∘ x_1) h
v : Set (α → β)
hv : v ∈ g
hs : Set.seq u v ⊆ s
⊢ Set.seq s t ∈ seq h (seq g x)
case refine'_1
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs : s ∈ seq (map (fun x x_1 => x ∘ x_1) h) g
t : Set α
ht : t ∈ x
⊢ Set.seq s t ∈ seq h (seq g x)
rcases mem_seq_iff.1 hs with ⟨u, hu, v, hv, hs⟩
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ seq (map (fun x x_1 => x ∘ x_1) h) g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x x_1 => x ∘ x_1) h
v : Set (α → β)
hv : v ∈ g
hs : Set.seq u v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x x_1 => x ∘ x_1) '' w ⊆ u
⊢ Set.seq s t ∈ seq h (seq g x)
case refine'_1.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ seq (map (fun x x_1 => x ∘ x_1) h) g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu : u ∈ map (fun x x_1 => x ∘ x_1) h
v : Set (α → β)
hv : v ∈ g
hs : Set.seq u v ⊆ s
⊢ Set.seq s t ∈ seq h (seq g x)
rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hu⟩
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ seq (map (fun x x_1 => x ∘ x_1) h) g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x x_1 => x ∘ x_1) h
v : Set (α → β)
hv : v ∈ g
hs : Set.seq u v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x x_1 => x ∘ x_1) '' w ⊆ u
⊢ Set.seq (Set.seq ((fun x x_1 => x ∘ x_1) '' w) v) t ∈ seq h (seq g x)
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ seq (map (fun x x_1 => x ∘ x_1) h) g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x x_1 => x ∘ x_1) h
v : Set (α → β)
hv : v ∈ g
hs : Set.seq u v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x x_1 => x ∘ x_1) '' w ⊆ u
⊢ Set.seq s t ∈ seq h (seq g x)
refine' mem_of_superset _ (Set.seq_mono ((Set.seq_mono hu Subset.rfl).trans hs) Subset.rfl)
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ seq (map (fun x x_1 => x ∘ x_1) h) g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x x_1 => x ∘ x_1) h
v : Set (α → β)
hv : v ∈ g
hs : Set.seq u v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x x_1 => x ∘ x_1) '' w ⊆ u
⊢ Set.seq w (Set.seq v t) ∈ seq h (seq g x)
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ seq (map (fun x x_1 => x ∘ x_1) h) g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x x_1 => x ∘ x_1) h
v : Set (α → β)
hv : v ∈ g
hs : Set.seq u v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x x_1 => x ∘ x_1) '' w ⊆ u
⊢ Set.seq (Set.seq ((fun x x_1 => x ∘ x_1) '' w) v) t ∈ seq h (seq g x)
rw [← Set.seq_seq]
no goals
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ seq (map (fun x x_1 => x ∘ x_1) h) g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x x_1 => x ∘ x_1) h
v : Set (α → β)
hv : v ∈ g
hs : Set.seq u v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x x_1 => x ∘ x_1) '' w ⊆ u
⊢ Set.seq w (Set.seq v t) ∈ seq h (seq g x)
exact seq_mem_seq hw (seq_mem_seq hv ht)
case refine'_2.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ seq g x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : Set.seq u v ⊆ t
⊢ Set.seq s t ∈ seq (seq (map (fun x x_1 => x ∘ x_1) h) g) x
case refine'_2
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht : t ∈ seq g x
⊢ Set.seq s t ∈ seq (seq (map (fun x x_1 => x ∘ x_1) h) g) x
rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩
case refine'_2.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ seq g x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : Set.seq u v ⊆ t
⊢ Set.seq s (Set.seq u v) ∈ seq (seq (map (fun x x_1 => x ∘ x_1) h) g) x
case refine'_2.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ seq g x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : Set.seq u v ⊆ t
⊢ Set.seq s t ∈ seq (seq (map (fun x x_1 => x ∘ x_1) h) g) x
refine' mem_of_superset _ (Set.seq_mono Subset.rfl ht)
case refine'_2.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ seq g x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : Set.seq u v ⊆ t
⊢ Set.seq (Set.seq ((fun x x_1 => x ∘ x_1) '' s) u) v ∈ seq (seq (map (fun x x_1 => x ∘ x_1) h) g) x
case refine'_2.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ seq g x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : Set.seq u v ⊆ t
⊢ Set.seq s (Set.seq u v) ∈ seq (seq (map (fun x x_1 => x ∘ x_1) h) g) x
rw [Set.seq_seq]
no goals
case refine'_2.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
δ : Type ?u.294746
ι : Sort x
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ seq g x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : Set.seq u v ⊆ t
⊢ Set.seq (Set.seq ((fun x x_1 => x ∘ x_1) '' s) u) v ∈ seq (seq (map (fun x x_1 => x ∘ x_1) h) g) x
exact seq_mem_seq (seq_mem_seq (image_mem_map hs) hu) hv