awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
m : ℕ
pm : ∃ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set X) (closure[inst] {x m}) (y n)
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l

Tactic:
subset_iUnion _ m (isClosed_closure.mem_of_frequently_of_tendsto pm hy')

Premises used: IsClosed.mem_of_frequently_of_tendsto, Set.subset_iUnion, isClosed_closure
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
m : ℕ
pm : ∃ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set X) (closure[inst] {x m}) (y n)
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l

Tactic:
exact subset_iUnion _ m (isClosed_closure.mem_of_frequently_of_tendsto pm hy')

Premises used: Set.subset_iUnion
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
j : ℕ
⊢ ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x k}) (y n)

Tactic:
frequently_atTop.2 fun a => ?_

Premises used: Iff.mpr, Filter.frequently_atTop
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
j : ℕ
refine : ∀ (a : ℕ), ∃ b ≥ a, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x b}) (y n)
⊢ ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x k}) (y n)

Tactic:
refine frequently_atTop.2 fun a => ?_

Premises used: Iff.mpr, Filter.frequently_atTop
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
j a : ℕ
⊢ (Iic a).Finite

Tactic:
simp
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
j a : ℕ
⊢ ∀ᶠ (x_1 : ℕ) in atTop, ∀ i ∈ Iic a, y x_1 ∉ closure[inst] {x i}

Tactic:
have := (Filter.eventually_all_finite (by simp : (Iic a).Finite)).2 fun i hi => hm i
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
j a : ℕ
this : ∀ᶠ (x_1 : ℕ) in atTop, ∀ i ∈ Iic a, y x_1 ∉ closure[inst] {x i}
⊢ ∃ (a_1 : ℕ), ∀ (b : ℕ), a_1 ≤ b → ∀ i ≤ a, y b ∉ closure[inst] {x i}

Tactic:
simp only [mem_Iic, eventually_atTop, ge_iff_le] at this

Premises used: ge_iff_le, Set.mem_Iic, Filter.eventually_atTop
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
j a : ℕ
this : ∃ (a_1 : ℕ), ∀ (b : ℕ), a_1 ≤ b → ∀ i ≤ a, y b ∉ closure[inst] {x i}
obtain :
  ∀ (c : ℕ) (hc : ∀ (b : ℕ), c ≤ b → ∀ i ≤ a, y b ∉ closure[inst] {x i}),
    ∃ b ≥ a, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x b}) (y n)
⊢ ∃ b ≥ a, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x b}) (y n)

Tactic:
obtain ⟨c, hc⟩ := this
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
j a c : ℕ
hc : ∀ (b : ℕ), c ≤ b → ∀ i ≤ a, y b ∉ closure[inst] {x i}
obtain :
  ∀ (b : ℕ) (hb : Membership.mem (γ := Set X) (closure[inst] {x b}) (y (c + j))),
    ∃ b ≥ a, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x b}) (y n)
⊢ ∃ b ≥ a, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x b}) (y n)

Tactic:
obtain ⟨b, hb⟩ := mem_iUnion.1 (hy (c + j))

Premises used: Set.mem_iUnion, HAdd.hAdd, Iff.mp
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
j a c : ℕ
hc : ∀ (b : ℕ), c ≤ b → ∀ i ≤ a, y b ∉ closure[inst] {x i}
b : ℕ
hb : Membership.mem (γ := Set X) (closure[inst] {x b}) (y (c + j))
⊢ ∃ b ≥ a, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x b}) (y n)

Tactic:
⟨b, ?_, c + j, j.le_add_left c, hb⟩

Premises used: Nat.le_add_left, HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
j a c : ℕ
hc : ∀ (b : ℕ), c ≤ b → ∀ i ≤ a, y b ∉ closure[inst] {x i}
b : ℕ
hb : Membership.mem (γ := Set X) (closure[inst] {x b}) (y (c + j))
refine : b ≥ a
⊢ ∃ b ≥ a, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x b}) (y n)

