awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : FirstCountableTopology X
inst_2 : CompactSpace X
x : ℕ → X
⊢ ∃ (a : X) (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
SeqCompactSpace.tendsto_subseq x

Premises used: SeqCompactSpace.tendsto_subseq
-- Module: Mathlib.Topology.Sequences
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
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)
⊢ ∃ a ∈ f '' K, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)

Tactic:
choose xs xs_in_K fxs_eq_ys using ys_in_fK
-- Module: Mathlib.Topology.Sequences
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
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)
⊢ ∃ 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
-- Module: Mathlib.Topology.Sequences
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)

Tactic:
⟨f a, mem_image_of_mem f a_in_K, phi, phi_mono, ?_⟩

Premises used: Set.mem_image_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Topology.Sequences
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)
refine : Tendsto (ys ∘ phi) atTop (𝓝 (f a))
⊢ ∃ a ∈ f '' K, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (ys ∘ φ) atTop (𝓝 a)

Tactic:
refine ⟨f a, mem_image_of_mem f a_in_K, phi, phi_mono, ?_⟩
-- Module: Mathlib.Topology.Sequences
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)
⊢ Tendsto (ys ∘ phi) atTop (𝓝 (f a))

Tactic:
(f_cont xs_phi_lim).congr fun x ↦ fxs_eq_ys (phi x)

Premises used: Filter.Tendsto.congr
-- Module: Mathlib.Topology.Sequences
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)
⊢ Tendsto (ys ∘ phi) atTop (𝓝 (f a))

Tactic:
exact (f_cont xs_phi_lim).congr fun x ↦ fxs_eq_ys (phi x)

Premises used: Filter.Tendsto.congr
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
inst_2 : SeqCompactSpace X
f_cont : SeqContinuous f
⊢ IsSeqCompact (Set.range f)

Tactic:
simpa using isSeqCompact_univ.image f_cont

Premises used: SeqCompactSpace.isSeqCompact_univ, IsSeqCompact.image
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
hs : IsSeqCompact s
u : ℕ → X
hu : ∃ᶠ (n : ℕ) in atTop, u n ∈ s
huc : CauchySeq u
⊢ ∃ x ∈ s, Tendsto u atTop (𝓝 x)

Tactic:
let ⟨x, hxs, _φ, φ_mono, hx⟩ := hs.subseq_of_frequently_in hu
  ⟨x, hxs, tendsto_nhds_of_cauchySeq_of_subseq huc φ_mono.tendsto_atTop hx⟩

Premises used: IsSeqCompact.subseq_of_frequently_in, Membership.mem, Exists, nhds, StrictMono.tendsto_atTop, tendsto_nhds_of_cauchySeq_of_subseq, Filter.atTop, And, Filter.Tendsto, And.intro, Exists.intro, _private.0.IsSeqCompact.exists_tendsto_of_frequently_mem.match_1
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : UniformSpace X
s : Set X
hs : IsSeqCompact s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ s
huc : CauchySeq u
⊢ ∃ x ∈ s, Tendsto u atTop (𝓝 x)

Tactic:
hs.exists_tendsto_of_frequently_mem (Frequently.of_forall hu) huc

Premises used: Filter.Frequently.of_forall, IsSeqCompact.exists_tendsto_of_frequently_mem
-- Module: Mathlib.Topology.Sequences
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
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)
⊢ ∃ (t : Set X), t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : X | (x, y) ∈ V}

Tactic:
contrapose! h
-- Module: Mathlib.Topology.Sequences
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}
⊢ ∀ (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

Premises used: not_exists, exists_prop, Set.mem_iUnion₂, Set.not_subset
-- Module: Mathlib.Topology.Sequences
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), ∃ a ∈ s, ∀ (x : X), ¬(x ∈ t ∧ Membership.mem (γ := Set X) {x_1 : X | (x_1, x) ∈ V} a)
⊢ ∃ (u : ℕ → X), (∀ (n : ℕ), u n ∈ s) ∧ ∀ (n m : ℕ), m < n → u m ∉ ball (u n) V

Tactic:
simpa only [forall_and, forall_mem_image, not_and] using seq_of_forall_finite_exists h

