awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst_1 : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst] (image2 ϕ v s) ⊆ c
u : (↑f.sets : Type u_1)
⊢ (image2 ϕ ((↑u : Set τ) ∩ v) s).Nonempty

Tactic:
have hn : (image2 ϕ (u ∩ v) s).Nonempty :=
      Nonempty.image2 (Filter.nonempty_of_mem (inter_mem u.prop hv₁)) hs
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst_1 : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst] (image2 ϕ v s) ⊆ c
u : (↑f.sets : Type u_1)
hn : (image2 ϕ ((↑u : Set τ) ∩ v) s).Nonempty
⊢ (closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s)).Nonempty

Tactic:
hn.mono subset_closure

Premises used: subset_closure, Set.Nonempty.mono
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst_1 : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst] (image2 ϕ v s) ⊆ c
u : (↑f.sets : Type u_1)
hn : (image2 ϕ ((↑u : Set τ) ∩ v) s).Nonempty
⊢ (closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s)).Nonempty

Tactic:
exact hn.mono subset_closure

Premises used: subset_closure, Set.Nonempty.mono
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst_1 : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst] (image2 ϕ v s) ⊆ c
i : (↑f.sets : Type u_1)
htc : closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s) ⊆ c
⊢ IsCompact (closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))

Tactic:
apply hc₁.of_isClosed_subset isClosed_closure

Premises used: IsCompact.of_isClosed_subset, isClosed_closure
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst_1 : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst] (image2 ϕ v s) ⊆ c
i : (↑f.sets : Type u_1)
⊢ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s) ⊆ closure[inst] (image2 ϕ v s)

Tactic:
closure_mono (image2_subset inter_subset_right Subset.rfl)

Premises used: Set.image2_subset, closure_mono, Set.Subset.rfl, Set.inter_subset_right
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst_1 : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst] (image2 ϕ v s) ⊆ c
i : (↑f.sets : Type u_1)
⊢ closure[inst] (image2 ϕ v s) ⊆ c

Tactic:
hv₂
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst_1 : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst] (image2 ϕ v s) ⊆ c
i : (↑f.sets : Type u_1)
⊢ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s) ⊆ c

Tactic:
calc
      _ ⊆ closure (image2 ϕ v s) := closure_mono (image2_subset inter_subset_right Subset.rfl)
      _ ⊆ c := hv₂

Premises used: Set.image2_subset, closure_mono, Set.Subset.rfl, closure, Set.image2, Set.inter_subset_right
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst_1 : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : (↑f.sets : Type u_1)), IsClosed[inst] (closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))

Tactic:
fun _ ↦ isClosed_closure

Premises used: isClosed_closure
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst_1 : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : (↑f.sets : Type u_1)), IsClosed[inst] (closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))

Tactic:
exact fun _ ↦ isClosed_closure

Premises used: isClosed_closure
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst_1 : CompactSpace β
inst_2 : f.NeBot
hs : s.Nonempty
⊢ (ω f ϕ s).Nonempty

Tactic:
nonempty_omegaLimit_of_isCompact_absorbing _ _ _ isCompact_univ ⟨univ, univ_mem, subset_univ _⟩ hs

Premises used: Set.subset_univ, Set.univ, nonempty_omegaLimit_of_isCompact_absorbing, isCompact_univ, And.intro, Exists.intro, Filter.univ_mem
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddMonoid τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun (x : τ) ↦ t + x) f f
⊢ IsInvariant ϕ.toFun (ω f ϕ.toFun s)

Tactic:
fun t ↦ MapsTo.mono_right ?_ (omegaLimit_subset_of_tendsto ϕ s (hf t))

Premises used: Set.MapsTo.mono_right, omegaLimit_subset_of_tendsto, IsInvariant, Flow.toFun
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddMonoid τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun (x : τ) ↦ t + x) f f
refine : ∀ (t : τ), MapsTo (ϕ.toFun t) (ω f ϕ.toFun s) (ω f (fun (t_1 : τ) (x : α) ↦ ϕ.toFun (t + t_1) x) s)
⊢ IsInvariant ϕ.toFun (ω f ϕ.toFun s)

Tactic:
refine fun t ↦ MapsTo.mono_right ?_ (omegaLimit_subset_of_tendsto ϕ s (hf t))