Tactic:
refine ⟨b, ?_, c + j, j.le_add_left c, hb⟩
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
j a c : ℕ
hc : ∀ (b : ℕ), c ≤ b → ∀ i ≤ a, y b ∉ closure[inst] {x i}
b : ℕ
hb : Membership.mem (γ := Set X) (closure[inst] {x b}) (y (c + j))
by_contra! : ∀ (hab : b < a), False
⊢ b ≥ a

Tactic:
by_contra! hab
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
j a c : ℕ
hc : ∀ (b : ℕ), c ≤ b → ∀ i ≤ a, y b ∉ closure[inst] {x i}
b : ℕ
hb : Membership.mem (γ := Set X) (closure[inst] {x b}) (y (c + j))
hab : b < a
⊢ False

Tactic:
simp_all [hc (c + j) (c.le_add_right j) b hab.le]

Premises used: Nat.le_add_right, LT.lt.le, HAdd.hAdd
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
⊢ ∀ (j : ℕ), ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x k}) (y n)

Tactic:
have (j : ℕ) : ∃ᶠ k in atTop, ∃ n ≥ j, y n ∈ closure {x k} := by
      refine frequently_atTop.2 fun a => ?_
      have := (Filter.eventually_all_finite (by simp : (Iic a).Finite)).2 fun i hi => hm i
      simp only [mem_Iic, eventually_atTop, ge_iff_le] at this
      obtain ⟨c, hc⟩ := this
      obtain ⟨b, hb⟩ := mem_iUnion.1 (hy (c + j))
      refine ⟨b, ?_, c + j, j.le_add_left c, hb⟩
      by_contra! hab
      simp_all [hc (c + j) (c.le_add_right j) b hab.le]
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
this : ∀ (j : ℕ), ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x k}) (y n)
neg :
  ∀ (φ : ℕ → ℕ)
    (hφ : StrictMono φ ∧ ∀ (n : ℕ), ∃ n_1 ≥ n, Membership.mem (γ := Set X) (closure[inst] {x (φ n)}) (y n_1)),
    Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l

Tactic:
obtain ⟨φ, hφ⟩ := extraction_forall_of_frequently this

Premises used: Filter.extraction_forall_of_frequently
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
this : ∀ (j : ℕ), ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x k}) (y n)
φ : ℕ → ℕ
hφ : StrictMono φ ∧ ∀ (n : ℕ), ∃ n_1 ≥ n, Membership.mem (γ := Set X) (closure[inst] {x (φ n)}) (y n_1)
neg :
  ∀ (ψ : (n : ℕ) → ℕ) (hψ1 : ∀ (n : ℕ), ψ n ≥ n)
    (hψ2 : ∀ (n : ℕ), Membership.mem (γ := Set X) (closure[inst] {x (φ n)}) (y (ψ n))),
    Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l

Tactic:
choose ψ hψ1 hψ2 using hφ.2

Premises used: And.right
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
this : ∀ (j : ℕ), ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x k}) (y n)
φ : ℕ → ℕ
hφ : StrictMono φ ∧ ∀ (n : ℕ), ∃ n_1 ≥ n, Membership.mem (γ := Set X) (closure[inst] {x (φ n)}) (y n_1)
ψ : (n : ℕ) → ℕ
hψ1 : ∀ (n : ℕ), ψ n ≥ n
hψ2 : ∀ (n : ℕ), Membership.mem (γ := Set X) (closure[inst] {x (φ n)}) (y (ψ n))
⊢ Tendsto ψ atTop atTop

Tactic:
have : Tendsto ψ atTop atTop := tendsto_atTop_mono hψ1 tendsto_id
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
this_1 : ∀ (j : ℕ), ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x k}) (y n)
φ : ℕ → ℕ
hφ : StrictMono φ ∧ ∀ (n : ℕ), ∃ n_1 ≥ n, Membership.mem (γ := Set X) (closure[inst] {x (φ n)}) (y n_1)
ψ : (n : ℕ) → ℕ
hψ1 : ∀ (n : ℕ), ψ n ≥ n
hψ2 : ∀ (n : ℕ), Membership.mem (γ := Set X) (closure[inst] {x (φ n)}) (y (ψ n))
this : Tendsto ψ atTop atTop
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l