Premises used: Set.seq_of_forall_finite_exists, not_and, Set.forall_mem_image, forall_and
-- Module: Mathlib.Topology.Sequences
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}
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)
⊢ ∃ (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
-- Module: Mathlib.Topology.Sequences
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)

Tactic:
⟨u, u_in, fun x _ φ hφ huφ => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Sequences
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
refine : ∀ x ∈ s, ∀ (φ : ℕ → ℕ) (hφ : StrictMono φ) (huφ : Tendsto (u ∘ φ) atTop (𝓝 x)), False
⊢ ∃ (x : ℕ → X),
    (∀ (n : ℕ), x n ∈ s) ∧ ∀ (a : X) (_ : a ∈ s) (φ : ℕ → ℕ) (_ : StrictMono φ), ¬Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
refine ⟨u, u_in, fun x _ φ hφ huφ => ?_⟩
-- Module: Mathlib.Topology.Sequences
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)
⊢ ∃ (N : ℕ), ∀ (p q : ℕ), p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V

Tactic:
huφ.cauchySeq.mem_entourage V_in

Premises used: Set.Mem, Filter.Tendsto.cauchySeq, CauchySeq.mem_entourage
-- Module: Mathlib.Topology.Sequences
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)
obtain : ∀ (N : ℕ) (hN : ∀ (p q : ℕ), p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V), False
⊢ False

Tactic:
obtain ⟨N, hN⟩ : ∃ N, ∀ p q, p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V :=
    huφ.cauchySeq.mem_entourage V_in

Premises used: Filter.Tendsto.cauchySeq, CauchySeq.mem_entourage
-- Module: Mathlib.Topology.Sequences
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)
N : ℕ
hN : ∀ (p q : ℕ), p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V
⊢ False

Tactic:
hu (φ <| N + 1) (φ N) (hφ <| Nat.lt_add_one N) (hN (N + 1) N N.le_succ le_rfl)

Premises used: le_rfl, Nat.lt_add_one, Nat.le_succ, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Topology.Sequences
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)
N : ℕ
hN : ∀ (p q : ℕ), p ≥ N → q ≥ N → (u (φ p), u (φ q)) ∈ V
⊢ False

Tactic:
exact hu (φ <| N + 1) (φ N) (hφ <| Nat.lt_add_one N) (hN (N + 1) N N.le_succ le_rfl)

Premises used: le_rfl, Nat.lt_add_one, Nat.le_succ, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Topology.Sequences
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
⊢ l.NeBot

Tactic:
have := hl.1
-- Module: Mathlib.Topology.Sequences
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
rcases : ∀ (V : ℕ → Set (X × X)) (hV : (𝓤 X).HasAntitoneBasis V), ∃ x ∈ s, l ≤ 𝓝 x
⊢ ∃ x ∈ s, l ≤ 𝓝 x

Tactic:
rcases exists_antitone_basis (𝓤 X) with ⟨V, hV⟩

Premises used: uniformity, Filter.exists_antitone_basis
-- Module: Mathlib.Topology.Sequences
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
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
⊢ ∃ x ∈ s, l ≤ 𝓝 x

Tactic:
choose W hW hWV using fun n => comp_mem_uniformity_sets (hV.mem n)

Premises used: Filter.HasAntitoneBasis.mem, comp_mem_uniformity_sets
-- Module: Mathlib.Topology.Sequences
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
⊢ ∀ (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⟩
-- Module: Mathlib.Topology.Sequences
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
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
⊢ ∀ (n : ℕ), ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s

Tactic:
rw [le_principal_iff] at hls

Premises used: Filter.le_principal_iff
-- Module: Mathlib.Topology.Sequences
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 : ℕ), 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)
-- Module: Mathlib.Topology.Sequences
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_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 : ℕ), W n ∩ s ×ˢ s ∈ l ×ˢ l
⊢ ∀ (n : ℕ), ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s

Tactic:
simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff,
        prod_self_subset_prod_self, and_assoc] using this

