awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Newton
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
r₁ r₂ : S
h_1 : IsNilpotent (r₁ - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r₁ : (a : R[X]) → S) P : S) (0 : S)
h_2 : IsNilpotent (r₂ - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r₂ : (a : R[X]) → S) P : S) (0 : S)
hr₁ : IsNilpotent (r₁ - x)
hr₁' : Eq.{u_2 + 1} (α := S) ((aeval r₁ : (a : R[X]) → S) P : S) (0 : S)
hr₂ : IsNilpotent (r₂ - x)
hr₂' : Eq.{u_2 + 1} (α := S) ((aeval r₂ : (a : R[X]) → S) P : S) (0 : S)
u : S
hu :
  eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
    eval r₁ (map (algebraMap R S) P) + eval r₁ ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) * (r₂ - r₁) +
      u * HPow.hPow (β := ℕ) (r₂ - r₁) 2
this : IsUnit.{u_2} (M := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
⊢ IsUnit
    (HAdd.hAdd (α := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
      (u * (r₂ - x - (r₁ - x))))

Tactic:
IsNilpotent.isUnit_add_left_of_commute ?_ this (Commute.all _ _)

Premises used: IsNilpotent.isUnit_add_left_of_commute, Commute.all
-- Module: Mathlib.Dynamics.Newton
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
r₁ r₂ : S
h_1 : IsNilpotent (r₁ - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r₁ : (a : R[X]) → S) P : S) (0 : S)
h_2 : IsNilpotent (r₂ - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r₂ : (a : R[X]) → S) P : S) (0 : S)
hr₁ : IsNilpotent (r₁ - x)
hr₁' : Eq.{u_2 + 1} (α := S) ((aeval r₁ : (a : R[X]) → S) P : S) (0 : S)
hr₂ : IsNilpotent (r₂ - x)
hr₂' : Eq.{u_2 + 1} (α := S) ((aeval r₂ : (a : R[X]) → S) P : S) (0 : S)
u : S
hu :
  eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
    eval r₁ (map (algebraMap R S) P) + eval r₁ ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) * (r₂ - r₁) +
      u * HPow.hPow (β := ℕ) (r₂ - r₁) 2
this : IsUnit.{u_2} (M := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
refine_2 : IsNilpotent (u * (r₂ - x - (r₁ - x)))
⊢ IsUnit
    (HAdd.hAdd (α := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
      (u * (r₂ - x - (r₁ - x))))

Tactic:
refine IsNilpotent.isUnit_add_left_of_commute ?_ this (Commute.all _ _)

Premises used: IsNilpotent.isUnit_add_left_of_commute, Commute.all
-- Module: Mathlib.Dynamics.Newton
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
r₁ r₂ : S
h_1 : IsNilpotent (r₁ - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r₁ : (a : R[X]) → S) P : S) (0 : S)
h_2 : IsNilpotent (r₂ - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r₂ : (a : R[X]) → S) P : S) (0 : S)
hr₁ : IsNilpotent (r₁ - x)
hr₁' : Eq.{u_2 + 1} (α := S) ((aeval r₁ : (a : R[X]) → S) P : S) (0 : S)
hr₂ : IsNilpotent (r₂ - x)
hr₂' : Eq.{u_2 + 1} (α := S) ((aeval r₂ : (a : R[X]) → S) P : S) (0 : S)
u : S
hu :
  eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
    eval r₁ (map (algebraMap R S) P) + eval r₁ ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) * (r₂ - r₁) +
      u * HPow.hPow (β := ℕ) (r₂ - r₁) 2
this : IsUnit.{u_2} (M := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
⊢ IsNilpotent (u * (r₂ - x - (r₁ - x)))

Tactic:
(Commute.all _ _).isNilpotent_mul_left <| (Commute.all _ _).isNilpotent_sub hr₂ hr₁

Premises used: Commute.isNilpotent_mul_left, Commute.isNilpotent_sub
-- Module: Mathlib.Dynamics.Newton
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
r₁ r₂ : S
h_1 : IsNilpotent (r₁ - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r₁ : (a : R[X]) → S) P : S) (0 : S)
h_2 : IsNilpotent (r₂ - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r₂ : (a : R[X]) → S) P : S) (0 : S)
hr₁ : IsNilpotent (r₁ - x)
hr₁' : Eq.{u_2 + 1} (α := S) ((aeval r₁ : (a : R[X]) → S) P : S) (0 : S)
hr₂ : IsNilpotent (r₂ - x)
hr₂' : Eq.{u_2 + 1} (α := S) ((aeval r₂ : (a : R[X]) → S) P : S) (0 : S)
u : S
hu :
  eval (r₁ + (r₂ - r₁)) (map (algebraMap R S) P) =
    eval r₁ (map (algebraMap R S) P) + eval r₁ ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) * (r₂ - r₁) +
      u * HPow.hPow (β := ℕ) (r₂ - r₁) 2