Tactic:
(hx l φ hφ.1 (Tendsto.specializes (hy'.comp this) (fun n => ?_))).elim

Premises used: False.elim, Tendsto.specializes, And.left, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
this_1 : ∀ (j : ℕ), ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x k}) (y n)
φ : ℕ → ℕ
hφ : StrictMono φ ∧ ∀ (n : ℕ), ∃ n_1 ≥ n, Membership.mem (γ := Set X) (closure[inst] {x (φ n)}) (y n_1)
ψ : (n : ℕ) → ℕ
hψ1 : ∀ (n : ℕ), ψ n ≥ n
hψ2 : ∀ (n : ℕ), Membership.mem (γ := Set X) (closure[inst] {x (φ n)}) (y (ψ n))
this : Tendsto ψ atTop atTop
neg : ∀ (n : ℕ), (x ∘ φ) n ⤳ (y ∘ ψ) n
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l

Tactic:
refine (hx l φ hφ.1 (Tendsto.specializes (hy'.comp this) (fun n => ?_))).elim

Premises used: False.elim, Tendsto.specializes, And.left, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
this_1 : ∀ (j : ℕ), ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x k}) (y n)
φ : ℕ → ℕ
hφ : StrictMono φ ∧ ∀ (n : ℕ), ∃ n_1 ≥ n, Membership.mem (γ := Set X) (closure[inst] {x (φ n)}) (y n_1)
ψ : (n : ℕ) → ℕ
hψ1 : ∀ (n : ℕ), ψ n ≥ n
hψ2 : ∀ (n : ℕ), Membership.mem (γ := Set X) (closure[inst] {x (φ n)}) (y (ψ n))
this : Tendsto ψ atTop atTop
n : ℕ
⊢ (x ∘ φ) n ⤳ (y ∘ ψ) n

Tactic:
specializes_iff_mem_closure.2 (hψ2 n)

Premises used: Iff.mpr, specializes_iff_mem_closure
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}
this_1 : ∀ (j : ℕ), ∃ᶠ (k : ℕ) in atTop, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x k}) (y n)
φ : ℕ → ℕ
hφ : StrictMono φ ∧ ∀ (n : ℕ), ∃ n_1 ≥ n, Membership.mem (γ := Set X) (closure[inst] {x (φ n)}) (y n_1)
ψ : (n : ℕ) → ℕ
hψ1 : ∀ (n : ℕ), ψ n ≥ n
hψ2 : ∀ (n : ℕ), Membership.mem (γ := Set X) (closure[inst] {x (φ n)}) (y (ψ n))
this : Tendsto ψ atTop atTop
n : ℕ
⊢ (x ∘ φ) n ⤳ (y ∘ ψ) n

Tactic:
exact specializes_iff_mem_closure.2 (hψ2 n)

Premises used: Iff.mpr, specializes_iff_mem_closure
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
inst_2 : T1Space X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
⊢ IsClosed[inst] (range x)

Tactic:
simpa using isClosed_iUnion_closure_singleton_of_not_tendsto hx

