awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
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)
pos :
  ∀ (hm : ∃ (m : ℕ), ∃ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set X) (closure[inst] {x m}) (y n)),
    Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
have neg : ∀ (hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}),
  Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
Tactic: by_cases! hm : ∃ m, ∃ᶠ n in atTop, y n ∈ closure {x m}
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
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 : ℕ), ∃ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set X) (closure[inst] {x m}) (y n)
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
have pos : ∀ (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: obtain ⟨m, pm⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
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)
have refine : ∀ (a : ℕ), ∃ b ≥ a, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x b}) (y n)
Tactic: refine frequently_atTop.2 fun a => ?_
-- Lean 4 proof step from Mathlib.Topology.Sequences (hypothesis)
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 : ℕ
⊢ ∃ b ≥ a, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x b}) (y n)
have this : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Topology.Sequences (hypothesis)
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}
⊢ ∃ b ≥ a, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x b}) (y n)
have this₁ : ∃ (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
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}
⊢ ∃ b ≥ a, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x b}) (y n)
have 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)
Tactic: obtain ⟨c, hc⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
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 ≥ a, ∃ n ≥ j, Membership.mem (γ := Set X) (closure[inst] {x b}) (y n)
have 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)
Tactic: obtain ⟨b, hb⟩ := mem_iUnion.1 (hy (c + j))
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
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)
have refine : b ≥ a
Tactic: refine ⟨b, ?_, c + j, j.le_add_left c, hb⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
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
have by_contra! : ∀ (hab : b < a), False
Tactic: by_contra! hab
-- Lean 4 proof step from Mathlib.Topology.Sequences (hypothesis)
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}
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
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)
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
have 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
Tactic: obtain ⟨φ, hφ⟩ := extraction_forall_of_frequently this
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
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)
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
have 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
Tactic: choose ψ hψ1 hψ2 using hφ.2
-- Lean 4 proof step from Mathlib.Topology.Sequences (hypothesis)
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))
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
have this₁ : Tendsto ψ atTop atTop
Tactic: have : Tendsto ψ atTop atTop := tendsto_atTop_mono hψ1 tendsto_id
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
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
have neg : ∀ (n : ℕ), (x ∘ φ) n ⤳ (y ∘ ψ) n
Tactic: refine (hx l φ hφ.1 (Tendsto.specializes (hy'.comp this) (fun n => ?_))).elim
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_4
ι : Sort u_3
t : ι → TopologicalSpace X
h : ∀ (i : ι), SequentialSpace X
this : TopologicalSpace X := ⨆ (i : ι), t i
⊢ SequentialSpace X
have refine : ∀ (s : Set X) (hs : IsSeqClosed s) (i : ι), IsClosed[t i] s
Tactic: refine ⟨fun s hs ↦ isClosed_iSup_iff.2 fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : SequentialSpace X
h₂ : SequentialSpace X
⊢ SequentialSpace X
have rw : SequentialSpace X
Tactic: rw [sup_eq_iSup]
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
ys : ℕ → Y
ys_in_fK : ∀ (n : ℕ), ys n ∈ f '' K
⊢ ∃ a ∈ f '' K, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)
have choose : ∀ (xs : (n : ℕ) → X) (xs_in_K : ∀ (n : ℕ), xs n ∈ K) (fxs_eq_ys : ∀ (n : ℕ), f (xs n) = ys n),
  ∃ a ∈ f '' K, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)
Tactic: choose xs xs_in_K fxs_eq_ys using ys_in_fK
Cleared hypotheses: ys_in_fK
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
ys : ℕ → Y
xs : (n : ℕ) → X
xs_in_K : ∀ (n : ℕ), xs n ∈ K
fxs_eq_ys : ∀ (n : ℕ), f (xs n) = ys n
⊢ ∃ a ∈ f '' K, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)
have obtain : ∀ (a : X) (a_in_K : a ∈ K) (phi : ℕ → ℕ) (phi_mono : StrictMono phi) (xs_phi_lim : Tendsto (xs ∘ phi) atTop (𝓝 a)),
  ∃ a ∈ f '' K, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)
