-- Mathlib/Dynamics/OmegaLimit.lean
theorem omegaLimit_omegaLimit (hf : ∀ t, Tendsto (t + ·) f f) : ω f ϕ (ω f ϕ s) ⊆ ω f ϕ s

Proof state:
case intro.intro.intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
l₂ : (closure (image2 ϕ.toFun u s) ∩ o).Nonempty
l₃ : (o ∩ image2 ϕ.toFun u s).Nonempty
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Tactic:
rcases l₃ with ⟨ϕra, ho, ⟨_, hr, _, ha, hϕra⟩⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
l₂ : (closure (image2 ϕ.toFun u s) ∩ o).Nonempty
ϕra : α
ho : ϕra ∈ o
w✝¹ : τ
hr : w✝¹ ∈ u
w✝ : α
ha : w✝ ∈ s
hϕra : ϕ.toFun w✝¹ w✝ = ϕra
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Proof state:
case intro.intro.intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Tactic:
have l₁ : (ω f ϕ s ∩ o).Nonempty :=
  ht₂.mono
    (inter_subset_inter_left _
      ((isInvariant_iff_image _ _).mp (isInvariant_omegaLimit _ _ _ hf) _))

Result:
case intro.intro.intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Proof state:
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Tactic:
rcases mem_nhds_iff.mp hn with ⟨o, ho₁, ho₂, ho₃⟩

Result:
case intro.intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Proof state:
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
⊢ ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' s ∩ n).Nonempty

Tactic:
rintro n hn u hu

Result:
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Proof state:
case intro.intro
τ : Type u_1
inst✝³ : TopologicalSpace τ
inst✝² : AddCommGroup τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun x => t + x) f f
x✝ : α
h : ∀ n ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (ϕ.toFun x '' ω f ϕ.toFun s ∩ n).Nonempty
n : Set α
hn : n ∈ 𝓝 x✝
u : Set τ
hu : u ∈ f
o : Set α
ho₁ : o ⊆ n
ho₂ : IsOpen o
ho₃ : x✝ ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
b : α
hb₁ : b ∈ closure (image2 ϕ.toFun u s)
hb₂ : b ∈ o
⊢ (o ∩ image2 ϕ.toFun u s).Nonempty

Tactic:
exact mem_closure_iff_nhds.mp hb₁ o (IsOpen.mem_nhds ho₂ hb₂)

Result:
no goals