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₁ s₂ : Set α
y : β
n₁ : Set β
hn₁ : n₁ ∈ 𝓝 y
h₁ : ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n₁ ⊆ ∅
n₂ : Set β
hn₂ : n₂ ∈ 𝓝 y
h₂ : ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n₂ ⊆ ∅
⊢ ∃ n ∈ 𝓝 y, (∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n ⊆ ∅) ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n ⊆ ∅

Tactic:
⟨n₁ ∩ n₂, inter_mem hn₁ hn₂, h₁.mono fun t ↦ ?_, h₂.mono fun t ↦ ?_⟩

Premises used: Filter.inter_mem, Inter.inter, Filter.Eventually.mono, And.intro, Exists.intro
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
n₁ : Set β
hn₁ : n₁ ∈ 𝓝 y
h₁ : ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n₁ ⊆ ∅
n₂ : Set β
hn₂ : n₂ ∈ 𝓝 y
h₂ : ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n₂ ⊆ ∅
h : ∀ (t : τ), s₁ ∩ ϕ t ⁻¹' n₁ ⊆ ∅ → s₁ ∩ ϕ t ⁻¹' (n₁ ∩ n₂) ⊆ ∅
h₃ : ∀ (t : τ), s₂ ∩ ϕ t ⁻¹' n₂ ⊆ ∅ → s₂ ∩ ϕ t ⁻¹' (n₁ ∩ n₂) ⊆ ∅
⊢ ∃ n ∈ 𝓝 y, (∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n ⊆ ∅) ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n ⊆ ∅

Tactic:
refine ⟨n₁ ∩ n₂, inter_mem hn₁ hn₂, h₁.mono fun t ↦ ?_, h₂.mono fun t ↦ ?_⟩
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
n₁ : Set β
hn₁ : n₁ ∈ 𝓝 y
h₁ : ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n₁ ⊆ ∅
n₂ : Set β
hn₂ : n₂ ∈ 𝓝 y
h₂ : ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n₂ ⊆ ∅
t : τ
⊢ s₁ ∩ ϕ t ⁻¹' n₁ ⊆ ∅ → s₁ ∩ ϕ t ⁻¹' (n₁ ∩ n₂) ⊆ ∅

Tactic:
Subset.trans <| inter_subset_inter_right _ <| preimage_mono inter_subset_left

Premises used: Set.inter_subset_inter_right, Set.Subset.trans, Set.inter_subset_left, Set.preimage_mono
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
n₁ : Set β
hn₁ : n₁ ∈ 𝓝 y
h₁ : ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n₁ ⊆ ∅
n₂ : Set β
hn₂ : n₂ ∈ 𝓝 y
h₂ : ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n₂ ⊆ ∅
t : τ
⊢ s₂ ∩ ϕ t ⁻¹' n₂ ⊆ ∅ → s₂ ∩ ϕ t ⁻¹' (n₁ ∩ n₂) ⊆ ∅

Tactic:
Subset.trans <| inter_subset_inter_right _ <| preimage_mono inter_subset_right

Premises used: Set.inter_subset_inter_right, Set.Subset.trans, Set.preimage_mono, Set.inter_subset_right
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
n₁ : Set β
hn₁ : n₁ ∈ 𝓝 y
h₁ : ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n₁ ⊆ ∅
n₂ : Set β
hn₂ : n₂ ∈ 𝓝 y
h₂ : ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n₂ ⊆ ∅
t : τ
⊢ s₁ ∩ ϕ t ⁻¹' n₁ ⊆ ∅ → s₁ ∩ ϕ t ⁻¹' (n₁ ∩ n₂) ⊆ ∅

Tactic:
exacts [Subset.trans <| inter_subset_inter_right _ <| preimage_mono inter_subset_left,
      Subset.trans <| inter_subset_inter_right _ <| preimage_mono inter_subset_right]

Premises used: Set.inter_subset_inter_right, Set.Subset.trans, Set.inter_subset_left, Set.preimage_mono, Set.inter_subset_right
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
hy : y ∈ ω f ϕ s₁
⊢ y ∈ ω f ϕ (s₁ ∪ s₂)

Tactic:
omegaLimit_mono_right _ _ subset_union_left hy