Tactic: obtain ⟨a, a_in_K, phi, phi_mono, xs_phi_lim⟩ := K_cpt xs_in_K
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
f_cont : SeqContinuous f
K : Set X
K_cpt : IsSeqCompact K
ys : ℕ → Y
xs : (n : ℕ) → X
xs_in_K : ∀ (n : ℕ), xs n ∈ K
fxs_eq_ys : ∀ (n : ℕ), f (xs n) = ys n
a : X
a_in_K : a ∈ K
phi : ℕ → ℕ
phi_mono : StrictMono phi
xs_phi_lim : Tendsto (xs ∘ phi) atTop (𝓝 a)
⊢ ∃ a ∈ f '' K, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)
have refine : Tendsto (ys ∘ phi) atTop (𝓝 (f a))
Tactic: refine ⟨f a, mem_image_of_mem f a_in_K, phi, phi_mono, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
h : ∀ ⦃x : ℕ → X⦄, (∀ (n : ℕ), x n ∈ s) → ∃ a ∈ s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
V : Set (X × X)
V_in : V ∈ 𝓤 X
⊢ ∃ (t : Set X), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : X | (x, y) ∈ V}
have contrapose! : ∀ (h : ∀ (t : Set X) (_ : t.Finite), ¬s ⊆ ⋃ y ∈ t, {x : X | (x, y) ∈ V}),
  ∃ (x : ℕ → X),
    (∀ (n : ℕ), x n ∈ s) ∧ ∀ (a : X) (_ : a ∈ s) (φ : ℕ → ℕ) (_ : StrictMono φ), ¬Tendsto (x ∘ φ) atTop (𝓝 a)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Sequences (hypothesis)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X) (_ : t.Finite), ¬s ⊆ ⋃ y ∈ t, {x : X | (x, y) ∈ V}
⊢ ∃ (u : ℕ → X), (∀ (n : ℕ), u n ∈ s) ∧ ∀ (n m : ℕ), m < n → u m ∉ ball (u n) V
have h₁ : ∀ (t : Set X) (_ : t.Finite), ∃ a ∈ s, ∀ (x : X), ¬(x ∈ t ∧ Membership.mem (γ := Set X) {x_1 : X | (x_1, x) ∈ V} a)
Tactic: simp only [not_subset, mem_iUnion₂, not_exists, exists_prop] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X) (_ : t.Finite), ¬s ⊆ ⋃ y ∈ t, {x : X | (x, y) ∈ V}
⊢ ∃ (x : ℕ → X),
    (∀ (n : ℕ), x n ∈ s) ∧ ∀ (a : X) (_ : a ∈ s) (φ : ℕ → ℕ) (_ : StrictMono φ), ¬Tendsto (x ∘ φ) atTop (𝓝 a)
have obtain : ∀ (u : ℕ → X) (u_in : ∀ (n : ℕ), u n ∈ s) (hu : ∀ (n m : ℕ), m < n → u m ∉ ball (u n) V),
  ∃ (x : ℕ → X),
    (∀ (n : ℕ), x n ∈ s) ∧ ∀ (a : X) (_ : a ∈ s) (φ : ℕ → ℕ) (_ : StrictMono φ), ¬Tendsto (x ∘ φ) atTop (𝓝 a)
Tactic: obtain ⟨u, u_in, hu⟩ : ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ ∀ n m, m < n → u m ∉ ball (u n) V := by
    simp only [not_subset, mem_iUnion₂, not_exists, exists_prop] at h
    simpa only [forall_and, forall_mem_image, not_and] using seq_of_forall_finite_exists h
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X) (_ : t.Finite), ¬s ⊆ ⋃ y ∈ t, {x : X | (x, y) ∈ V}
u : ℕ → X
u_in : ∀ (n : ℕ), u n ∈ s
hu : ∀ (n m : ℕ), m < n → u m ∉ ball (u n) V
⊢ ∃ (x : ℕ → X),
    (∀ (n : ℕ), x n ∈ s) ∧ ∀ (a : X) (_ : a ∈ s) (φ : ℕ → ℕ) (_ : StrictMono φ), ¬Tendsto (x ∘ φ) atTop (𝓝 a)