Premises used: isClosed_iUnion_closure_singleton_of_not_tendsto
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsSeqClosed s
hf : SeqContinuous f
⊢ IsSeqClosed (f ⁻¹' s)

Tactic:
fun _x _p hx hp => hs hx (hf hp)

Premises used: Set.Mem, setOf, Set.preimage, IsSeqClosed
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ SeqContinuous f

Tactic:
fun _x p hx => (hf.tendsto p).comp hx

Premises used: Continuous.tendsto, Filter.Tendsto.comp, SeqContinuous
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SequentialSpace X
f : X → Y
hf : SeqContinuous f
⊢ Continuous[inst, inst_1] f

Tactic:
continuous_iff_isClosed.mpr fun _s hs => (hs.isSeqClosed.preimage hf).isClosed

Premises used: Iff.mpr, IsClosed.isSeqClosed, continuous_iff_isClosed, IsSeqClosed.isClosed, IsSeqClosed.preimage
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SequentialSpace X
f : X → Y
⊢ Continuous[inst, inst_1] f ↔ SeqContinuous f

Tactic:
⟨Continuous.seqContinuous, SeqContinuous.continuous⟩

Premises used: SeqContinuous.continuous, Continuous.seqContinuous, Iff.intro
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SequentialSpace X
Y : Type u_3
f : X → Y
⊢ SequentialSpace Y

Tactic:
letI : TopologicalSpace Y := .coinduced f ‹_›
  ⟨fun _ hs ↦ isClosed_coinduced.2 (hs.preimage continuous_coinduced_rng.seqContinuous).isClosed⟩

Premises used: Iff.mpr, SequentialSpace.mk, Continuous.seqContinuous, IsSeqClosed.isClosed, IsSeqClosed.preimage, continuous_coinduced_rng, isClosed_coinduced
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
this : TopologicalSpace X := ⨆ (i : ι), t i
⊢ SequentialSpace X

Tactic:
⟨fun s hs ↦ isClosed_iSup_iff.2 fun i ↦ ?_⟩

Premises used: Iff.mpr, isClosed_iSup_iff, SequentialSpace.mk
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
this : TopologicalSpace X := ⨆ (i : ι), t i
refine : ∀ (s : Set X) (hs : IsSeqClosed s) (i : ι), IsClosed[t i] s
⊢ SequentialSpace X

Tactic:
refine ⟨fun s hs ↦ isClosed_iSup_iff.2 fun i ↦ ?_⟩
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
this_1 : TopologicalSpace X := ⨆ (i : ι), t i
s : Set X
hs : IsSeqClosed s
i : ι
this : TopologicalSpace X := t i
⊢ IsClosed[t i] s

Tactic:
IsSeqClosed.isClosed fun u x hus hux ↦ hs hus <| hux.mono_right <| nhds_mono <| le_iSup _ _

Premises used: le_iSup, nhds_mono, IsSeqClosed.isClosed, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
this_1 : TopologicalSpace X := ⨆ (i : ι), t i
s : Set X
hs : IsSeqClosed s
i : ι
this : TopologicalSpace X := t i
⊢ IsClosed[t i] s

Tactic:
exact IsSeqClosed.isClosed fun u x hus hux ↦ hs hus <| hux.mono_right <| nhds_mono <| le_iSup _ _

Premises used: le_iSup, nhds_mono, IsSeqClosed.isClosed, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : SequentialSpace X
h₂ : SequentialSpace X
rw : SequentialSpace X
⊢ SequentialSpace X

Tactic:
rw [sup_eq_iSup]

Premises used: sup_eq_iSup
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : SequentialSpace X
h₂ : SequentialSpace X
⊢ SequentialSpace X

Tactic:
.iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩

Premises used: Iff.mpr, SequentialSpace.iSup, Bool.forall_bool, And.intro
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : SequentialSpace X
h₂ : SequentialSpace X
⊢ SequentialSpace X

Tactic:
exact .iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩

Premises used: Iff.mpr, Bool.forall_bool, And.intro
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SequentialSpace X
f : X → Y
hf : IsQuotientMap f
⊢ SequentialSpace Y

Tactic:
hf.isCoinducing.eq_coinduced.symm ▸ .coinduced f

Premises used: Eq.rec, Topology.IsCoinducing.eq_coinduced, Topology.IsQuotientMap.isCoinducing, Eq.symm, SequentialSpace.coinduced
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SequentialSpace X
s : Setoid X
⊢ SequentialSpace.{u_1} (Quotient s)

Tactic:
isQuotientMap_quot_mk.sequentialSpace

Premises used: Topology.IsQuotientMap.sequentialSpace, Quotient, Quotient.mk', isQuotientMap_quot_mk
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : SequentialSpace X
inst_3 : SequentialSpace Y
⊢ SequentialSpace (X ⊕ Y)

Tactic:
.sup (.coinduced Sum.inl) (.coinduced Sum.inr)

Premises used: setOf, Sum.inl, Sum.inr, SequentialSpace.sup, SequentialSpace.coinduced
-- Module: Mathlib.Topology.Sequences
Goal:
X_1 : Type u_1
Y : Type u_2
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
ι : Type u_3
X : ι → Type u_4
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), SequentialSpace.{u_4} (X i)
⊢ SequentialSpace ((i : ι) × X i)