Premises used: omegaLimit_mono_right, Set.subset_union_left
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
hy : y ∈ ω f ϕ s₂
⊢ y ∈ ω f ϕ (s₁ ∪ s₂)

Tactic:
omegaLimit_mono_right _ _ subset_union_right hy

Premises used: Set.subset_union_right, omegaLimit_mono_right
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
hy : y ∈ ω f ϕ s₁
⊢ y ∈ ω f ϕ (s₁ ∪ s₂)

Tactic:
exacts [omegaLimit_mono_right _ _ subset_union_left hy,
      omegaLimit_mono_right _ _ subset_union_right hy]

Premises used: Set.subset_union_right, omegaLimit_mono_right, Set.subset_union_left
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
p : ι → Set α
rw : ∀ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ (i : ι), p i)
⊢ ⋃ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ (i : ι), p i)

Tactic:
rw [iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
p : ι → Set α
⊢ ∀ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ (i : ι), p i)

Tactic:
fun i ↦ omegaLimit_mono_right _ _ (subset_iUnion _ _)

Premises used: omegaLimit_mono_right, Set.subset_iUnion
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
p : ι → Set α
⊢ ∀ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ (i : ι), p i)

Tactic:
exact fun i ↦ omegaLimit_mono_right _ _ (subset_iUnion _ _)

Premises used: omegaLimit_mono_right, Set.subset_iUnion
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
⊢ ω f ϕ s = ⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ (↑u : Set τ) s)

Tactic:
biInter_eq_iInter _ _

Premises used: omegaLimit, Set.biInter_eq_iInter
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
v : Set τ
hv : v ∈ f
⊢ ω f ϕ s = ⋂ u ∈ f, closure[inst] (image2 ϕ (u ∩ v) s)

Tactic:
Subset.antisymm (iInter₂_mono' fun u hu ↦ ⟨u ∩ v, inter_mem hu hv, Subset.rfl⟩)
    (iInter₂_mono fun _u _hu ↦ closure_mono <| image2_subset inter_subset_left Subset.rfl)

Premises used: Set.Subset.antisymm, Set.iInter₂_mono', Set.image2_subset, Set.iInter₂_mono, Filter.inter_mem, Set.inter_subset_left, closure_mono, Inter.inter, Set.Subset.rfl, Exists.intro
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
v : Set τ
hv : v ∈ f
rw :
  Eq.{u_3 + 1} (α := Set β) (⋂ u ∈ f, closure[inst] (image2 ϕ (u ∩ v) s))
    (⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s))
⊢ ω f ϕ s = ⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s)

Tactic:
rw [omegaLimit_eq_biInter_inter _ _ _ hv]

Premises used: omegaLimit_eq_biInter_inter
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
v : Set τ
hv : v ∈ f
⊢ Eq.{u_3 + 1} (α := Set β) (⋂ u ∈ f, closure[inst] (image2 ϕ (u ∩ v) s))
    (⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s))

Tactic:
apply biInter_eq_iInter

Premises used: Set.biInter_eq_iInter
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
rw : ⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ (↑u : Set τ) s) ⊆ closure[inst] (image2 ϕ u s)
⊢ ω f ϕ s ⊆ closure[inst] (image2 ϕ u s)

Tactic:
rw [omegaLimit_eq_iInter]

Premises used: omegaLimit_eq_iInter
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
a : β
hx : Membership.mem (γ := Set β) (⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ (↑u : Set τ) s)) a
⊢ ∀ (i : (↑f.sets : Type u_1)), a ∈ closure[inst] (image2 ϕ (↑i : Set τ) s)

Tactic:
rw [mem_iInter] at hx

Premises used: Set.mem_iInter
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
a : β
hx : ∀ (i : (↑f.sets : Type u_1)), a ∈ closure[inst] (image2 ϕ (↑i : Set τ) s)
⊢ a ∈ closure[inst] (image2 ϕ u s)

Tactic:
hx ⟨u, hu⟩

Premises used: Set.Mem, Subtype.mk
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
a : β
hx : ∀ (i : (↑f.sets : Type u_1)), a ∈ closure[inst] (image2 ϕ (↑i : Set τ) s)
⊢ a ∈ closure[inst] (image2 ϕ u s)