have refine : ∀ x ∈ s, ∀ (φ : ℕ → ℕ) (hφ : StrictMono φ) (huφ : Tendsto (u ∘ φ) atTop (𝓝 x)), False
Tactic: refine ⟨u, u_in, fun x _ φ hφ huφ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
h : ∀ (t : Set X) (_ : t.Finite), ¬s ⊆ ⋃ y ∈ t, {x : X | (x, y) ∈ V}
u : ℕ → X
u_in : ∀ (n : ℕ), u n ∈ s
hu : ∀ (n m : ℕ), m < n → u m ∉ ball (u n) V
x : X
h_1 : x ∈ s
φ : ℕ → ℕ
hφ : StrictMono φ
huφ : Tendsto (u ∘ φ) atTop (𝓝 x)
⊢ False
have obtain : ∀ (N : ℕ) (hN : ∀ (p q : ℕ), p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V), False
Tactic: obtain ⟨N, hN⟩ : ∃ N, ∀ p q, p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V :=
    huφ.cauchySeq.mem_entourage V_in
-- Lean 4 proof step from Mathlib.Topology.Sequences (hypothesis)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
⊢ ∃ x ∈ s, l ≤ 𝓝 x
have this : l.NeBot
Tactic: have := hl.1
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
⊢ ∃ x ∈ s, l ≤ 𝓝 x
have rcases : ∀ (V : ℕ → Set (X × X)) (hV : (𝓤 X).HasAntitoneBasis V), ∃ x ∈ s, l ≤ 𝓝 x
Tactic: rcases exists_antitone_basis (𝓤 X) with ⟨V, hV⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
⊢ ∃ x ∈ s, l ≤ 𝓝 x
have choose : ∀ (W : (n : ℕ) → Set (X × X)) (hW : ∀ (n : ℕ), W n ∈ 𝓤 X) (hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n),
  ∃ x ∈ s, l ≤ 𝓝 x
Tactic: choose W hW hWV using fun n => comp_mem_uniformity_sets (hV.mem n)
-- Lean 4 proof step from Mathlib.Topology.Sequences (hypothesis)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
⊢ ∃ x ∈ s, l ≤ 𝓝 x
have hWV' : ∀ (n : ℕ), W n ⊆ V n
Tactic: have hWV' : ∀ n, W n ⊆ V n := fun n ⟨x, y⟩ hx =>
    @hWV n (x, y) ⟨x, refl_mem_uniformity <| hW _, hx⟩
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∀ (n : ℕ), ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s
have rw : ∀ (hls : s ∈ l) (this : l.NeBot) (V : ℕ → Set (X × X)) (hV : (𝓤 X).HasAntitoneBasis V) (W : (n : ℕ) → Set (X × X))
  (hW : ∀ (n : ℕ), W n ∈ 𝓤 X) (hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n) (hWV' : ∀ (n : ℕ), W n ⊆ V n) (n : ℕ),
  ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s
Tactic: rw [le_principal_iff] at hls
Cleared hypotheses: hls, this, V, hV, W, hW, hWV, hWV'
-- Lean 4 proof step from Mathlib.Topology.Sequences (hypothesis)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : s ∈ l
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∀ (n : ℕ), ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s
have this₁ : ∀ (n : ℕ), W n ∩ s ×ˢ s ∈ l ×ˢ l
Tactic: have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)
-- Lean 4 proof step from Mathlib.Topology.Sequences (hypothesis)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∃ (t : ℕ → Set X), Antitone t ∧ (∀ (n : ℕ), t n ∈ l) ∧ (∀ (n : ℕ), t n ×ˢ t n ⊆ W n) ∧ ∀ (n : ℕ), t n ⊆ s
have this₁ : ∀ (n : ℕ), ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s
Tactic: have : ∀ n, ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s := by
      rw [le_principal_iff] at hls
      have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)
      simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff,
        prod_self_subset_prod_self, and_assoc] using this
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this_1 : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
this : ∀ (n : ℕ), ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s
⊢ ∃ (t : ℕ → Set X), Antitone t ∧ (∀ (n : ℕ), t n ∈ l) ∧ (∀ (n : ℕ), t n ×ˢ t n ⊆ W n) ∧ ∀ (n : ℕ), t n ⊆ s
have choose : ∀ (t : (n : ℕ) → Set X) (htl : ∀ (n : ℕ), t n ∈ l) (htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n) (hts : ∀ (n : ℕ), t n ⊆ s),
  ∃ (t : ℕ → Set X), Antitone t ∧ (∀ (n : ℕ), t n ∈ l) ∧ (∀ (n : ℕ), t n ×ˢ t n ⊆ W n) ∧ ∀ (n : ℕ), t n ⊆ s