Premises used: Filter.HasBasis.mem_iff, Set.subset_inter_iff, Filter.HasBasis.prod_self, Filter.basis_sets, true_imp_iff, and_assoc, Set.prod_self_subset_prod_self
-- Module: Mathlib.Topology.Sequences
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

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
-- Module: Mathlib.Topology.Sequences
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
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
⊢ ∃ (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
-- Module: Mathlib.Topology.Sequences
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 : ℕ
j : n ≤ n
⊢ ⋂ (k : ℕ), ⋂ (_ : k ≤ n), t k ⊆ t n

Tactic:
apply iInter₂_subset

Premises used: Set.iInter₂_subset
-- Module: Mathlib.Topology.Sequences
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 : ℕ
⊢ n ≤ n

Tactic:
rfl
-- Module: Mathlib.Topology.Sequences
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

Tactic:
have : ∀ n : ℕ, ⋂ k ≤ n, t k ⊆ t n := fun n => by apply iInter₂_subset; rfl
-- Module: Mathlib.Topology.Sequences
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
t : (n : ℕ) → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
this : ∀ (n : ℕ), ⋂ (k : ℕ), ⋂ (_ : k ≤ n), t k ⊆ t n
⊢ ∃ (t : ℕ → Set X), Antitone t ∧ (∀ (n : ℕ), t n ∈ l) ∧ (∀ (n : ℕ), t n ×ˢ t n ⊆ W n) ∧ ∀ (n : ℕ), t n ⊆ s

Tactic:
⟨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)⟩

Premises used: Iff.mpr, Set.iInter, HasSubset.Subset.trans, Set.biInter_subset_biInter_left, And.intro, Filter.biInter_mem, Exists.intro, Set.prod_mono, LE.le.trans, Set.finite_le_nat
-- Module: Mathlib.Topology.Sequences
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
t : (n : ℕ) → Set X
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
this : ∀ (n : ℕ), ⋂ (k : ℕ), ⋂ (_ : k ≤ n), t k ⊆ t n
⊢ ∃ (t : ℕ → Set X), Antitone t ∧ (∀ (n : ℕ), t n ∈ l) ∧ (∀ (n : ℕ), t n ×ˢ t n ⊆ W n) ∧ ∀ (n : ℕ), t n ⊆ s

Tactic:
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)⟩
-- Module: Mathlib.Topology.Sequences
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
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
⊢ ∃ 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)⟩
-- Module: Mathlib.Topology.Sequences
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
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
choose : ∀ (u : (n : ℕ) → X) (hu : ∀ (n : ℕ), u n ∈ t n), ∃ x ∈ s, l ≤ 𝓝 x
⊢ ∃ x ∈ s, l ≤ 𝓝 x

Tactic:
choose u hu using fun n => Filter.nonempty_of_mem (htl n)

Premises used: Filter.nonempty_of_mem
-- Module: Mathlib.Topology.Sequences
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
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
⊢ CauchySeq u

Tactic:
have huc : CauchySeq u := hV.toHasBasis.cauchySeq_iff.2 fun N _ =>
      ⟨N, fun m hm n hn => hWV' _ <| @htW N (_, _) ⟨ht_anti hm (hu _), ht_anti hn (hu _)⟩⟩
-- Module: Mathlib.Topology.Sequences
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
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
rcases : ∀ (x : X) (hxs : x ∈ s) (hx : Tendsto u atTop (𝓝 x)), ∃ x ∈ s, l ≤ 𝓝 x
⊢ ∃ x ∈ s, l ≤ 𝓝 x

Tactic:
rcases hs.exists_tendsto (fun n => hts n (hu n)) huc with ⟨x, hxs, hx⟩

Premises used: IsSeqCompact.exists_tendsto
-- Module: Mathlib.Topology.Sequences
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
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : (n : ℕ) → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
⊢ ∃ x ∈ s, l ≤ 𝓝 x

Tactic:
⟨x, hxs, (nhds_basis_uniformity' hV.toHasBasis).ge_iff.2 fun N _ => ?_⟩

Premises used: Iff.mpr, Filter.HasAntitoneBasis.toHasBasis, nhds_basis_uniformity', Filter.HasBasis.ge_iff, And.intro, Exists.intro