Tactic:
exact hx ⟨u, hu⟩

Premises used: Subtype.mk
-- 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
hc₂ : ∃ v ∈ f, closure[inst] (image2 ϕ v s) ⊆ c
n : Set β
hn₁ : IsOpen[inst] n
hn₂ : ω f ϕ s ⊆ n
rcases : ∀ (v : Set τ) (hv₁ : v ∈ f) (hv₂ : closure[inst] (image2 ϕ v s) ⊆ c), ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n
⊢ ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n

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 α
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)
⊢ IsCompact (k \ n)

Tactic:
have hk : IsCompact (k \ n) :=
    (hc₁.of_isClosed_subset isClosed_closure hv₂).diff hn₁
-- 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))ᶜ
⊢ ∀ u ∈ f, IsOpen[inst] (j u)

Tactic:
have hj₁ : ∀ u ∈ f, IsOpen (j u) := fun _ _ ↦ isOpen_compl_iff.mpr isClosed_closure
-- 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)
⊢ Eq.{u_3 + 1} (α := Set β) (⋃ u ∈ f, j u) (⋃ (u : (↑f.sets : Type u_1)), j (↑u : Set τ))

Tactic:
have : ⋃ u ∈ f, j u = ⋃ u : (↥f.sets), j u := biUnion_eq_iUnion _ _
-- 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)
this : Eq.{u_3 + 1} (α := Set β) (⋃ u ∈ f, j u) (⋃ (u : (↑f.sets : Type u_1)), j (↑u : Set τ))
rw : ⋂ (i : (↑f.sets : Type u_1)), k \ j (↑i : Set τ) ⊆ n
⊢ k \ n ⊆ ⋃ u ∈ f, j u

Tactic:
rw [this, diff_subset_comm, diff_iUnion]

Premises used: Set.diff_subset_comm, Set.diff_iUnion
-- 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)
this : Eq.{u_3 + 1} (α := Set β) (⋃ u ∈ f, j u) (⋃ (u : (↑f.sets : Type u_1)), j (↑u : Set τ))
rw :
  ∀ (hn₂ : ⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s) ⊆ n) (hv₁ : v ∈ f)
    (hv₂ : closure[inst] (image2 ϕ v s) ⊆ c),
    let k := closure[inst] (image2 ϕ v s);
    ∀ (hk : IsCompact (k \ n)),
      let j : (u : Set τ) → Set β := fun (u : Set τ) ↦ (closure[inst] (image2 ϕ (u ∩ v) s))ᶜ;
      ∀ (hj₁ : ∀ u ∈ f, IsOpen[inst] (j u))
        (this : Eq.{u_3 + 1} (α := Set β) (⋃ u ∈ f, j u) (⋃ (u : (↑f.sets : Type u_1)), j (↑u : Set τ))),
        ⋂ (i : (↑f.sets : Type u_1)), k \ j (↑i : Set τ) ⊆ n
⊢ ⋂ (i : (↑f.sets : Type u_1)), k \ j (↑i : Set τ) ⊆ n

Tactic:
rw [omegaLimit_eq_iInter_inter _ _ _ hv₁] at hn₂

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 α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst] n
v : Set τ
hn₂ : ⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s) ⊆ n
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)
this : Eq.{u_3 + 1} (α := Set β) (⋃ u ∈ f, j u) (⋃ (u : (↑f.sets : Type u_1)), j (↑u : Set τ))
simp_rw : ⋂ (i : (↑f.sets : Type u_1)), k ∩ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s) ⊆ n
⊢ ⋂ (i : (↑f.sets : Type u_1)), k \ j (↑i : Set τ) ⊆ n

Tactic:
simp_rw [j, diff_compl]

Premises used: Set.diff_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
v : Set τ
hn₂ : ⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s) ⊆ n
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)
this : Eq.{u_3 + 1} (α := Set β) (⋃ u ∈ f, j u) (⋃ (u : (↑f.sets : Type u_1)), j (↑u : Set τ))
rw : k ∩ ⋂ (i : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s) ⊆ n
⊢ ⋂ (i : (↑f.sets : Type u_1)), k ∩ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s) ⊆ n

Tactic:
rw [← inter_iInter]

