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 α
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
u : Set τ
hu : u ∈ g
⊢ u ⊆ u

Tactic:
exact Subset.rfl

Premises used: Set.Subset.rfl
-- Module: Mathlib.Dynamics.OmegaLimit
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
u : Set τ
hu : u ∈ g
⊢ u ⊆ u

Tactic:
all_goals exact Subset.rfl

Premises used: Set.Subset.rfl
-- Module: Mathlib.Dynamics.OmegaLimit
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
⊢ k \ n ⊆ (closure[inst] (image2 ϕ w s))ᶜ

Tactic:
have hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ := by
    apply Subset.trans hg₃
    simp only [j, iUnion_subset_iff, compl_subset_compl]
    intro u hu
    unfold w
    gcongr
    refine iInter_subset_of_subset u (iInter_subset_of_subset hu ?_)
    all_goals exact Subset.rfl
-- Module: Mathlib.Dynamics.OmegaLimit
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))ᶜ
simp : closure[inst] (image2 ϕ w s) ⊆ k
⊢ kᶜ ⊆ (closure[inst] (image2 ϕ w s))ᶜ

Tactic:
simp only [compl_subset_compl]

Premises used: Set.compl_subset_compl
-- Module: Mathlib.Dynamics.OmegaLimit
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))ᶜ
⊢ closure[inst] (image2 ϕ w s) ⊆ k

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 α
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))ᶜ
⊢ closure[inst] (image2 ϕ w s) ⊆ k

Tactic:
exact 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 α
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))ᶜ
⊢ kᶜ ⊆ (closure[inst] (image2 ϕ w s))ᶜ

Tactic:
have hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ := by
    simp only [compl_subset_compl]
    exact closure_mono (image2_subset inter_subset_right Subset.rfl)
-- Module: Mathlib.Dynamics.OmegaLimit
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ᶜ
rw₃ rw₄ : k ∩ nᶜ ⊆ k ∩ nᶜ
⊢ nᶜ ⊆ k \ n ∪ kᶜ

Tactic:
rw [union_comm, ← inter_subset, diff_eq, inter_comm]

Premises used: Set.diff_eq, Set.union_comm, Set.inter_comm, Set.inter_subset
-- Module: Mathlib.Dynamics.OmegaLimit
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))ᶜ
⊢ nᶜ ⊆ k \ n ∪ kᶜ

Tactic:
have hnc : nᶜ ⊆ k \ n ∪ kᶜ := by rw [union_comm, ← inter_subset, diff_eq, inter_comm]
-- Module: Mathlib.Dynamics.OmegaLimit
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ᶜ
⊢ 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₄))
-- Module: Mathlib.Dynamics.OmegaLimit
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ᶜ
hw : closure[inst] (image2 ϕ w s) ⊆ n
⊢ ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n

Tactic:
⟨_, hw₂, hw⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Dynamics.OmegaLimit
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ᶜ
hw : closure[inst] (image2 ϕ w s) ⊆ n
⊢ ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n

Tactic:
exact ⟨_, hw₂, hw⟩
-- Module: Mathlib.Dynamics.OmegaLimit
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 ∈ f, closure[inst] (image2 ϕ u s) ⊆ n

Tactic:
eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset' f ϕ _ hc₁
    ⟨_, hc₂, closure_minimal (image2_subset_iff.2 fun _t ↦ id) hc₁.isClosed⟩ hn₁ hn₂

Premises used: Iff.mpr, closure_minimal, id, Set.image2_subset_iff, eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset', And.intro, Exists.intro, IsCompact.isClosed
-- Module: Mathlib.Dynamics.OmegaLimit
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
rcases : ∀ (u : Set τ) (hu_mem : u ∈ f) (hu : closure[inst] (image2 ϕ u s) ⊆ n), ∀ᶠ (t : τ) in f, MapsTo (ϕ t) 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⟩

Premises used: eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset
-- Module: Mathlib.Dynamics.OmegaLimit
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

Tactic:
mem_of_superset hu_mem fun t ht x hx ↦ ?_

Premises used: Filter.Eventually, Filter.mem_of_superset
-- Module: Mathlib.Dynamics.OmegaLimit
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
refine : ∀ (t : τ) (ht : t ∈ u) (x : α) (hx : x ∈ s), ϕ t x ∈ n
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s n

Tactic:
refine mem_of_superset hu_mem fun t ht x hx ↦ ?_
-- Module: Mathlib.Dynamics.OmegaLimit
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 : τ
ht : t ∈ u
x : α
hx : x ∈ s
⊢ ϕ t x ∈ n

Tactic:
hu (subset_closure <| mem_image2_of_mem ht hx)