Premises used: Set.MapsTo.mono_right, omegaLimit_subset_of_tendsto, Flow.toFun
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddMonoid τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun (x : τ) ↦ t + x) f f
t : τ
⊢ MapsTo (ϕ.toFun t) (ω f ϕ.toFun s) (ω f (fun (t_1 : τ) (x : α) ↦ ϕ.toFun (t + t_1) x) s)

Tactic:
mapsTo_omegaLimit _ (mapsTo_id _) (fun t' x ↦ (ϕ.map_add _ _ _).symm)
      (continuous_const.flow ϕ continuous_id)

Premises used: Continuous.flow, Set.mapsTo_id, continuous_const, Flow.map_add, mapsTo_omegaLimit, continuous_id, Eq.symm
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddMonoid τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun (x : τ) ↦ t + x) f f
t : τ
⊢ MapsTo (ϕ.toFun t) (ω f ϕ.toFun s) (ω f (fun (t_1 : τ) (x : α) ↦ ϕ.toFun (t + t_1) x) s)

Tactic:
exact
    mapsTo_omegaLimit _ (mapsTo_id _) (fun t' x ↦ (ϕ.map_add _ _ _).symm)
      (continuous_const.flow ϕ continuous_id)

Premises used: Continuous.flow, Set.mapsTo_id, continuous_const, id, Flow.map_add, mapsTo_omegaLimit, continuous_id, Eq.symm
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddMonoid τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun (x : τ) ↦ x + t) f f
simp : ω f (fun (t_1 : τ) (x : α) ↦ ϕ.toFun (t_1 + t) x) s ⊆ ω f ϕ.toFun s
⊢ ω f ϕ.toFun (ϕ.toFun t '' s) ⊆ ω f ϕ.toFun s

Tactic:
simp only [omegaLimit_image_eq, ← map_add]

Premises used: omegaLimit_image_eq, Flow.map_add
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddMonoid τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun (x : τ) ↦ x + t) f f
⊢ ω f (fun (t_1 : τ) (x : α) ↦ ϕ.toFun (t_1 + t) x) s ⊆ ω f ϕ.toFun s

Tactic:
omegaLimit_subset_of_tendsto ϕ s ht

Premises used: omegaLimit_subset_of_tendsto, Flow.toFun
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddMonoid τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
t : τ
ht : Tendsto (fun (x : τ) ↦ x + t) f f
⊢ ω f (fun (t_1 : τ) (x : α) ↦ ϕ.toFun (t_1 + t) x) s ⊆ ω f ϕ.toFun s

Tactic:
exact omegaLimit_subset_of_tendsto ϕ s ht

Premises used: omegaLimit_subset_of_tendsto, Flow.toFun
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddCommGroup τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun (x : τ) ↦ x + t) f f
t : τ
⊢ ω f ϕ.toFun s = ω f ϕ.toFun (ϕ.toFun (-t) '' ϕ.toFun t '' s)

Tactic:
simp [image_image, ← map_add]

Premises used: Set.image_image, Flow.map_add
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddCommGroup τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
f : Filter τ
ϕ : Flow τ α
s : Set α
hf : ∀ (t : τ), Tendsto (fun (x : τ) ↦ t + x) f f
simp :
  ∀ (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
⊢ ω f ϕ.toFun (ω f ϕ.toFun s) ⊆ ω f ϕ.toFun s

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

Premises used: Filter.frequently_iff, Set.subset_def, mem_omegaLimit_iff_frequently₂
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddCommGroup τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : 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
rcases : ∀ (o : Set α) (ho₁ : o ⊆ n) (ho₂ : IsOpen[inst_3] o) (ho₃ : x ∈ o), ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

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

Premises used: mem_nhds_iff, Iff.mp
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddCommGroup τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : 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[inst_3] o
ho₃ : x ∈ o
rcases :
  ∀ (t : τ) (_ht₁ : t ∈ u) (ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty), ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

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

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddCommGroup τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : 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[inst_3] o
ho₃ : x ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
⊢ (ω f ϕ.toFun s ∩ o).Nonempty

Tactic:
have l₁ : (ω f ϕ s ∩ o).Nonempty :=
    ht₂.mono
      (inter_subset_inter_left _
        ((isInvariant_iff_image _ _).mp (isInvariant_omegaLimit _ _ _ hf) _))
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddCommGroup τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : 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[inst_3] o
ho₃ : x ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
⊢ (closure[inst_3] (image2 ϕ.toFun u s) ∩ o).Nonempty

Tactic:
have l₂ : (closure (image2 ϕ u s) ∩ o).Nonempty :=
    l₁.mono fun b hb ↦ ⟨omegaLimit_subset_closure_image2 _ _ _ hu hb.1, hb.2⟩
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddCommGroup τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : 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[inst_3] o
ho₃ : x ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
l₂ : (closure[inst_3] (image2 ϕ.toFun u s) ∩ o).Nonempty
rcases : ∀ (b : α) (hb₁ : b ∈ closure[inst_3] (image2 ϕ.toFun u s)) (hb₂ : b ∈ o), (o ∩ image2 ϕ.toFun u s).Nonempty
⊢ (o ∩ image2 ϕ.toFun u s).Nonempty

Tactic:
rcases l₂ with ⟨b, hb₁, hb₂⟩
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddCommGroup τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : 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[inst_3] 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[inst_3] (image2 ϕ.toFun u s)
hb₂ : b ∈ o
⊢ (o ∩ image2 ϕ.toFun u s).Nonempty

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

Premises used: mem_closure_iff_nhds, IsOpen.mem_nhds, Iff.mp
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddCommGroup τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : 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[inst_3] 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[inst_3] (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₂)

Premises used: mem_closure_iff_nhds, IsOpen.mem_nhds, Iff.mp
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddCommGroup τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : 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[inst_3] o
ho₃ : x ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
l₂ : (closure[inst_3] (image2 ϕ.toFun u s) ∩ o).Nonempty
⊢ (o ∩ image2 ϕ.toFun u s).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₂)
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddCommGroup τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : 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[inst_3] o
ho₃ : x ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
l₂ : (closure[inst_3] (image2 ϕ.toFun u s) ∩ o).Nonempty
l₃ : (o ∩ image2 ϕ.toFun u s).Nonempty
rcases :
  ∀ (ϕra : α) (ho : ϕra ∈ o) (w : τ) (hr : w ∈ u) (w_1 : α) (ha : w_1 ∈ s) (hϕra : ϕ.toFun w w_1 = ϕra),
    ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Tactic:
rcases l₃ with ⟨ϕra, ho, ⟨_, hr, _, ha, hϕra⟩⟩
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddCommGroup τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : 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[inst_3] o
ho₃ : x ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
l₂ : (closure[inst_3] (image2 ϕ.toFun u s) ∩ o).Nonempty
ϕra : α
ho : ϕra ∈ o
w : τ
hr : w ∈ u
w_1 : α
ha : w_1 ∈ s
hϕra : ϕ.toFun w w_1 = ϕra
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

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

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
inst : TopologicalSpace τ
inst_1 : AddCommGroup τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : 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[inst_3] o
ho₃ : x ∈ o
t : τ
_ht₁ : t ∈ u
ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty
l₁ : (ω f ϕ.toFun s ∩ o).Nonempty
l₂ : (closure[inst_3] (image2 ϕ.toFun u s) ∩ o).Nonempty
ϕra : α
ho : ϕra ∈ o
w : τ
hr : w ∈ u
w_1 : α
ha : w_1 ∈ s
hϕra : ϕ.toFun w w_1 = ϕra
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty

Tactic:
exact ⟨_, hr, ϕra, ⟨_, ha, hϕra⟩, ho₁ ho⟩
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
hf : IsFixedPt f x
n : ℕ
⊢ IsPeriodicPt f n x

Tactic:
hf.iterate n

Premises used: Function.IsPeriodicPt, Function.IsFixedPt.iterate
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
n : ℕ
x : α
⊢ IsPeriodicPt id n x

Tactic:
(isFixedPt_id x).isPeriodicPt n

Premises used: Function.IsFixedPt.isPeriodicPt, Function.isFixedPt_id
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
⊢ IsPeriodicPt f 0 x

Tactic:
isFixedPt_id x

Premises used: Function.isFixedPt_id, Nat.iterate, Function.IsPeriodicPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
inst : Subsingleton α
f : α → α
n : ℕ
x : α
⊢ IsPeriodicPt f n x

Tactic:
IsFixedPt.of_subsingleton _ _

Premises used: Function.IsPeriodicPt, Function.IsFixedPt.of_subsingleton
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hf : IsPeriodicPt f n x
⊢ IsFixedPt f^[n] x

Tactic:
hf

Premises used: Function.IsPeriodicPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
x : α
n : ℕ
hx : IsPeriodicPt fa n x
g : α → β
hg : Semiconj g fa fb
⊢ IsPeriodicPt fb n (g x)

Tactic:
IsFixedPt.map hx (hg.iterate_right n)

Premises used: Function.IsPeriodicPt, Function.Semiconj.iterate_right, Function.IsFixedPt.map
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hx : IsPeriodicPt f n x
m : ℕ
⊢ IsPeriodicPt f n (f^[m] x)

Tactic:
hx.map <| Commute.iterate_self f m

Premises used: Function.Commute.iterate_self, Function.IsPeriodicPt.map
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hx : IsPeriodicPt f n x
⊢ IsPeriodicPt f n (f x)

Tactic:
hx.apply_iterate 1

Premises used: Nat.iterate, Function.IsPeriodicPt.apply_iterate, OfNat.ofNat
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
rw : IsFixedPt (f^[n] ∘ f^[m]) x
⊢ IsPeriodicPt f (n + m) x

Tactic:
rw [IsPeriodicPt, iterate_add]

Premises used: Function.iterate_add, Function.IsPeriodicPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsFixedPt (f^[n] ∘ f^[m]) x

Tactic:
hn.comp hm

Premises used: Function.IsFixedPt.comp
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsFixedPt (f^[n] ∘ f^[m]) x

Tactic:
exact hn.comp hm

Premises used: Function.IsFixedPt.comp
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f m x
⊢ IsFixedPt (f^[n] ∘ f^[m]) x

Tactic:
rw [IsPeriodicPt, iterate_add] at hn

Premises used: Function.iterate_add, Function.IsPeriodicPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f m x
hn₁ : IsFixedPt (f^[n] ∘ f^[m]) x
⊢ IsPeriodicPt f m x

Tactic:
rw [IsPeriodicPt, iterate_add] at hn

Premises used: Function.iterate_add, Function.IsPeriodicPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsFixedPt (f^[n] ∘ f^[m]) x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x

Tactic:
hn.left_of_comp hm

Premises used: Function.IsFixedPt.left_of_comp, Function.IsPeriodicPt
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsFixedPt (f^[n] ∘ f^[m]) x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x

Tactic:
exact hn.left_of_comp hm

Premises used: Function.IsFixedPt.left_of_comp
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m + n) x

Tactic:
rw [add_comm] at hn

Premises used: add_comm
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f n x
hn₁ : IsPeriodicPt f (m + n) x
⊢ IsPeriodicPt f n x

Tactic:
rw [add_comm] at hn

Premises used: add_comm
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (m + n) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x

Tactic:
hn.left_of_add hm

Premises used: Function.IsPeriodicPt.left_of_add
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (m + n) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x

Tactic:
exact hn.left_of_add hm

Premises used: Function.IsPeriodicPt.left_of_add
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
inl : ∀ (h : n ≤ m), IsPeriodicPt f (m - n) x
inr : ∀ (h : m ≤ n), IsPeriodicPt f (m - n) x
⊢ IsPeriodicPt f (m - n) x

Tactic:
rcases le_total n m with h | h

Premises used: le_total
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n) x

Tactic:
left_of_add ?_ hn

Premises used: Function.IsPeriodicPt.left_of_add
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
inl : IsPeriodicPt f (m - n + n) x
⊢ IsPeriodicPt f (m - n) x

Tactic:
refine left_of_add ?_ hn

Premises used: Function.IsPeriodicPt.left_of_add
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
inl inl₁ inl₂ inl₃ : IsPeriodicPt f m x
⊢ IsPeriodicPt f (m - n + n) x

Tactic:
rwa [tsub_add_cancel_of_le h]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
inr : IsPeriodicPt f 0 x
⊢ IsPeriodicPt f (m - n) x

Tactic:
rw [tsub_eq_zero_iff_le.mpr h]

Premises used: Iff.mpr, tsub_eq_zero_iff_le
-- Module: Mathlib.Dynamics.PeriodicPts.Defs
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f 0 x

Tactic:
apply isPeriodicPt_zero

Premises used: Function.isPeriodicPt_zero