Premises used: Set.inter_iInter
-- 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
v : Set τ
hn₂ : ⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s) ⊆ n
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)
this : Eq.{u_3 + 1} (α := Set β) (⋃ u ∈ f, j u) (⋃ (u : (↑f.sets : Type u_1)), j (↑u : Set τ))
⊢ k ∩ ⋂ (i : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s) ⊆ n

Tactic:
Subset.trans inter_subset_right hn₂

Premises used: Set.Subset.trans, 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
v : Set τ
hn₂ : ⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s) ⊆ n
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)
this : Eq.{u_3 + 1} (α := Set β) (⋃ u ∈ f, j u) (⋃ (u : (↑f.sets : Type u_1)), j (↑u : Set τ))
⊢ k ∩ ⋂ (i : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s) ⊆ n

Tactic:
exact Subset.trans inter_subset_right hn₂

Premises used: Set.Subset.trans, 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)
⊢ k \ n ⊆ ⋃ u ∈ f, j u

Tactic:
have hj₂ : k \ n ⊆ ⋃ u ∈ f, j u := by
    have : ⋃ u ∈ f, j u = ⋃ u : (↥f.sets), j u := biUnion_eq_iUnion _ _
    rw [this, diff_subset_comm, diff_iUnion]
    rw [omegaLimit_eq_iInter_inter _ _ _ hv₁] at hn₂
    simp_rw [j, diff_compl]
    rw [← inter_iInter]
    exact Subset.trans inter_subset_right hn₂
-- 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
rcases :
  ∀ (g : Set (Set τ)) (hg₁ : ∀ u ∈ g, u ∈ f) (hg₂ : g.Finite) (hg₃ : k \ n ⊆ ⋃ i ∈ g, j i),
    ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n
⊢ ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n

Tactic:
rcases hk.elim_finite_subcover_image hj₁ hj₂ with ⟨g, hg₁ : ∀ u ∈ g, u ∈ f, hg₂, hg₃⟩

Premises used: IsCompact.elim_finite_subcover_image
-- 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
⊢ w ∈ f

Tactic:
simpa [w, *]
-- 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
⊢ w ∈ f

Tactic:
have hw₂ : w ∈ f := by simpa [w, *]
-- 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
apply : ⋃ i ∈ g, j i ⊆ (closure[inst] (image2 ϕ w s))ᶜ
⊢ k \ n ⊆ (closure[inst] (image2 ϕ w s))ᶜ

Tactic:
apply Subset.trans hg₃

Premises used: Set.Subset.trans
-- 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
simp : ∀ (i : Set τ) (i_1 : i ∈ g), closure[inst] (image2 ϕ w s) ⊆ closure[inst] (image2 ϕ (i ∩ v) s)
⊢ ⋃ i ∈ g, j i ⊆ (closure[inst] (image2 ϕ w s))ᶜ

Tactic:
simp only [j, iUnion_subset_iff, compl_subset_compl]

Premises used: Set.iUnion_subset_iff, 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
u : Set τ
hu : u ∈ g
unfold : closure[inst] (image2 ϕ ((⋂ u ∈ g, u) ∩ v) s) ⊆ closure[inst] (image2 ϕ (u ∩ v) s)
⊢ closure[inst] (image2 ϕ w s) ⊆ closure[inst] (image2 ϕ (u ∩ v) s)

Tactic:
unfold w
-- 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
h : ⋂ u ∈ g, u ⊆ u
⊢ closure[inst] (image2 ϕ ((⋂ u ∈ g, u) ∩ v) s) ⊆ closure[inst] (image2 ϕ (u ∩ v) s)

Tactic:
gcongr
-- 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 ∈ g, u ⊆ u

Tactic:
iInter_subset_of_subset u (iInter_subset_of_subset hu ?_)

Premises used: Set.iInter_subset_of_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
u : Set τ
hu : u ∈ g
h : u ⊆ u
⊢ ⋂ u ∈ g, u ⊆ u

Tactic:
refine iInter_subset_of_subset u (iInter_subset_of_subset hu ?_)

Premises used: Set.iInter_subset_of_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
u : Set τ
hu : u ∈ g
⊢ u ⊆ u

Tactic:
Subset.rfl

Premises used: Set.Subset.rfl