-- 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
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Tactic:
have l₃ : (o ∩ image2 ϕ u s).Nonempty := by
  rcases l₂ with ⟨b, hb₁, hb₂⟩
  exact mem_closure_iff_nhds.mp hb₁ o (IsOpen.mem_nhds ho₂ hb₂)

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
l₂ : (closure (image2 ϕ.toFun u s) ∩ o).Nonempty
l₃ : (o ∩ image2 ϕ.toFun u s).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 : α),
    (∀ 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:
intro _ h

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 ∈ 𝓝 x✝, ∀ {U : Set τ}, U ∈ f → ∃ 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
⊢ ω f ϕ.toFun (ω f ϕ.toFun s) ⊆ ω f ϕ.toFun s

Tactic:
simp only [subset_def, mem_omegaLimit_iff_frequently₂, frequently_iff]

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 : α),
    (∀ 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

Proof state:
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

Tactic:
exact ⟨_, hr, ϕra, ⟨_, ha, hϕra⟩, ho₁ ho⟩

Result:
no goals

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
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Tactic:
have l₂ : (closure (image2 ϕ u s) ∩ o).Nonempty :=
  l₁.mono fun b hb ↦ ⟨omegaLimit_subset_closure_fw_image _ _ _ hu hb.1, hb.2⟩

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
l₂ : (closure (image2 ϕ.toFun u 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
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
⊢ (o ∩ image2 ϕ.toFun u s).Nonempty

Tactic:
rcases l₂ with ⟨b, hb₁, hb₂⟩

Result:
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

Proof state:
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

Tactic:
rcases h o (IsOpen.mem_nhds ho₂ ho₃) hu with ⟨t, _ht₁, ht₂⟩

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
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty