awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : (u : Set τ) → Set β := fun (u : Set τ) ↦ (closure[inst] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst] (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure[inst] (image2 ϕ w s))ᶜ
hw₄ : kᶜ ⊆ (closure[inst] (image2 ϕ w s))ᶜ
rw : nᶜ ⊆ kᶜ ∪ k \ n
rw₁ : nᶜ ∩ k ⊆ k \ n
rw₂ : nᶜ ∩ k ⊆ k ∩ nᶜ
⊢ nᶜ ⊆ k \ n ∪ kᶜ
have rw₃ : k ∩ nᶜ ⊆ k ∩ nᶜ
Tactic: rw [union_comm, ← inter_subset, diff_eq, inter_comm]
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (hypothesis)
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : (u : Set τ) → Set β := fun (u : Set τ) ↦ (closure[inst] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst] (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure[inst] (image2 ϕ w s))ᶜ
hw₄ : kᶜ ⊆ (closure[inst] (image2 ϕ w s))ᶜ
⊢ ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n
have hnc : nᶜ ⊆ k \ n ∪ kᶜ
Tactic: have hnc : nᶜ ⊆ k \ n ∪ kᶜ := by rw [union_comm, ← inter_subset, diff_eq, inter_comm]
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (hypothesis)
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : (u : Set τ) → Set β := fun (u : Set τ) ↦ (closure[inst] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst] (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure[inst] (image2 ϕ w s))ᶜ
hw₄ : kᶜ ⊆ (closure[inst] (image2 ϕ w s))ᶜ
hnc : nᶜ ⊆ k \ n ∪ kᶜ
⊢ ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n
have hw : closure[inst] (image2 ϕ w s) ⊆ n
Tactic: have hw : closure (image2 ϕ w s) ⊆ n :=
    compl_subset_compl.mp (Subset.trans hnc (union_subset hw₃ hw₄))
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst_1 : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen[inst] n
hn₂ : ω f ϕ s ⊆ n
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n
have rcases : ∀ (u : Set τ) (hu_mem : u ∈ f) (hu : closure[inst] (image2 ϕ u s) ⊆ n), ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n
Tactic: rcases eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset f ϕ s hc₁
      hc₂ hn₁ hn₂ with
    ⟨u, hu_mem, hu⟩
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst_1 : T2Space β
c : Set β
hc₁ : IsCompact c
hc₂ : ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s c
n : Set β
hn₁ : IsOpen[inst] n
hn₂ : ω f ϕ s ⊆ n
u : Set τ
hu_mem : u ∈ f
hu : closure[inst] (image2 ϕ u s) ⊆ n
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n
have refine : ∀ (t : τ) (ht : t ∈ u) (x : α) (hx : x ∈ s), ϕ t x ∈ n
Tactic: refine mem_of_superset hu_mem fun t ht x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst_1 : CompactSpace β
v : Set β
hv₁ : IsOpen[inst] v
hv₂ : ω f ϕ s ⊆ v
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v
have rcases : ∀ (u : Set τ) (hu_mem : u ∈ f) (hu : closure[inst] (image2 ϕ u s) ⊆ v), ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v
Tactic: rcases eventually_closure_subset_of_isOpen_of_omegaLimit_subset f ϕ s hv₁ hv₂ with ⟨u, hu_mem, hu⟩
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst_1 : CompactSpace β
v : Set β
hv₁ : IsOpen[inst] v
hv₂ : ω f ϕ s ⊆ v
u : Set τ
hu_mem : u ∈ f
hu : closure[inst] (image2 ϕ u s) ⊆ v
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v
have refine : ∀ (t : τ) (ht : t ∈ u) (x : α) (hx : x ∈ s), ϕ t x ∈ v
Tactic: refine mem_of_superset hu_mem fun t ht x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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
hc₂ : ∃ v ∈ f, closure[inst] (image2 ϕ v s) ⊆ c
hs : s.Nonempty
⊢ (ω f ϕ s).Nonempty
have rcases : ∀ (v : Set τ) (hv₁ : v ∈ f) (hv₂ : closure[inst] (image2 ϕ v s) ⊆ c), (ω f ϕ s).Nonempty
Tactic: rcases hc₂ with ⟨v, hv₁, hv₂⟩
Cleared hypotheses: hc₂
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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
⊢ (ω f ϕ s).Nonempty
have rw : Set.Nonempty.{u_3} (α := β) (⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s))
Tactic: rw [omegaLimit_eq_iInter_inter _ _ _ hv₁]
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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
⊢ Set.Nonempty.{u_3} (α := β) (⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s))
have htd : Directed (fun (x1 x2 : Set β) ↦ x1 ⊇ x2) fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s)
Tactic: apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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
htd :
  Directed (fun (x1 x2 : Set β) ↦ x1 ⊇ x2) fun (i : (↑f.sets : Type u_1)) ↦
    closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s)
⊢ Set.Nonempty.{u_3} (α := β) (⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s))
have htn : ∀ (i : (↑f.sets : Type u_1)), (closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s)).Nonempty
Tactic: apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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
htd :
  Directed (fun (x1 x2 : Set β) ↦ x1 ⊇ x2) fun (i : (↑f.sets : Type u_1)) ↦
    closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s)
htn : ∀ (i : (↑f.sets : Type u_1)), (closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s)).Nonempty
⊢ Set.Nonempty.{u_3} (α := β) (⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s))
have htc : ∀ (i : (↑f.sets : Type u_1)), IsCompact (closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
Tactic: apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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
htd :
  Directed (fun (x1 x2 : Set β) ↦ x1 ⊇ x2) fun (i : (↑f.sets : Type u_1)) ↦
    closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s)
htn : ∀ (i : (↑f.sets : Type u_1)), (closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s)).Nonempty
htc : ∀ (i : (↑f.sets : Type u_1)), IsCompact (closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
⊢ Set.Nonempty.{u_3} (α := β) (⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s))
have htcl : ∀ (i : (↑f.sets : Type u_1)), IsClosed[inst] (closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
Tactic: apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ ∃ (z : (↑f.sets : Type u_1)),
    (fun (x1 x2 : Set β) ↦ x1 ⊇ x2)
        ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
          (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) u₁ hu₁))
        ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s)) z) ∧
      (fun (x1 x2 : Set β) ↦ x1 ⊇ x2)
        ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
          (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) u₂ hu₂))
        ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s)) z)
have h : (fun (x1 x2 : Set β) ↦ x1 ⊇ x2)
    ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
      (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) u₁ hu₁))
    ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
      (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) (u₁ ∩ u₂) sorry)) ∧
  (fun (x1 x2 : Set β) ↦ x1 ⊇ x2)
    ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
      (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) u₂ hu₂))
    ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
      (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) (u₁ ∩ u₂) sorry))
Tactic: use ⟨u₁ ∩ u₂, inter_mem hu₁ hu₂⟩
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (fun (x1 x2 : Set β) ↦ x1 ⊇ x2)
      ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
        (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) u₁ hu₁))
      ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
        (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) (u₁ ∩ u₂) ⋯)) ∧
    (fun (x1 x2 : Set β) ↦ x1 ⊇ x2)
      ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
        (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) u₂ hu₂))
      ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
        (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) (u₁ ∩ u₂) ⋯))
have h : (fun (x1 x2 : Set β) ↦ x1 ⊇ x2)
  ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
    (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) u₁ hu₁))
  ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
    (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) (u₁ ∩ u₂) sorry))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
h :
  (fun (x1 x2 : Set β) ↦ x1 ⊇ x2)
    ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
      (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) u₁ hu₁))
    ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
      (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) (u₁ ∩ u₂) ⋯))
⊢ (fun (x1 x2 : Set β) ↦ x1 ⊇ x2)
      ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
        (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) u₁ hu₁))
      ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
        (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) (u₁ ∩ u₂) ⋯)) ∧
    (fun (x1 x2 : Set β) ↦ x1 ⊇ x2)
      ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
        (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) u₂ hu₂))
      ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
        (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) (u₁ ∩ u₂) ⋯))
have h₁ : (fun (x1 x2 : Set β) ↦ x1 ⊇ x2)
  ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
    (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) u₂ hu₂))
  ((fun (i : (↑f.sets : Type u_1)) ↦ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
    (Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) (u₁ ∩ u₂) sorry))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (hypothesis)
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)
⊢ (closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s)).Nonempty
have hn : (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
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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)
⊢ IsCompact (closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
have htc : closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s) ⊆ c
Tactic: apply hc₁.of_isClosed_subset isClosed_closure
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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)
have refine : ∀ (t : τ), MapsTo (ϕ.toFun t) (ω f ϕ.toFun s) (ω f (fun (t_1 : τ) (x : α) ↦ ϕ.toFun (t + t_1) x) s)
Tactic: refine fun t ↦ MapsTo.mono_right ?_ (omegaLimit_subset_of_tendsto ϕ s (hf t))
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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 ϕ.toFun (ϕ.toFun t '' s) ⊆ ω f ϕ.toFun s
have simp : ω f (fun (t_1 : τ) (x : α) ↦ ϕ.toFun (t_1 + t) x) s ⊆ ω f ϕ.toFun s
Tactic: simp only [omegaLimit_image_eq, ← map_add]
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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
⊢ ω f ϕ.toFun (ω f ϕ.toFun s) ⊆ ω f ϕ.toFun s
have 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
Tactic: simp only [subset_def, mem_omegaLimit_iff_frequently₂, frequently_iff]
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
have rcases : ∀ (o : Set α) (ho₁ : o ⊆ n) (ho₂ : IsOpen[inst_3] o) (ho₃ : x ∈ o), ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
Tactic: rcases mem_nhds_iff.mp hn with ⟨o, ho₁, ho₂, ho₃⟩
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
have rcases : ∀ (t : τ) (_ht₁ : t ∈ u) (ht₂ : (ϕ.toFun t '' ω f ϕ.toFun s ∩ o).Nonempty), ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
Tactic: rcases h o (IsOpen.mem_nhds ho₂ ho₃) hu with ⟨t, _ht₁, ht₂⟩
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (hypothesis)
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
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
have l₁ : (ω 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) _))
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (hypothesis)
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
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
have l₂ : (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⟩
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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
have rcases : ∀ (b : α) (hb₁ : b ∈ closure[inst_3] (image2 ϕ.toFun u s)) (hb₂ : b ∈ o), (o ∩ image2 ϕ.toFun u s).Nonempty
Tactic: rcases l₂ with ⟨b, hb₁, hb₂⟩
Cleared hypotheses: l₂
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (hypothesis)
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
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
have l₃ : (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₂)
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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
⊢ ∃ x ∈ u, (ϕ.toFun x '' s ∩ n).Nonempty
have 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
Tactic: rcases l₃ with ⟨ϕra, ho, ⟨_, hr, _, ha, hϕra⟩⟩
Cleared hypotheses: l₃
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f (n + m) x
have rw : IsFixedPt (f^[n] ∘ f^[m]) x
Tactic: rw [IsPeriodicPt, iterate_add]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (hypothesis)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x
have hn₁ : IsFixedPt (f^[n] ∘ f^[m]) x
Tactic: rw [IsPeriodicPt, iterate_add] at hn
Cleared hypotheses: hn, hm
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (hypothesis)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f n x
⊢ IsPeriodicPt f m x
have hn₁ : IsPeriodicPt f (m + n) x
Tactic: rw [add_comm] at hn
Cleared hypotheses: hn, hm
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m - n) x
have inl : ∀ (h : n ≤ m), IsPeriodicPt f (m - n) x
Tactic: rcases le_total n m with h | h
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
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
⊢ IsPeriodicPt f (m - n) x
have inr : ∀ (h : m ≤ n), IsPeriodicPt f (m - n) x
Tactic: rcases le_total n m with h | h
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
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
have inl : IsPeriodicPt f (m - n + n) x
Tactic: refine left_of_add ?_ hn
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f (m - n) x
have inr : IsPeriodicPt f 0 x
Tactic: rw [tsub_eq_zero_iff_le.mpr h]
-- Lean 4 proof step from Mathlib.Dynamics.PeriodicPts.Defs (goal)
Goal:
α : Type u_1
f : α → α
x : α
n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsPeriodicPt f^[m] n x
have rw : IsFixedPt f^[n]^[m] x
Tactic: rw [IsPeriodicPt, ← iterate_mul, mul_comm, iterate_mul]