awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsSeqCompact A
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
a : E
ha : a ∈ A
φ : ℕ → ℕ
hφ : StrictMono φ
hφa : Tendsto (x ∘ φ) atTop (𝓝 a)
⊢ ∃ a ∈ A, MapClusterPt a atTop x

Tactic:
exact ⟨a, ha, hφa.mapClusterPt.of_comp hφ.tendsto_atTop⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A : Set E
hA : IsCountablyCompact A
f : E → F
hf : Continuous[inst, inst_1] f
l : Filter F
hl_nebot : l.NeBot
hl_count : l.IsCountablyGenerated
hle : l ≤ 𝓟 (f '' A)
⊢ (comap f l ⊓ 𝓟 A).NeBot

Tactic:
have : NeBot (l.comap f ⊓ 𝓟 A) :=
    comap_inf_principal_neBot_of_image_mem hl_nebot (le_principal_iff.mp hle)
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A : Set E
hA : IsCountablyCompact A
f : E → F
hf : Continuous[inst, inst_1] f
l : Filter F
hl_nebot : l.NeBot
hl_count : l.IsCountablyGenerated
hle : l ≤ 𝓟 (f '' A)
this : (comap f l ⊓ 𝓟 A).NeBot
obtain : ∀ (x : E) (hxA : x ∈ A) (hx : ClusterPt x (comap f l ⊓ 𝓟 A)), ∃ a ∈ f '' A, ClusterPt a l
⊢ ∃ a ∈ f '' A, ClusterPt a l

Tactic:
obtain ⟨x, hxA, hx⟩ := hA (f := l.comap f ⊓ 𝓟 A) inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A : Set E
hA : IsCountablyCompact A
f : E → F
hf : Continuous[inst, inst_1] f
l : Filter F
hl_nebot : l.NeBot
hl_count : l.IsCountablyGenerated
hle : l ≤ 𝓟 (f '' A)
this : (comap f l ⊓ 𝓟 A).NeBot
x : E
hxA : x ∈ A
hx : ClusterPt x (comap f l ⊓ 𝓟 A)
⊢ (𝓝 x ⊓ comap f l).NeBot

Tactic:
have := (hx.mono inf_le_left).neBot
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A : Set E
hA : IsCountablyCompact A
f : E → F
hf : Continuous[inst, inst_1] f
l : Filter F
hl_nebot : l.NeBot
hl_count : l.IsCountablyGenerated
hle : l ≤ 𝓟 (f '' A)
this_1 : (comap f l ⊓ 𝓟 A).NeBot
x : E
hxA : x ∈ A
hx : ClusterPt x (comap f l ⊓ 𝓟 A)
this : (𝓝 x ⊓ comap f l).NeBot
⊢ ∃ a ∈ f '' A, ClusterPt a l

Tactic:
⟨f x, mem_image_of_mem f hxA, (hf.continuousAt.inf tendsto_comap).neBot⟩

Premises used: Filter.tendsto_comap, Continuous.continuousAt, Set.mem_image_of_mem, And.intro, Exists.intro, Filter.Tendsto.neBot, Filter.Tendsto.inf
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A : Set E
hA : IsCountablyCompact A
f : E → F
hf : Continuous[inst, inst_1] f
l : Filter F
hl_nebot : l.NeBot
hl_count : l.IsCountablyGenerated
hle : l ≤ 𝓟 (f '' A)
this_1 : (comap f l ⊓ 𝓟 A).NeBot
x : E
hxA : x ∈ A
hx : ClusterPt x (comap f l ⊓ 𝓟 A)
this : (𝓝 x ⊓ comap f l).NeBot
⊢ ∃ a ∈ f '' A, ClusterPt a l

Tactic:
exact ⟨f x, mem_image_of_mem f hxA, (hf.continuousAt.inf tendsto_comap).neBot⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A : Set E
f : E → F
hf : IsInducing f
⊢ IsCountablyCompact A ↔ IsCountablyCompact (f '' A)

Tactic:
⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot Fc F_le => ?_⟩

Premises used: IsCountablyCompact.image, Iff.intro, Topology.IsInducing.continuous
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A : Set E
f : E → F
hf : IsInducing f
refine :
  ∀ (hs : IsCountablyCompact (f '' A)) (F : Filter E) (F_ne_bot : F.NeBot) (Fc : F.IsCountablyGenerated)
    (F_le : F ≤ 𝓟 A), ∃ a ∈ A, ClusterPt a F
⊢ IsCountablyCompact A ↔ IsCountablyCompact (f '' A)

Tactic:
refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot Fc F_le => ?_⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
F_1 : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F_1
A : Set E
f : E → F_1
hf : IsInducing f
hs : IsCountablyCompact (f '' A)
F : Filter E
F_ne_bot : F.NeBot
Fc : F.IsCountablyGenerated
F_le : F ≤ 𝓟 A
obtain : ∀ (x : E) (x_in : x ∈ A) (hx : ClusterPt (f x) (map f F)), ∃ a ∈ A, ClusterPt a F
⊢ ∃ a ∈ A, ClusterPt a F