this : IsUnit.{u_2} (M := S) ((aeval r₁ : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
⊢ IsNilpotent (u * (r₂ - x - (r₁ - x)))

Tactic:
exact (Commute.all _ _).isNilpotent_mul_left <| (Commute.all _ _).isNilpotent_sub hr₂ hr₁

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

Tactic:
rfl

Premises used: omegaLimit, rfl
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
ϕ : τ → α → β
s : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
⊢ ω f₁ (fun (t : τ) (x : α) ↦ ϕ (m t) x) s ⊆ ω f₂ ϕ s

Tactic:
iInter₂_mono' fun u hu ↦ ⟨m ⁻¹' u, tendsto_def.mp hf _ hu, ?_⟩

Premises used: omegaLimit, Set.iInter₂_mono', Filter.tendsto_def, Set.preimage, Exists.intro, Iff.mp
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
ϕ : τ → α → β
s : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
refine :
  ∀ (u : Set τ) (hu : u ∈ f₂),
    closure[inst] (image2 (fun (t : τ) (x : α) ↦ ϕ (m t) x) (m ⁻¹' u) s) ⊆ closure[inst] (image2 ϕ u s)
⊢ ω f₁ (fun (t : τ) (x : α) ↦ ϕ (m t) x) s ⊆ ω f₂ ϕ s

Tactic:
refine iInter₂_mono' fun u hu ↦ ⟨m ⁻¹' u, tendsto_def.mp hf _ hu, ?_⟩

Premises used: Set.iInter₂_mono', Filter.tendsto_def, Set.preimage, Exists.intro, Iff.mp
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
ϕ : τ → α → β
s : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
rw : closure[inst] (image2 ϕ (m '' m ⁻¹' u) s) ⊆ closure[inst] (image2 ϕ u s)
⊢ closure[inst] (image2 (fun (t : τ) (x : α) ↦ ϕ (m t) x) (m ⁻¹' u) s) ⊆ closure[inst] (image2 ϕ u s)

Tactic:
rw [← image2_image_left]

Premises used: Set.image2_image_left
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
ϕ : τ → α → β
s : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure[inst] (image2 ϕ (m '' m ⁻¹' u) s) ⊆ closure[inst] (image2 ϕ u s)

Tactic:
closure_mono (image2_subset (image_preimage_subset _ _) Subset.rfl)

Premises used: Set.image2_subset, closure_mono, Set.Subset.rfl, Set.image_preimage_subset
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
ϕ : τ → α → β
s : Set α
m : τ → τ
f₁ f₂ : Filter τ
hf : Tendsto m f₁ f₂
u : Set τ
hu : u ∈ f₂
⊢ closure[inst] (image2 ϕ (m '' m ⁻¹' u) s) ⊆ closure[inst] (image2 ϕ u s)

Tactic:
exact closure_mono (image2_subset (image_preimage_subset _ _) Subset.rfl)

Premises used: Set.image2_subset, closure_mono, Set.Subset.rfl, Set.image_preimage_subset
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
ϕ : τ → α → β
s : Set α
f₁ f₂ : Filter τ
hf : f₁ ≤ f₂
⊢ ω f₁ ϕ s ⊆ ω f₂ ϕ s

Tactic:
omegaLimit_subset_of_tendsto ϕ s (tendsto_id'.2 hf)

Premises used: Iff.mpr, Filter.tendsto_id', omegaLimit_subset_of_tendsto
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
hs : s₁ ⊆ s₂
⊢ ω f ϕ s₁ ⊆ ω f ϕ s₂

Tactic:
iInter₂_mono fun _u _hu ↦ closure_mono (image2_subset Subset.rfl hs)

Premises used: omegaLimit, Set.image2_subset, Set.iInter₂_mono, closure_mono, Set.Subset.rfl
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
⊢ IsClosed[inst] (ω f ϕ s)

Tactic:
isClosed_iInter fun _u ↦ isClosed_iInter fun _hu ↦ isClosed_closure

Premises used: omegaLimit, isClosed_closure, isClosed_iInter
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst_1 : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous[inst, inst_1] gb
simp :
  ∀ ⦃x : β⦄,
    (∀ (i : Set τ) (i_1 : i ∈ f), x ∈ closure[inst] (image2 ϕ i s)) →
      ∀ (i : Set τ) (i_1 : i ∈ f), gb x ∈ closure[inst_1] (image2 ϕ' i s')
⊢ MapsTo gb (ω f ϕ s) (ω f ϕ' s')

Tactic:
simp only [omegaLimit_def, mem_iInter, MapsTo]

Premises used: omegaLimit_def, Set.mem_iInter, Set.MapsTo
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst_1 : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous[inst, inst_1] gb
y : β
hy : ∀ (i : Set τ) (i_1 : i ∈ f), y ∈ closure[inst] (image2 ϕ i s)
u : Set τ
hu : u ∈ f
⊢ gb y ∈ closure[inst_1] (image2 ϕ' u s')

Tactic:
map_mem_closure hgc (hy _ (inter_mem hu hg)) (forall_mem_image2.2 fun t ht x hx ↦ ?_)

Premises used: Iff.mpr, Set.forall_mem_image2, Filter.inter_mem, map_mem_closure
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst_1 : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous[inst, inst_1] gb
y : β
hy : ∀ (i : Set τ) (i_1 : i ∈ f), y ∈ closure[inst] (image2 ϕ i s)
u : Set τ
hu : u ∈ f
refine :
  ∀ (t : τ) (ht : t ∈ u ∩ {x : τ | (fun (t : τ) ↦ EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s) x}) (x : α) (hx : x ∈ s),
    gb (ϕ t x) ∈ image2 ϕ' u s'
⊢ gb y ∈ closure[inst_1] (image2 ϕ' u s')

Tactic:
refine map_mem_closure hgc (hy _ (inter_mem hu hg)) (forall_mem_image2.2 fun t ht x hx ↦ ?_)

Premises used: Iff.mpr, Set.forall_mem_image2, Filter.inter_mem, map_mem_closure
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst_1 : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous[inst, inst_1] gb
y : β
hy : ∀ (i : Set τ) (i_1 : i ∈ f), y ∈ closure[inst] (image2 ϕ i s)
u : Set τ
hu : u ∈ f
t : τ
ht : t ∈ u ∩ {x : τ | (fun (t : τ) ↦ EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s) x}
x : α
hx : x ∈ s
⊢ ϕ' t (ga x) ∈ image2 ϕ' u s'

Tactic:
mem_image2_of_mem ht.1 (hs hx)

Premises used: And.left, Set.mem_image2_of_mem
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst_1 : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous[inst, inst_1] gb
y : β
hy : ∀ (i : Set τ) (i_1 : i ∈ f), y ∈ closure[inst] (image2 ϕ i s)
u : Set τ
hu : u ∈ f
t : τ
ht : t ∈ u ∩ {x : τ | (fun (t : τ) ↦ EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s) x}
x : α
hx : x ∈ s
⊢ ϕ' t (ga x) = gb (ϕ t x)

Tactic:
ht.2 hx |>.symm

Premises used: And.right, Eq.symm
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst_1 : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ᶠ (t : τ) in f, EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s
hgc : Continuous[inst, inst_1] gb
y : β
hy : ∀ (i : Set τ) (i_1 : i ∈ f), y ∈ closure[inst] (image2 ϕ i s)
u : Set τ
hu : u ∈ f
t : τ
ht : t ∈ u ∩ {x : τ | (fun (t : τ) ↦ EqOn (gb ∘ ϕ t) (ϕ' t ∘ ga) s) x}
x : α
hx : x ∈ s
⊢ gb (ϕ t x) ∈ image2 ϕ' u s'

Tactic:
calc
    ϕ' t (ga x) ∈ image2 ϕ' u s' := mem_image2_of_mem ht.1 (hs hx)
    _ = gb (ϕ t x) := ht.2 hx |>.symm

Premises used: And.right, And.left, Set.image2, Set.mem_image2_of_mem, Eq.symm
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
s : Set α
α' : Type u_5
β' : Type u_6
inst_1 : TopologicalSpace β'
f : Filter τ
ϕ : τ → α → β
ϕ' : τ → α' → β'
ga : α → α'
s' : Set α'
hs : MapsTo ga s s'
gb : β → β'
hg : ∀ (t : τ) (x : α), gb (ϕ t x) = ϕ' t (ga x)
hgc : Continuous[inst, inst_1] gb
⊢ MapsTo gb (ω f ϕ s) (ω f ϕ' s')

Tactic:
mapsTo_omegaLimit' _ hs (Eventually.of_forall fun t x _hx ↦ hg t x) hgc

Premises used: Filter.Eventually.of_forall, mapsTo_omegaLimit'
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
s : Set α
α' : Type u_5
ϕ : τ → α' → β
f : Filter τ
g : α → α'
⊢ ω f ϕ (g '' s) = ω f (fun (t : τ) (x : α) ↦ ϕ t (g x)) s

Tactic:
simp only [omegaLimit, image2_image_right]

Premises used: omegaLimit, Set.image2_image_right
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
α' : Type u_5
ϕ : τ → α' → β
s : Set α'
f : Filter τ
g : α → α'
⊢ ω f (fun (t : τ) (x : α) ↦ ϕ t (g x)) (g ⁻¹' s) ⊆ ω f ϕ s

Tactic:
mapsTo_omegaLimit _ (mapsTo_preimage _ _) (fun _t _x ↦ rfl) continuous_id

Premises used: Set.Mem, Set.Subset, Set.mapsTo_preimage, mapsTo_omegaLimit, continuous_id, Set.MapsTo, rfl
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
simp_rw :
  (∀ (i : Set τ) (i_1 : i ∈ f), ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty) ↔
    ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
⊢ y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (s ∩ ϕ t ⁻¹' n).Nonempty

Tactic:
simp_rw [frequently_iff, omegaLimit_def, mem_iInter, mem_closure_iff_nhds]

Premises used: Filter.frequently_iff, mem_closure_iff_nhds, omegaLimit_def, Set.mem_iInter
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
mp :
  (∀ (i : Set τ) (i_1 : i ∈ f), ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty) →
    ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
mpr :
  (∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty) →
    ∀ (i : Set τ) (i_1 : i ∈ f), ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
⊢ (∀ (i : Set τ) (i_1 : i ∈ f), ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty) ↔
    ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty

Tactic:
constructor
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ (i : Set τ) (i_1 : i ∈ f), ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
mp : ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
⊢ ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty

Tactic:
_
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ (i : Set τ) (i_1 : i ∈ f), ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
n : Set β
hn : n ∈ 𝓝 y
mp : ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
⊢ ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty

Tactic:
_
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ (i : Set τ) (i_1 : i ∈ f), ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
n : Set β
hn : n ∈ 𝓝 y
U : Set τ
hu : U ∈ f
mp : ∀ (w : τ) (ht : w ∈ U) (w_1 : α) (hx : w_1 ∈ s), ϕ w w_1 ∈ n → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
⊢ ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty

Tactic:
rcases h _ hu _ hn with ⟨_, _, _, ht, _, hx, rfl⟩

Premises used: rfl
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ (i : Set τ) (i_1 : i ∈ f), ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
n : Set β
hn : n ∈ 𝓝 y
U : Set τ
hu : U ∈ f
w : τ
ht : w ∈ U
w_1 : α
hx : w_1 ∈ s
left rwa rwa₁ rwa₂ rwa₃ : ϕ w w_1 ∈ n
⊢ w_1 ∈ ϕ w ⁻¹' n

Tactic:
rwa [mem_preimage]

Premises used: Set.mem_preimage
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ (i : Set τ) (i_1 : i ∈ f), ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
n : Set β
hn : n ∈ 𝓝 y
U : Set τ
hu : U ∈ f
w : τ
ht : w ∈ U
w_1 : α
hx : w_1 ∈ s
left : ϕ w w_1 ∈ n
⊢ ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty

Tactic:
exact ⟨_, ht, _, hx, by rwa [mem_preimage]⟩
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
mpr : ∀ (i : Set τ) (i_1 : i ∈ f), ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
⊢ ∀ (i : Set τ) (i_1 : i ∈ f), ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty

Tactic:
_
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
i : Set τ
hu : i ∈ f
mpr : ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
⊢ ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty

Tactic:
_
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
i : Set τ
hu : i ∈ f
t : Set β
hn : t ∈ 𝓝 y
mpr : ∀ (w : τ) (ht : w ∈ i) (w_1 : α) (hx : w_1 ∈ s) (hϕtx : w_1 ∈ ϕ w ⁻¹' t), (t ∩ image2 ϕ i s).Nonempty
⊢ (t ∩ image2 ϕ i s).Nonempty

Tactic:
rcases h _ hn hu with ⟨_, ht, _, hx, hϕtx⟩
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
i : Set τ
hu : i ∈ f
t : Set β
hn : t ∈ 𝓝 y
w : τ
ht : w ∈ i
w_1 : α
hx : w_1 ∈ s
hϕtx : w_1 ∈ ϕ w ⁻¹' t
⊢ (t ∩ image2 ϕ i s).Nonempty

Tactic:
⟨_, hϕtx, _, ht, _, hx, rfl⟩

Premises used: Set.Nonempty, And.intro, Exists.intro, rfl
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
i : Set τ
hu : i ∈ f
t : Set β
hn : t ∈ 𝓝 y
w : τ
ht : w ∈ i
w_1 : α
hx : w_1 ∈ s
hϕtx : w_1 ∈ ϕ w ⁻¹' t
⊢ (t ∩ image2 ϕ i s).Nonempty

Tactic:
exact ⟨_, hϕtx, _, ht, _, hx, rfl⟩
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
simp_rw : (∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (s ∩ ϕ t ⁻¹' n).Nonempty) ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (ϕ t '' s ∩ n).Nonempty
⊢ y ∈ ω f ϕ s ↔ ∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, (ϕ t '' s ∩ n).Nonempty

Tactic:
simp_rw [mem_omegaLimit_iff_frequently, image_inter_nonempty_iff]

Premises used: mem_omegaLimit_iff_frequently, Set.image_inter_nonempty_iff
-- Module: Mathlib.Dynamics.OmegaLimit
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
simp_rw₂ : (∀ n ∈ 𝓝 y, ∃ᶠ (t : τ) in f, x ∈ ϕ t ⁻¹' n) ↔ ∀ s ∈ 𝓝 y, ∃ᶠ (a : τ) in f, ϕ a x ∈ s
⊢ y ∈ ω f ϕ {x} ↔ MapClusterPt y f fun (t : τ) ↦ ϕ t x

Tactic:
simp_rw [mem_omegaLimit_iff_frequently, mapClusterPt_iff_frequently, singleton_inter_nonempty,
    mem_preimage]

Premises used: mapClusterPt_iff_frequently, mem_omegaLimit_iff_frequently, Set.singleton_inter_nonempty, Set.mem_preimage
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
⊢ ω f ϕ (s₁ ∩ s₂) ⊆ ω f ϕ s₁ ∩ ω f ϕ s₂

Tactic:
subset_inter (omegaLimit_mono_right _ _ inter_subset_left)
    (omegaLimit_mono_right _ _ inter_subset_right)

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

Tactic:
subset_iInter fun _i ↦ omegaLimit_mono_right _ _ (iInter_subset _ _)

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

Tactic:
ext y
-- Module: Mathlib.Dynamics.OmegaLimit
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₂
h₁ : y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂ → y ∈ ω f ϕ (s₁ ∪ s₂)
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) ↔ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂

Tactic:
constructor
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
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
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) → y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂

Tactic:
simp only [mem_union, mem_omegaLimit_iff_frequently, union_inter_distrib_right, union_nonempty,
      frequently_or_distrib]

Premises used: Set.mem_union, Set.union_nonempty, mem_omegaLimit_iff_frequently, Set.union_inter_distrib_right, Filter.frequently_or_distrib
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
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 = ∅
⊢ (∀ 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:
contrapose!
-- Module: Mathlib.Dynamics.OmegaLimit
Goal:
τ : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
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 ⊆ ∅
⊢ ((∃ 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]

Premises used: Set.subset_empty_iff