Tactic: choose t htl htW hts using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : (n : ℕ) → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
n : ℕ
⊢ ⋂ (k : ℕ), ⋂ (_ : k ≤ n), t k ⊆ t n
have j : n ≤ n
Tactic: apply iInter₂_subset
-- Lean 4 proof step from Mathlib.Topology.Sequences (hypothesis)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
t : (n : ℕ) → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
⊢ ∃ (t : ℕ → Set X), Antitone t ∧ (∀ (n : ℕ), t n ∈ l) ∧ (∀ (n : ℕ), t n ×ˢ t n ⊆ W n) ∧ ∀ (n : ℕ), t n ⊆ s
have this₁ : ∀ (n : ℕ), ⋂ (k : ℕ), ⋂ (_ : k ≤ n), t k ⊆ t n
Tactic: have : ∀ n : ℕ, ⋂ k ≤ n, t k ⊆ t n := fun n => by apply iInter₂_subset; rfl
-- Lean 4 proof step from Mathlib.Topology.Sequences (goal)
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
inst_1 : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : (n : ℕ) → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∃ x ∈ s, l ≤ 𝓝 x
have obtain : ∀ (t : ℕ → Set X) (ht_anti : Antitone t) (htl : ∀ (n : ℕ), t n ∈ l) (htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n)
  (hts : ∀ (n : ℕ), t n ⊆ s), ∃ x ∈ s, l ≤ 𝓝 x
Tactic: obtain ⟨t, ht_anti, htl, htW, hts⟩ :
      ∃ t : ℕ → Set X, Antitone t ∧ (∀ n, t n ∈ l) ∧ (∀ n, t n ×ˢ t n ⊆ W n) ∧ ∀ n, t n ⊆ s := by
    have : ∀ n, ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s := by
      rw [le_principal_iff] at hls
      have : ∀ n, W n ∩ s ×ˢ s ∈ l ×ˢ l := fun n => inter_mem (hl.2 (hW n)) (prod_mem_prod hls hls)
      simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff,
        prod_self_subset_prod_self, and_assoc] using this
    choose t htl htW hts using this
    have : ∀ n : ℕ, ⋂ k ≤ n, t k ⊆ t n := fun n => by apply iInter₂_subset; rfl
    exact ⟨fun n => ⋂ k ≤ n, t k, fun m n h =>
      biInter_subset_biInter_left fun k (hk : k ≤ m) => hk.trans h, fun n =>
      (biInter_mem (finite_le_nat n)).2 fun k _ => htl k, fun n =>
      (prod_mono (this n) (this n)).trans (htW n), fun n => (this n).trans (hts n)⟩