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 τ
ϕ : τ → α → β
x : α
y : β
simp_rw : (∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, ({x} ∩ ϕ t ⁻¹' n).Nonempty) ↔ MapClusterPt y f fun (t : τ) ↦ ϕ t x
⊢ y ∈ ω f ϕ {x} ↔ MapClusterPt y f fun (t : τ) ↦ ϕ t x
have simp_rw₁ : (∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, ({x} ∩ ϕ t ⁻¹' n).Nonempty) ↔ ∀ s ∈ 𝓝 y, ∃ᶠ (a : τ) in f, ϕ a x ∈ s
Tactic: simp_rw [mem_omegaLimit_iff_frequently, mapClusterPt_iff_frequently, singleton_inter_nonempty,
    mem_preimage]
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
x : α
y : β
simp_rw : (∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, ({x} ∩ ϕ t ⁻¹' n).Nonempty) ↔ MapClusterPt y f fun (t : τ) ↦ ϕ t x
simp_rw₁ : (∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, ({x} ∩ ϕ t ⁻¹' n).Nonempty) ↔ ∀ s ∈ 𝓝 y, ∃ᶠ (a : τ) in f, ϕ a x ∈ s
⊢ y ∈ ω f ϕ {x} ↔ MapClusterPt y f fun (t : τ) ↦ ϕ t x
have simp_rw₂ : (∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, x ∈ ϕ t ⁻¹' n) ↔ ∀ s ∈ 𝓝 y, ∃ᶠ (a : τ) in f, ϕ a x ∈ s
Tactic: simp_rw [mem_omegaLimit_iff_frequently, mapClusterPt_iff_frequently, singleton_inter_nonempty,
    mem_preimage]
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
⊢ ω f ϕ (s₁ ∪ s₂) = ω f ϕ s₁ ∪ ω f ϕ s₂
have h : ∀ (y : β), y ∈ ω f ϕ (s₁ ∪ s₂) ↔ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂
Tactic: ext y
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) ↔ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂
have h : y ∈ ω f ϕ (s₁ ∪ s₂) → y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂
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₁ s₂ : Set α
y : β
h : y ∈ ω f ϕ (s₁ ∪ s₂) → y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) ↔ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂
have h₁ : y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂ → y ∈ ω f ϕ (s₁ ∪ s₂)
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₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) → y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂
have h : (∀ n ∈ 𝓝 y, (∃ᶠ (x : τ) in f, (s₁ ∩ ϕ x ⁻¹' n).Nonempty) ∨ ∃ᶠ (x : τ) in f, (s₂ ∩ ϕ x ⁻¹' n).Nonempty) →
  (∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (s₁ ∩ ϕ t ⁻¹' n).Nonempty) ∨ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (s₂ ∩ ϕ t ⁻¹' n).Nonempty
Tactic: simp only [mem_union, mem_omegaLimit_iff_frequently, union_inter_distrib_right, union_nonempty,
      frequently_or_distrib]
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ (∀ n ∈ 𝓝 y, (∃ᶠ (x : τ) in f, (s₁ ∩ ϕ x ⁻¹' n).Nonempty) ∨ ∃ᶠ (x : τ) in f, (s₂ ∩ ϕ x ⁻¹' n).Nonempty) →
    (∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (s₁ ∩ ϕ t ⁻¹' n).Nonempty) ∨ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (s₂ ∩ ϕ t ⁻¹' n).Nonempty
have h : ((∃ n ∈ 𝓝 y, ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n = ∅) ∧ ∃ n ∈ 𝓝 y, ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n = ∅) →
  ∃ n ∈ 𝓝 y, (∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n = ∅) ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n = ∅
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ ((∃ n ∈ 𝓝 y, ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n = ∅) ∧ ∃ n ∈ 𝓝 y, ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n = ∅) →
    ∃ n ∈ 𝓝 y, (∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n = ∅) ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n = ∅
have h : ((∃ n ∈ 𝓝 y, ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n ⊆ ∅) ∧ ∃ n ∈ 𝓝 y, ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n ⊆ ∅) →
  ∃ n ∈ 𝓝 y, (∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n ⊆ ∅) ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n ⊆ ∅
Tactic: simp only [← subset_empty_iff]
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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 ⊆ ∅
have h : ∀ (t : τ), s₁ ∩ ϕ t ⁻¹' n₁ ⊆ ∅ → s₁ ∩ ϕ t ⁻¹' (n₁ ∩ n₂) ⊆ ∅
Tactic: refine ⟨n₁ ∩ n₂, inter_mem hn₁ hn₂, h₁.mono fun t ↦ ?_, h₂.mono fun t ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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₂) ⊆ ∅
⊢ ∃ n ∈ 𝓝 y, (∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n ⊆ ∅) ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n ⊆ ∅
have h₃ : ∀ (t : τ), s₂ ∩ ϕ t ⁻¹' n₂ ⊆ ∅ → s₂ ∩ ϕ t ⁻¹' (n₁ ∩ n₂) ⊆ ∅
Tactic: refine ⟨n₁ ∩ n₂, inter_mem hn₁ hn₂, h₁.mono fun t ↦ ?_, h₂.mono fun t ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.OmegaLimit (goal)
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)
have rw : ∀ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ (i : ι), p i)
Tactic: rw [iUnion_subset_iff]
-- 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 α
v : Set τ
hv : v ∈ f
⊢ ω f ϕ s = ⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑u : Set τ) ∩ v) s)
have 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))
Tactic: rw [omegaLimit_eq_biInter_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 α
u : Set τ
hu : u ∈ f
⊢ ω f ϕ s ⊆ closure[inst] (image2 ϕ u s)
have rw : ⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ (↑u : Set τ) s) ⊆ closure[inst] (image2 ϕ u s)
Tactic: rw [omegaLimit_eq_iInter]
-- 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 α
u : Set τ
hu : u ∈ f
a : β
hx : Membership.mem (γ := Set β) (⋂ (u : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ (↑u : Set τ) s)) a
⊢ a ∈ closure[inst] (image2 ϕ u s)
have hx₁ : ∀ (i : (↑f.sets : Type u_1)), a ∈ closure[inst] (image2 ϕ (↑i : Set τ) s)
Tactic: rw [mem_iInter] at hx
Cleared hypotheses: 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 α
c : Set β
hc₁ : IsCompact c
hc₂ : ∃ v ∈ f, closure[inst] (image2 ϕ v s) ⊆ c
n : Set β
hn₁ : IsOpen[inst] n
hn₂ : ω f ϕ s ⊆ n
⊢ ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n
have rcases : ∀ (v : Set τ) (hv₁ : v ∈ f) (hv₂ : closure[inst] (image2 ϕ v s) ⊆ c), ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n
Tactic: rcases hc₂ with ⟨v, hv₁, hv₂⟩
Cleared hypotheses: hc₂
-- 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)
⊢ ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n
have hk : IsCompact (k \ n)
Tactic: have hk : IsCompact (k \ n) :=
    (hc₁.of_isClosed_subset isClosed_closure hv₂).diff hn₁
-- 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))ᶜ
⊢ ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n
have hj₁ : ∀ u ∈ f, IsOpen[inst] (j u)
Tactic: have hj₁ : ∀ u ∈ f, IsOpen (j u) := fun _ _ ↦ isOpen_compl_iff.mpr isClosed_closure
-- 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)
⊢ k \ n ⊆ ⋃ u ∈ f, j u
have this : 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 _ _
-- 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)
this : Eq.{u_3 + 1} (α := Set β) (⋃ u ∈ f, j u) (⋃ (u : (↑f.sets : Type u_1)), j (↑u : Set τ))
⊢ k \ n ⊆ ⋃ u ∈ f, j u
have rw : ⋂ (i : (↑f.sets : Type u_1)), k \ j (↑i : Set τ) ⊆ n
Tactic: rw [this, diff_subset_comm, diff_iUnion]
-- 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)
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
have 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
Tactic: rw [omegaLimit_eq_iInter_inter _ _ _ hv₁] at hn₂
Cleared hypotheses: hn₂, hv₁, hv₂, k, hk, j, hj₁, this
-- 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
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 τ))
⊢ ⋂ (i : (↑f.sets : Type u_1)), k \ j (↑i : Set τ) ⊆ n
have simp_rw : ⋂ (i : (↑f.sets : Type u_1)), k ∩ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s) ⊆ n
Tactic: simp_rw [j, diff_compl]
-- 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
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 τ))
⊢ ⋂ (i : (↑f.sets : Type u_1)), k ∩ closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s) ⊆ n
have rw : k ∩ ⋂ (i : (↑f.sets : Type u_1)), closure[inst] (image2 ϕ ((↑i : Set τ) ∩ v) s) ⊆ n
Tactic: rw [← inter_iInter]
-- 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)
⊢ ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n
have hj₂ : 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₂
-- 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
⊢ ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n
have 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
Tactic: rcases hk.elim_finite_subcover_image hj₁ hj₂ with ⟨g, hg₁ : ∀ u ∈ g, u ∈ f, hg₂, hg₃⟩
-- 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
⊢ ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n
have hw₂ : w ∈ f
Tactic: have hw₂ : w ∈ f := by simpa [w, *]
-- 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
⊢ k \ n ⊆ (closure[inst] (image2 ϕ w s))ᶜ
have apply : ⋃ i ∈ g, j i ⊆ (closure[inst] (image2 ϕ w s))ᶜ
Tactic: apply Subset.trans hg₃
-- 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
⊢ ⋃ i ∈ g, j i ⊆ (closure[inst] (image2 ϕ w s))ᶜ
have simp : ∀ (i : Set τ) (i_1 : i ∈ g), closure[inst] (image2 ϕ w s) ⊆ closure[inst] (image2 ϕ (i ∩ v) s)
Tactic: simp only [j, iUnion_subset_iff, compl_subset_compl]
-- 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
u : Set τ
hu : u ∈ g
⊢ closure[inst] (image2 ϕ ((⋂ u ∈ g, u) ∩ v) s) ⊆ closure[inst] (image2 ϕ (u ∩ v) s)
have h : ⋂ u ∈ g, u ⊆ u
Tactic: gcongr
-- 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
u : Set τ
hu : u ∈ g
⊢ ⋂ u ∈ g, u ⊆ u
have h : u ⊆ u
Tactic: refine iInter_subset_of_subset u (iInter_subset_of_subset hu ?_)
-- 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
⊢ ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n
have hw₃ : 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
-- 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))ᶜ
⊢ kᶜ ⊆ (closure[inst] (image2 ϕ w s))ᶜ
have simp : closure[inst] (image2 ϕ w s) ⊆ k
Tactic: simp only [compl_subset_compl]
-- 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))ᶜ
⊢ ∃ u ∈ f, closure[inst] (image2 ϕ u s) ⊆ n
have hw₄ : 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)
-- 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))ᶜ
⊢ nᶜ ⊆ k \ n ∪ kᶜ
have rw : nᶜ ⊆ kᶜ ∪ k \ n
Tactic: rw [union_comm, ← inter_subset, diff_eq, inter_comm]
-- 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
⊢ nᶜ ⊆ k \ n ∪ kᶜ
have rw₁ : nᶜ ∩ k ⊆ k \ n
Tactic: rw [union_comm, ← inter_subset, diff_eq, inter_comm]
-- 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
⊢ nᶜ ⊆ k \ n ∪ kᶜ
have rw₂ : nᶜ ∩ k ⊆ k ∩ nᶜ
Tactic: rw [union_comm, ← inter_subset, diff_eq, inter_comm]