Tactic:
.iSup fun _ ↦ .coinduced _

Premises used: SequentialSpace.iSup, Sigma.mk, SequentialSpace.coinduced
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsSeqCompact s
x : ℕ → X
hx : ∃ᶠ (n : ℕ) in atTop, x n ∈ s
⊢ ∃ a ∈ s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
let ⟨ψ, hψ, huψ⟩ := extraction_of_frequently_atTop hx
  let ⟨a, a_in, φ, hφ, h⟩ := hs huψ
  ⟨a, a_in, ψ ∘ φ, hψ.comp hφ, h⟩

Premises used: StrictMono, Function.comp, Membership.mem, Exists, _private.0.IsSeqCompact.subseq_of_frequently_in.match_1, nhds, _private.0.IsSeqCompact.subseq_of_frequently_in.match_2, Filter.extraction_of_frequently_atTop, Filter.atTop, And, Filter.Tendsto, And.intro, Exists.intro, StrictMono.comp
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SeqCompactSpace X
x : ℕ → X
⊢ ∃ (a : X) (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
let ⟨a, _, φ, mono, h⟩ := isSeqCompact_univ fun n => mem_univ (x n)
  ⟨a, φ, mono, h⟩

Premises used: SeqCompactSpace.isSeqCompact_univ, StrictMono, Function.comp, Exists, nhds, Filter.atTop, And, _private.0.SeqCompactSpace.tendsto_subseq.match_1, Filter.Tendsto, And.intro, Exists.intro, Set.mem_univ
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : FirstCountableTopology X
s : Set X
hs : IsCompact s
⊢ IsSeqCompact s

Tactic:
fun _x x_in =>
  let ⟨a, a_in, ha⟩ := hs (tendsto_principal.mpr (Eventually.of_forall x_in))
  ⟨a, a_in, MapClusterPt.tendsto_subseq ha⟩

Premises used: Iff.mpr, StrictMono, _private.0.IsCompact.isSeqCompact.match_1, Function.comp, Membership.mem, Exists, nhds, Filter.Eventually.of_forall, Filter.tendsto_principal, Filter.atTop, And, MapClusterPt.tendsto_subseq, Filter.Tendsto, And.intro, Exists.intro, IsSeqCompact
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : FirstCountableTopology X
s : Set X
x : ℕ → X
hs : IsCompact s
hx : ∃ᶠ (n : ℕ) in atTop, x n ∈ s
⊢ ∃ a ∈ s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
hs.isSeqCompact.subseq_of_frequently_in hx

Premises used: IsSeqCompact.subseq_of_frequently_in, IsCompact.isSeqCompact
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : FirstCountableTopology X
s : Set X
x : ℕ → X
hs : IsCompact s
hx : ∀ (n : ℕ), x n ∈ s
⊢ ∃ a ∈ s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
hs.isSeqCompact hx

Premises used: IsCompact.isSeqCompact
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : FirstCountableTopology X
inst_2 : CompactSpace X
⊢ SeqCompactSpace X

Tactic:
⟨isCompact_univ.isSeqCompact⟩

Premises used: isCompact_univ, SeqCompactSpace.mk, IsCompact.isSeqCompact