Tactic:
obtain ⟨_, ⟨x, x_in : x ∈ A, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)

Premises used: Filter.map_mono, LE.le.trans_eq, Filter.map_principal, rfl
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
F_1 : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F_1
A : Set E
f : E → F_1
hf : IsInducing f
hs : IsCountablyCompact (f '' A)
F : Filter E
F_ne_bot : F.NeBot
Fc : F.IsCountablyGenerated
F_le : F ≤ 𝓟 A
x : E
x_in : x ∈ A
hx : ClusterPt (f x) (map f F)
⊢ ∃ a ∈ A, ClusterPt a F

Tactic:
⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩

Premises used: And.intro, Exists.intro, Iff.mp, Topology.IsInducing.mapClusterPt_iff
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
F_1 : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F_1
A : Set E
f : E → F_1
hf : IsInducing f
hs : IsCountablyCompact (f '' A)
F : Filter E
F_ne_bot : F.NeBot
Fc : F.IsCountablyGenerated
F_le : F ≤ 𝓟 A
x : E
x_in : x ∈ A
hx : ClusterPt (f x) (map f F)
⊢ ∃ a ∈ A, ClusterPt a F

Tactic:
exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A : Set E
f : E → F
hf : IsEmbedding f
⊢ IsCountablyCompact A ↔ IsCountablyCompact (f '' A)

Tactic:
hf.isInducing.isCountablyCompact_iff

