-- Mathlib/Order/Filter/Map.lean
theorem seq_assoc (x : Filter α) (g : Filter (α → β)) (h : Filter (β → γ)) :
    seq h (seq g x) = seq (seq (map (· ∘ ·) h) g) x

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 => x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x1 x2 => x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x1 x2 => x1 ∘ x2) '' w ⊆ u
⊢ w.seq (v.seq t) ∈ h.seq (g.seq x)

Tactic:
exact seq_mem_seq hw (seq_mem_seq hv ht)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
⊢ h.seq (g.seq x) = ((map (fun x1 x2 => x1 ∘ x2) h).seq g).seq x

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
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs : s ∈ (map (fun x1 x2 => x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
⊢ s.seq t ∈ h.seq (g.seq x)

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht : t ∈ g.seq x
⊢ s.seq t ∈ ((map (fun x1 x2 => x1 ∘ x2) h).seq g).seq x

Proof state:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ (((fun x1 x2 => x1 ∘ x2) '' s).seq u).seq v ∈ ((map (fun x1 x2 => x1 ∘ x2) h).seq g).seq x

Tactic:
exact seq_mem_seq (seq_mem_seq (image_mem_map hs) hu) hv

Result:
no goals

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 => x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x1 x2 => x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x1 x2 => x1 ∘ x2) '' w ⊆ u
⊢ (((fun x1 x2 => x1 ∘ x2) '' w).seq v).seq t ∈ h.seq (g.seq x)

Tactic:
rw [← Set.seq_seq]

Result:
case refine_1.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 => x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x1 x2 => x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x1 x2 => x1 ∘ x2) '' w ⊆ u
⊢ w.seq (v.seq t) ∈ h.seq (g.seq x)

Proof state:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ s.seq t ∈ ((map (fun x1 x2 => x1 ∘ x2) h).seq g).seq x

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

Result:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ s.seq (u.seq v) ∈ ((map (fun x1 x2 => x1 ∘ x2) h).seq g).seq x

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs : s ∈ (map (fun x1 x2 => x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
⊢ s.seq t ∈ h.seq (g.seq x)

Tactic:
rcases mem_seq_iff.1 hs with ⟨u, hu, v, hv, hs⟩

Result:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 => x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu : u ∈ map (fun x1 x2 => x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
⊢ s.seq t ∈ h.seq (g.seq x)

Proof state:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ s.seq (u.seq v) ∈ ((map (fun x1 x2 => x1 ∘ x2) h).seq g).seq x

Tactic:
rw [Set.seq_seq]

Result:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ (((fun x1 x2 => x1 ∘ x2) '' s).seq u).seq v ∈ ((map (fun x1 x2 => x1 ∘ x2) h).seq g).seq x

Proof state:
case refine_1.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 => x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x1 x2 => x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x1 x2 => x1 ∘ x2) '' w ⊆ u
⊢ s.seq t ∈ h.seq (g.seq x)

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

Result:
case refine_1.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 => x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x1 x2 => x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x1 x2 => x1 ∘ x2) '' w ⊆ u
⊢ (((fun x1 x2 => x1 ∘ x2) '' w).seq v).seq t ∈ h.seq (g.seq x)

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 => x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu : u ∈ map (fun x1 x2 => x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
⊢ s.seq t ∈ h.seq (g.seq x)

Tactic:
rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hu⟩

Result:
case refine_1.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 => x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x1 x2 => x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x1 x2 => x1 ∘ x2) '' w ⊆ u
⊢ s.seq t ∈ h.seq (g.seq x)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht : t ∈ g.seq x
⊢ s.seq t ∈ ((map (fun x1 x2 => x1 ∘ x2) h).seq g).seq x

Tactic:
rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩

Result:
case refine_2.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ s.seq t ∈ ((map (fun x1 x2 => x1 ∘ x2) h).seq g).seq x