Premises used: subset_closure, Set.mem_image2_of_mem
-- Module: Mathlib.Dynamics.OmegaLimit
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 : τ
ht : t ∈ u
x : α
hx : x ∈ s
⊢ ϕ t x ∈ n

Tactic:
exact hu (subset_closure <| mem_image2_of_mem ht hx)

Premises used: subset_closure, Set.mem_image2_of_mem
-- Module: Mathlib.Dynamics.OmegaLimit
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 ∈ f, closure[inst] (image2 ϕ u s) ⊆ v

Tactic:
eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset' _ _ _
    isCompact_univ ⟨univ, univ_mem, subset_univ _⟩ hv₁ hv₂

Premises used: Set.subset_univ, Set.univ, isCompact_univ, eventually_closure_subset_of_isCompact_absorbing_of_isOpen_of_omegaLimit_subset', And.intro, Exists.intro, Filter.univ_mem
-- Module: Mathlib.Dynamics.OmegaLimit
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
rcases : ∀ (u : Set τ) (hu_mem : u ∈ f) (hu : closure[inst] (image2 ϕ u s) ⊆ v), ∀ᶠ (t : τ) in f, MapsTo (ϕ t) 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⟩

Premises used: eventually_closure_subset_of_isOpen_of_omegaLimit_subset
-- Module: Mathlib.Dynamics.OmegaLimit
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

Tactic:
mem_of_superset hu_mem fun t ht x hx ↦ ?_

Premises used: Filter.Eventually, Filter.mem_of_superset
-- Module: Mathlib.Dynamics.OmegaLimit
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
refine : ∀ (t : τ) (ht : t ∈ u) (x : α) (hx : x ∈ s), ϕ t x ∈ v
⊢ ∀ᶠ (t : τ) in f, MapsTo (ϕ t) s v

Tactic:
refine mem_of_superset hu_mem fun t ht x hx ↦ ?_
-- Module: Mathlib.Dynamics.OmegaLimit
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 : τ
ht : t ∈ u
x : α
hx : x ∈ s
⊢ ϕ t x ∈ v

Tactic:
hu (subset_closure <| mem_image2_of_mem ht hx)

Premises used: subset_closure, Set.mem_image2_of_mem
-- Module: Mathlib.Dynamics.OmegaLimit
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 : τ
ht : t ∈ u
x : α
hx : x ∈ s
⊢ ϕ t x ∈ v

Tactic:
exact hu (subset_closure <| mem_image2_of_mem ht hx)

Premises used: subset_closure, Set.mem_image2_of_mem
-- 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
hc₂ : ∃ v ∈ f, closure[inst] (image2 ϕ v s) ⊆ c
hs : s.Nonempty
rcases : ∀ (v : Set τ) (hv₁ : v ∈ f) (hv₂ : closure[inst] (image2 ϕ v s) ⊆ c), (ω f ϕ s).Nonempty
⊢ (ω f ϕ s).Nonempty

Tactic:
rcases hc₂ with ⟨v, hv₁, 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
rw : Set.Nonempty.{u_3} (α := β) (⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s))
⊢ (ω f ϕ s).Nonempty

Tactic:
rw [omegaLimit_eq_iInter_inter _ _ _ hv₁]

Premises used: omegaLimit_eq_iInter_inter
-- 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
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))
htcl : ∀ (i : (↑f.sets : Type u_1)), IsClosed[inst] (closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s))
⊢ Set.Nonempty.{u_3} (α := β) (⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s))

Tactic:
apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed

Premises used: IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
-- 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₁ : 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₂) ⋯))
⊢ ∃ (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)

Tactic:
use ⟨u₁ ∩ u₂, inter_mem hu₁ hu₂⟩
-- 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₁ : 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₂) ⋯))
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₂) ⋯))

Tactic:
constructor
-- 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₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (↑(Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) (u₁ ∩ u₂) ⋯) : Set τ) ⊆
    (↑(Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) u₁ hu₁) : Set τ)

Tactic:
simp
-- 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₁ : 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₂) ⋯))

Tactic:
exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)

Premises used: Set.image2_subset, closure_mono, Set.inter_subset_inter_left, Set.Subset.rfl
-- 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₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ (↑(Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) (u₁ ∩ u₂) ⋯) : Set τ) ⊆
    (↑(Subtype.mk (p := fun (x : Set τ) ↦ x ∈ f.sets) u₂ hu₂) : Set τ)

Tactic:
simp
-- 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₁ : 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₂) ⋯))

Tactic:
exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)

Premises used: Set.image2_subset, closure_mono, Set.inter_subset_inter_left, Set.Subset.rfl