Premises used: Topology.IsEmbedding.isInducing, Topology.IsInducing.isCountablyCompact_iff
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
p : E → Prop
A : Set { x : E // p x }
⊢ IsCountablyCompact A ↔ IsCountablyCompact (val (p := fun (x : E) ↦ p x) '' A)

Tactic:
IsEmbedding.subtypeVal.isCountablyCompact_iff

Premises used: Topology.IsEmbedding.isCountablyCompact_iff, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
rw :
  IsCountablyCompact A ↔
    IsCountablyCompact.{u_2} (E := E) (image (α := { x : E // x ∈ A }) (Subtype.val (p := fun (x : E) ↦ x ∈ A)) univ)
rw₁ :
  IsCountablyCompact A ↔
    IsCountablyCompact.{u_2} (E := E) (range (ι := { x : E // x ∈ A }) (Subtype.val (p := fun (x : E) ↦ x ∈ A)))
rw₂ rw₃ : IsCountablyCompact A ↔ IsCountablyCompact A
⊢ IsCountablyCompact A ↔ IsCountablyCompact.{u_2} (E := (↑A : Type u_2)) univ

Tactic:
rw [Subtype.isCountablyCompact_iff, image_univ, Subtype.range_coe]

Premises used: Set.image_univ, Subtype.range_coe, Subtype.isCountablyCompact_iff
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
⊢ IsCountablyCompact.{u_2} (E := E) univ ↔ CountablyCompactSpace E

Tactic:
⟨fun h => ⟨h⟩, fun h => h.1⟩

Premises used: CountablyCompactSpace.isCountablyCompact_univ, Iff.intro, CountablyCompactSpace.mk
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
⊢ IsCountablyCompact A ↔ CountablyCompactSpace.{u_2} (↑A : Type u_2)

Tactic:
isCountablyCompact_iff_isCountablyCompact_univ.trans isCountablyCompact_univ_iff

Premises used: Iff.trans, isCountablyCompact_univ_iff, isCountablyCompact_iff_isCountablyCompact_univ
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
by_contra : ∀ (this : ¬SeqCompactSpace E), False
⊢ SeqCompactSpace E

Tactic:
by_contra
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
this : ¬SeqCompactSpace E
⊢ ∃ (x : ℕ → E), ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)

Tactic:
simp only [seqCompactSpace_iff, IsSeqCompact, mem_univ, not_forall,
    true_and, not_exists, not_and, exists_const] at this

Premises used: not_exists, exists_const, Set.mem_univ, IsSeqCompact, not_and, Classical.not_forall, seqCompactSpace_iff, true_and
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
this : ∃ (x : ℕ → E), ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
obtain : ∀ (x : ℕ → E) (hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)), False
⊢ False

Tactic:
obtain ⟨x, hx⟩ := this
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
⊢ IsCountablyCompact A

Tactic:
have : IsCountablyCompact A :=
    (isClosed_iUnion_closure_singleton_of_not_tendsto hx).isCountablyCompact
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this : IsCountablyCompact A
⊢ ∃ a ∈ A, MapClusterPt a atTop x

Tactic:
isCountablyCompact_iff_seq_clusterPt.1 this _ (.of_forall fun n => ?_)

Premises used: Filter.Eventually.of_forall, Iff.mp, isCountablyCompact_iff_seq_clusterPt
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this : IsCountablyCompact A
refine : ∀ (n : ℕ), x n ∈ A
⊢ ∃ a ∈ A, MapClusterPt a atTop x

Tactic:
refine isCountablyCompact_iff_seq_clusterPt.1 this _ (.of_forall fun n => ?_)

Premises used: Filter.Eventually.of_forall, Iff.mp, isCountablyCompact_iff_seq_clusterPt
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this : IsCountablyCompact A
n : ℕ
⊢ x n ∈ A

Tactic:
mem_iUnion_of_mem n <| subset_closure <| mem_singleton (x n)

Premises used: Set.mem_singleton, Set.Mem, subset_closure, Set.mem_iUnion_of_mem
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this : IsCountablyCompact A
n : ℕ
⊢ x n ∈ A

Tactic:
exact mem_iUnion_of_mem n <| subset_closure <| mem_singleton (x n)

Premises used: Set.mem_singleton, subset_closure, Set.mem_iUnion_of_mem
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this : IsCountablyCompact A
obtain : ∀ (a : E) (ha : a ∈ A ∧ MapClusterPt a atTop x), False
⊢ False

Tactic:
obtain ⟨a, ha⟩ : ∃ a ∈ A, MapClusterPt a atTop x := by
    refine isCountablyCompact_iff_seq_clusterPt.1 this _ (.of_forall fun n => ?_)
    exact mem_iUnion_of_mem n <| subset_closure <| mem_singleton (x n)
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
by_contra! : ∀ (this : ∀ (k : ℕ), ∃ n > k, Membership.mem (γ := Set E) (closure[inst] {x n}) a), False
⊢ ∃ (k : ℕ), ∀ n > k, a ∉ closure[inst] {x n}

Tactic:
by_contra!
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this_1 : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
this : ∀ (k : ℕ), ∃ n > k, Membership.mem (γ := Set E) (closure[inst] {x n}) a
obtain :
  ∀ (φ : ℕ → ℕ) (hφ1 : StrictMono φ) (hφ2 : ∀ (n : ℕ), Membership.mem (γ := Set E) (closure[inst] {x (φ n)}) a), False
⊢ False

Tactic:
obtain ⟨φ, hφ1, hφ2⟩ := Nat.exists_strictMono_subsequence this

Premises used: Nat.exists_strictMono_subsequence
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this_1 : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
this : ∀ (k : ℕ), ∃ n > k, Membership.mem (γ := Set E) (closure[inst] {x n}) a
φ : ℕ → ℕ
hφ1 : StrictMono φ
hφ2 : ∀ (n : ℕ), Membership.mem (γ := Set E) (closure[inst] {x (φ n)}) a
⊢ False

Tactic:
hx a φ hφ1 (tendsto_atTop_nhds.2 fun U ha hUo => ⟨0, fun n _ => ?_⟩)

Premises used: Iff.mpr, Exists.intro, tendsto_atTop_nhds, OfNat.ofNat
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this_1 : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
this : ∀ (k : ℕ), ∃ n > k, Membership.mem (γ := Set E) (closure[inst] {x n}) a
φ : ℕ → ℕ
hφ1 : StrictMono φ
hφ2 : ∀ (n : ℕ), Membership.mem (γ := Set E) (closure[inst] {x (φ n)}) a
refine : ∀ (U : Set E) (ha : a ∈ U) (hUo : IsOpen[inst] U) (n : ℕ), 0 ≤ n → (x ∘ φ) n ∈ U
⊢ False

Tactic:
refine hx a φ hφ1 (tendsto_atTop_nhds.2 fun U ha hUo => ⟨0, fun n _ => ?_⟩)

Premises used: Iff.mpr, Exists.intro, tendsto_atTop_nhds, OfNat.ofNat
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this_1 : IsCountablyCompact A
a : E
ha_1 : a ∈ A ∧ MapClusterPt a atTop x
this : ∀ (k : ℕ), ∃ n > k, Membership.mem (γ := Set E) (closure[inst] {x n}) a
φ : ℕ → ℕ
hφ1 : StrictMono φ
hφ2 : ∀ (n : ℕ), Membership.mem (γ := Set E) (closure[inst] {x (φ n)}) a
U : Set E
ha : a ∈ U
hUo : IsOpen[inst] U
n : ℕ
h : 0 ≤ n
⊢ (x ∘ φ) n ∈ U

Tactic:
simpa using mem_closure_iff.1 (hφ2 n) U hUo ha

Premises used: mem_closure_iff, Iff.mp
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
obtain : ∀ (k : ℕ) (hk : ∀ n > k, a ∉ closure[inst] {x n}), False
⊢ False

Tactic:
obtain ⟨k, hk⟩ : ∃ k, ∀ n > k, a ∉ closure {x n} := by
    by_contra!
    obtain ⟨φ, hφ1, hφ2⟩ := Nat.exists_strictMono_subsequence this
    refine hx a φ hφ1 (tendsto_atTop_nhds.2 fun U ha hUo => ⟨0, fun n _ => ?_⟩)
    simpa using mem_closure_iff.1 (hφ2 n) U hUo ha
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst] {x n}
⊢ a ∉ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}

Tactic:
simpa [← iUnion_ge_eq_iUnion_nat_add (fun n => closure {x n}) (k + 1)] using
      fun i hi => hk i (Nat.lt_of_lt_of_eq hi rfl)

Premises used: Nat.lt_of_lt_of_eq, Set.iUnion_ge_eq_iUnion_nat_add, closure, HAdd.hAdd, Singleton.singleton, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst] {x n}
⊢ a ∉ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}

Tactic:
have : a ∉ ⋃ i, closure {x (i + (k + 1))} := by
    simpa [← iUnion_ge_eq_iUnion_nat_add (fun n => closure {x n}) (k + 1)] using
      fun i hi => hk i (Nat.lt_of_lt_of_eq hi rfl)
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this_1 : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst] {x n}
this : a ∉ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}
apply : Membership.mem (γ := Set E) (⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}) a
⊢ False

Tactic:
apply this
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this_1 : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst] {x n}
this : a ∉ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}
suffices : closure[inst] (x '' Ici (k + 1)) ⊆ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}
⊢ Membership.mem (γ := Set E) (⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}) a

Tactic:
suffices h : closure (x '' Ici (k + 1)) ⊆ ⋃ i, closure {x (i + (k + 1))} from
    h <| mapClusterPt_atTop_iff_forall_mem_closure.1 ha.2 (k + 1)
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this_1 : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst] {x n}
this : a ∉ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}
⊢ closure[inst] (x '' Ici (k + 1)) ⊆ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}

Tactic:
(IsClosed.closure_subset_iff
    (isClosed_iUnion_closure_singleton_of_not_tendsto fun l φ hφ => ?_)).2 ?_

Premises used: Iff.mpr, IsClosed.closure_subset_iff, isClosed_iUnion_closure_singleton_of_not_tendsto
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this_1 : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst] {x n}
this : a ∉ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}
refine_1 : ∀ (l : E) (φ : ℕ → ℕ) (hφ : StrictMono φ), ¬Tendsto ((fun (i : ℕ) ↦ x (i + (k + 1))) ∘ φ) atTop (𝓝 l)
refine_2 : x '' Ici (k + 1) ⊆ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}
⊢ closure[inst] (x '' Ici (k + 1)) ⊆ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}

Tactic:
refine (IsClosed.closure_subset_iff
    (isClosed_iUnion_closure_singleton_of_not_tendsto fun l φ hφ => ?_)).2 ?_

Premises used: Iff.mpr, IsClosed.closure_subset_iff, isClosed_iUnion_closure_singleton_of_not_tendsto
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this_1 : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst] {x n}
this : a ∉ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}
l : E
φ : ℕ → ℕ
hφ : StrictMono φ
⊢ ¬Tendsto ((fun (i : ℕ) ↦ x (i + (k + 1))) ∘ φ) atTop (𝓝 l)

Tactic:
hx l _ ((strictMono_id.add_const _).comp hφ)

Premises used: strictMono_id, StrictMono.add_const, StrictMono.comp
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this_1 : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst] {x n}
this : a ∉ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}
l : E
φ : ℕ → ℕ
hφ : StrictMono φ
⊢ ¬Tendsto ((fun (i : ℕ) ↦ x (i + (k + 1))) ∘ φ) atTop (𝓝 l)

Tactic:
exact hx l _ ((strictMono_id.add_const _).comp hφ)

Premises used: strictMono_id, StrictMono.add_const, StrictMono.comp
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
F : Type u_3
inst : TopologicalSpace E
inst_1 : TopologicalSpace F
A_1 B : Set E
inst_2 : SequentialSpace E
inst_3 : CountablyCompactSpace E
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ (i : ℕ), closure[inst] {x i}
this_1 : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst] {x n}
this : a ∉ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}
refine_2 : Subset.{u_2} (α := Set E) (⋃ (i : ℕ), {x (i + (k + 1))}) (⋃ (i : ℕ), closure[inst] {x (i + (k + 1))})
⊢ x '' Ici (k + 1) ⊆ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}

Tactic:
simp only [image_eq_iUnion, mem_Ici, iUnion_ge_eq_iUnion_nat_add _ (k + 1)]

Premises used: Set.image_eq_iUnion, Set.iUnion_ge_eq_iUnion_nat_add, HAdd.hAdd, Set.mem_Ici, OfNat.ofNat