awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))}
⊢ Subset.{u_2} (α := Set E) (⋃ (i : ℕ), {x (i + (k + 1))}) (⋃ (i : ℕ), closure[inst] {x (i + (k + 1))})

Tactic:
iUnion_mono fun i => subset_closure

Premises used: subset_closure, Set.iUnion_mono
-- 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))}
⊢ Subset.{u_2} (α := Set E) (⋃ (i : ℕ), {x (i + (k + 1))}) (⋃ (i : ℕ), closure[inst] {x (i + (k + 1))})

Tactic:
exact iUnion_mono fun i => subset_closure

Premises used: subset_closure, Set.iUnion_mono
-- 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
hA : IsSeqCompact A
x : ℕ → F
hx : ∀ (n : ℕ), x n ∈ f '' A
choose :
  ∀ (y : (n : ℕ) → E) (hy : ∀ (n : ℕ), y n ∈ A ∧ f (y n) = x n),
    ∃ a ∈ f '' A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
⊢ ∃ a ∈ f '' A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
choose y hy using 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
hA : IsSeqCompact A
x : ℕ → F
y : (n : ℕ) → E
hy : ∀ (n : ℕ), y n ∈ A ∧ f (y n) = x n
obtain :
  ∀ (a : E) (ha : a ∈ A) (φ : ℕ → ℕ) (hφ : StrictMono φ ∧ Tendsto (y ∘ φ) atTop (𝓝 a)),
    ∃ a ∈ f '' A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
⊢ ∃ a ∈ f '' A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
obtain ⟨a, ha, ⟨φ, hφ⟩⟩ := hA (fun n => (hy n).1)

Premises used: And.left
-- 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
hA : IsSeqCompact A
x : ℕ → F
y : (n : ℕ) → E
hy : ∀ (n : ℕ), y n ∈ A ∧ f (y n) = x n
a : E
ha : a ∈ A
φ : ℕ → ℕ
hφ : StrictMono φ ∧ Tendsto (y ∘ φ) atTop (𝓝 a)
⊢ ∃ a ∈ f '' A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
⟨f a, mem_image_of_mem f ha, φ, hφ.1, ?_⟩

Premises used: And.left, Set.mem_image_of_mem, And.intro, Exists.intro
-- 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
hA : IsSeqCompact A
x : ℕ → F
y : (n : ℕ) → E
hy : ∀ (n : ℕ), y n ∈ A ∧ f (y n) = x n
a : E
ha : a ∈ A
φ : ℕ → ℕ
hφ : StrictMono φ ∧ Tendsto (y ∘ φ) atTop (𝓝 a)
refine : Tendsto (x ∘ φ) atTop (𝓝 (f a))
⊢ ∃ a ∈ f '' A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
refine ⟨f a, mem_image_of_mem f ha, φ, hφ.1, ?_⟩
-- 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
hA : IsSeqCompact A
x : ℕ → F
y : (n : ℕ) → E
hy : ∀ (n : ℕ), y n ∈ A ∧ f (y n) = x n
a : E
ha : a ∈ A
φ : ℕ → ℕ
hφ : StrictMono φ ∧ Tendsto (y ∘ φ) atTop (𝓝 a)
suffices : f ∘ y ∘ φ = x ∘ φ
⊢ Tendsto (x ∘ φ) atTop (𝓝 (f a))

Tactic:
suffices f ∘ y ∘ φ = x ∘ φ from this ▸ (hf.continuous.tendsto a).comp hφ.2
-- 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
hA : IsSeqCompact A
x : ℕ → F
y : (n : ℕ) → E
hy : ∀ (n : ℕ), y n ∈ A ∧ f (y n) = x n
a : E
ha : a ∈ A
φ : ℕ → ℕ
hφ : StrictMono φ ∧ Tendsto (y ∘ φ) atTop (𝓝 a)
⊢ f ∘ y ∘ φ = x ∘ φ

Tactic:
grind
-- 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
hA : IsSeqCompact (f '' A)
x : ℕ → E
hx : ∀ (n : ℕ), x n ∈ A
obtain :
  ∀ (fa : F) (hfa : fa ∈ f '' A) (φ : ℕ → ℕ) (hφ : StrictMono φ ∧ Tendsto ((fun (n : ℕ) ↦ f (x n)) ∘ φ) atTop (𝓝 fa)),
    ∃ a ∈ A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
⊢ ∃ a ∈ A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
obtain ⟨fa, hfa, ⟨φ, hφ⟩⟩ := hA (fun n => mem_image_of_mem f (hx n))

Premises used: Set.mem_image_of_mem
-- 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
hA : IsSeqCompact (f '' A)
x : ℕ → E
hx : ∀ (n : ℕ), x n ∈ A
fa : F
hfa : fa ∈ f '' A
φ : ℕ → ℕ
hφ : StrictMono φ ∧ Tendsto ((fun (n : ℕ) ↦ f (x n)) ∘ φ) atTop (𝓝 fa)
choose : ∀ (a : E) (ha : a ∈ A ∧ f a = fa), ∃ a ∈ A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
⊢ ∃ a ∈ A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
choose a ha using hfa
-- 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
hA : IsSeqCompact (f '' A)
x : ℕ → E
hx : ∀ (n : ℕ), x n ∈ A
fa : F
φ : ℕ → ℕ
hφ : StrictMono φ ∧ Tendsto ((fun (n : ℕ) ↦ f (x n)) ∘ φ) atTop (𝓝 fa)
a : E
ha : a ∈ A ∧ f a = fa
⊢ ∃ a ∈ A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
⟨a, ha.1, φ, hφ.1, hf.tendsto_nhds_iff.2 (ha.2 ▸ hφ.2)⟩

Premises used: Iff.mpr, Eq.rec, Topology.IsEmbedding.tendsto_nhds_iff, And.right, And.left, And.intro, Exists.intro, Eq.symm
-- 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
hA : IsSeqCompact (f '' A)
x : ℕ → E
hx : ∀ (n : ℕ), x n ∈ A
fa : F
φ : ℕ → ℕ
hφ : StrictMono φ ∧ Tendsto ((fun (n : ℕ) ↦ f (x n)) ∘ φ) atTop (𝓝 fa)
a : E
ha : a ∈ A ∧ f a = fa
⊢ ∃ a ∈ A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Tactic:
exact ⟨a, ha.1, φ, hφ.1, hf.tendsto_nhds_iff.2 (ha.2 ▸ hφ.2)⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
p : E → Prop
A : Set { x : E // p x }
⊢ IsSeqCompact A ↔ IsSeqCompact (val (p := fun (x : E) ↦ p x) '' A)

Tactic:
IsEmbedding.subtypeVal.isSeqCompact_iff

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

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

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

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

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

Tactic:
isSeqCompact_iff_isSeqCompact_univ.trans isSeqCompact_univ_iff

Premises used: isSeqCompact_univ_iff, Iff.trans, isSeqCompact_iff_isSeqCompact_univ
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
inst_1 : FirstCountableTopology E
hA : IsCountablyCompact A
⊢ IsSeqCompact A

Tactic:
have : CountablyCompactSpace A := isCountablyCompact_iff_countablyCompactSpace.1 hA
  isSeqCompact_iff_seqCompactSpace.2 inferInstance

Premises used: Iff.mpr, inferInstance, isCountablyCompact_iff_countablyCompactSpace, isSeqCompact_iff_seqCompactSpace, Iff.mp
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
inst_1 : FirstCountableTopology E
⊢ IsCountablyCompact A ↔ IsSeqCompact A

Tactic:
⟨fun h => h.isSeqCompact, fun h => h.isCountablyCompact⟩

Premises used: IsCountablyCompact.isSeqCompact, Iff.intro, IsSeqCompact.isCountablyCompact
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
f : ℕ ↪ (↑B : Type u_2) := Set.Infinite.natEmbedding B hB
x : ℕ → E :=
  Function.comp (β := (↑B : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ B)) (⇑f : (a : ℕ) → (↑B : Type u_2))
⊢ Function.Injective x

Tactic:
have hx_inj : Function.Injective x := Subtype.val_injective.comp f.injective
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
f : ℕ ↪ (↑B : Type u_2) := Set.Infinite.natEmbedding B hB
x : ℕ → E :=
  Function.comp (β := (↑B : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ B)) (⇑f : (a : ℕ) → (↑B : Type u_2))
hx_inj : Function.Injective x
obtain : ∀ (a : E) (haA : a ∈ A) (hac : MapClusterPt a atTop x), ∃ a ∈ A, AccPt a (𝓟 B)
⊢ ∃ a ∈ A, AccPt a (𝓟 B)

Tactic:
obtain ⟨a, haA, hac⟩ :=
    IsCountablyCompact.seq_clusterPt hA x (Eventually.of_forall (fun n => hBA (f n).2))

Premises used: Filter.Eventually.of_forall, IsCountablyCompact.seq_clusterPt, DFunLike.coe, Subtype.property
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
f : ℕ ↪ (↑B : Type u_2) := Set.Infinite.natEmbedding B hB
x : ℕ → E :=
  Function.comp (β := (↑B : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ B)) (⇑f : (a : ℕ) → (↑B : Type u_2))
hx_inj : Function.Injective x
a : E
haA : a ∈ A
hac : MapClusterPt a atTop x
⊢ ∃ a ∈ A, AccPt a (𝓟 B)

Tactic:
⟨a, haA, accPt_iff_clusterPt.2 <| ClusterPt.mono hac <| le_inf ?_ ?_⟩

Premises used: Iff.mpr, ClusterPt.mono, le_inf, And.intro, Exists.intro, accPt_iff_clusterPt
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
f : ℕ ↪ (↑B : Type u_2) := Set.Infinite.natEmbedding B hB
x : ℕ → E :=
  Function.comp (β := (↑B : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ B)) (⇑f : (a : ℕ) → (↑B : Type u_2))
hx_inj : Function.Injective x
a : E
haA : a ∈ A
hac : MapClusterPt a atTop x
refine_1 : map x atTop ≤ 𝓟 {a}ᶜ
refine_2 : map x atTop ≤ 𝓟 B
⊢ ∃ a ∈ A, AccPt a (𝓟 B)

Tactic:
refine ⟨a, haA, accPt_iff_clusterPt.2 <| ClusterPt.mono hac <| le_inf ?_ ?_⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
f : ℕ ↪ (↑B : Type u_2) := Set.Infinite.natEmbedding B hB
x : ℕ → E :=
  Function.comp (β := (↑B : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ B)) (⇑f : (a : ℕ) → (↑B : Type u_2))
hx_inj : Function.Injective x
a : E
haA : a ∈ A
hac : MapClusterPt a atTop x
⊢ map x atTop ≤ 𝓟 {a}ᶜ

Tactic:
tendsto_principal.mpr <| Nat.cofinite_eq_atTop ▸
      ((Set.finite_singleton a).preimage hx_inj.injOn).compl_mem_cofinite

Premises used: Iff.mpr, Function.Injective.injOn, Eq.rec, Filter.tendsto_principal, Filter.Tendsto, Set.Finite.compl_mem_cofinite, Nat.cofinite_eq_atTop, Set.finite_singleton, Set.Finite.preimage
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
f : ℕ ↪ (↑B : Type u_2) := Set.Infinite.natEmbedding B hB
x : ℕ → E :=
  Function.comp (β := (↑B : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ B)) (⇑f : (a : ℕ) → (↑B : Type u_2))
hx_inj : Function.Injective x
a : E
haA : a ∈ A
hac : MapClusterPt a atTop x
⊢ map x atTop ≤ 𝓟 {a}ᶜ

Tactic:
exact tendsto_principal.mpr <| Nat.cofinite_eq_atTop ▸
      ((Set.finite_singleton a).preimage hx_inj.injOn).compl_mem_cofinite

Premises used: Iff.mpr, Filter.tendsto_principal
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
f : ℕ ↪ (↑B : Type u_2) := Set.Infinite.natEmbedding B hB
x : ℕ → E :=
  Function.comp (β := (↑B : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ B)) (⇑f : (a : ℕ) → (↑B : Type u_2))
hx_inj : Function.Injective x
a : E
haA : a ∈ A
hac : MapClusterPt a atTop x
⊢ map x atTop ≤ 𝓟 B

Tactic:
tendsto_principal.mpr <| Eventually.of_forall fun n => (f n).2

Premises used: Iff.mpr, Filter.Eventually.of_forall, Filter.tendsto_principal, Filter.Tendsto, DFunLike.coe, Subtype.property
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
f : ℕ ↪ (↑B : Type u_2) := Set.Infinite.natEmbedding B hB
x : ℕ → E :=
  Function.comp (β := (↑B : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ B)) (⇑f : (a : ℕ) → (↑B : Type u_2))
hx_inj : Function.Injective x
a : E
haA : a ∈ A
hac : MapClusterPt a atTop x
⊢ map x atTop ≤ 𝓟 B

Tactic:
exact tendsto_principal.mpr <| Eventually.of_forall fun n => (f n).2

Premises used: Iff.mpr, Filter.Eventually.of_forall, Filter.tendsto_principal, DFunLike.coe, Subtype.property
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
⊢ IsCountablyCompact A

Tactic:
IsCountablyCompact.of_seq_clusterPt fun x hx => ?_

Premises used: IsCountablyCompact.of_seq_clusterPt
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
refine : ∀ (x : ℕ → E) (hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A), ∃ a ∈ A, MapClusterPt a atTop x
⊢ IsCountablyCompact A

Tactic:
refine IsCountablyCompact.of_seq_clusterPt fun x hx => ?_

Premises used: IsCountablyCompact.of_seq_clusterPt
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
rw : ∀ (hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A), ∃ a ∈ A, MapClusterPt a cofinite x
⊢ ∃ a ∈ A, MapClusterPt a atTop x

Tactic:
rw [← Nat.cofinite_eq_atTop] at hx ⊢

Premises used: Nat.cofinite_eq_atTop
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
pos : ∀ (hfin : (range x).Finite), ∃ a ∈ A, MapClusterPt a cofinite x
neg : ∀ (hfin : (range x).Infinite), ∃ a ∈ A, MapClusterPt a cofinite x
⊢ ∃ a ∈ A, MapClusterPt a cofinite x

Tactic:
by_cases! hfin : (Set.range x).Finite

Premises used: Set.Finite, Set.range
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Finite
this : ∃ a ∈ range x ∩ A, MapClusterPt a cofinite x
⊢ ∃ a ∈ A, MapClusterPt a cofinite x

Tactic:
aesop
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Finite
pos : ∃ a ∈ range x ∩ A, MapClusterPt a cofinite x
⊢ ∃ a ∈ A, MapClusterPt a cofinite x

Tactic:
suffices ∃ a ∈ range x ∩ A, MapClusterPt a cofinite x by aesop
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Finite
⊢ ∀ᶠ (x_1 : ℕ) in cofinite, x x_1 ∈ A → x x_1 ∈ range x ∩ A

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Finite
⊢ ∃ a ∈ range x ∩ A, MapClusterPt a cofinite x

Tactic:
exact hfin.inter_of_left A |>.isCompact.exists_mapClusterPt_of_frequently <|
        hx.frequently.mp (by simp)

Premises used: Set.Finite.inter_of_left, Set.Finite.isCompact, IsCompact.exists_mapClusterPt_of_frequently, Filter.Eventually.frequently, Filter.Frequently.mp
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
⊢ Set.Finite (α := ℕ) {a : ℕ | x a ∉ A}

Tactic:
rw [eventually_iff, mem_cofinite, compl_setOf] at hx

Premises used: Filter.mem_cofinite, Filter.eventually_iff, Set.compl_setOf
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
hx₁ : Set.Finite (α := ℕ) {a : ℕ | x a ∉ A}
⊢ (range x).Infinite

Tactic:
rw [eventually_iff, mem_cofinite, compl_setOf] at hx

Premises used: Filter.mem_cofinite, Filter.eventually_iff, Set.compl_setOf
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : Set.Finite (α := ℕ) {a : ℕ | x a ∉ A}
hfin : (range x).Infinite
⊢ range x \ A ⊆ x '' {a : ℕ | x a ∉ A}

Tactic:
grind
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : Set.Finite (α := ℕ) {a : ℕ | x a ∉ A}
hfin : (range x).Infinite
⊢ (range x ∩ A).Infinite

Tactic:
exact hfin.inter_of_finite_diff (hx.image x |>.subset (by grind))

Premises used: Set.Finite.subset, Set.Finite.image, Set.Infinite.inter_of_finite_diff
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
neg : ∀ (a : E) (haA : a ∈ A) (hacc : AccPt a (𝓟 (range x ∩ A))), ∃ a ∈ A, MapClusterPt a cofinite x
⊢ ∃ a ∈ A, MapClusterPt a cofinite x

Tactic:
obtain ⟨a, haA, hacc⟩ := h (Set.range x ∩ A) inter_subset_right <| by
        rw [eventually_iff, mem_cofinite, compl_setOf] at hx
        exact hfin.inter_of_finite_diff (hx.image x |>.subset (by grind))

Premises used: Inter.inter, Set.range, Set.inter_subset_right
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
a : E
haA : a ∈ A
hacc : AccPt a (𝓟 (range x ∩ A))
⊢ ∃ a ∈ A, MapClusterPt a cofinite x

Tactic:
⟨a, haA, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
a : E
haA : a ∈ A
hacc : AccPt a (𝓟 (range x ∩ A))
neg : MapClusterPt a cofinite x
⊢ ∃ a ∈ A, MapClusterPt a cofinite x

Tactic:
refine ⟨a, haA, ?_⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
a : E
haA : a ∈ A
hacc : AccPt a (𝓟 (range x ∩ A))
neg : ∀ s ∈ 𝓝 a, Set.Infinite (α := ℕ) {a : ℕ | x a ∈ s}
⊢ MapClusterPt a cofinite x

Tactic:
simp_rw [mapClusterPt_iff_frequently, frequently_cofinite_iff_infinite]

Premises used: Filter.frequently_cofinite_iff_infinite, mapClusterPt_iff_frequently
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
a : E
haA : a ∈ A
hacc : AccPt a (𝓟 (range x ∩ A))
s : Set E
hs : s ∈ 𝓝 a
⊢ s ∩ (range x ∩ A) ⊆ x '' {a : ℕ | x a ∈ s}

Tactic:
grind
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
inst_1 : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
a : E
haA : a ∈ A
hacc : AccPt a (𝓟 (range x ∩ A))
⊢ ∀ s ∈ 𝓝 a, Set.Infinite (α := ℕ) {a : ℕ | x a ∈ s}

Tactic:
exact fun s hs ↦ Infinite.of_accPt (hacc.nhds_inter hs) |>.mono (by grind) |>.of_image x

Premises used: Set.Infinite.mono, Set.Infinite.of_image, Set.Infinite.of_accPt, AccPt.nhds_inter
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
hl : IsLindelof A
⊢ IsCompact A

Tactic:
isCompact_of_finite_subcover fun {ι} U hUo hAU => ?_

Premises used: isCompact_of_finite_subcover
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
hl : IsLindelof A
refine :
  ∀ {ι : Type u_2} (U : ι → Set E) (hUo : ∀ (i : ι), IsOpen[inst] (U i)) (hAU : A ⊆ ⋃ (i : ι), U i),
    ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i
⊢ IsCompact A

Tactic:
refine isCompact_of_finite_subcover fun {ι} U hUo hAU => ?_

Premises used: isCompact_of_finite_subcover
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
hl : IsLindelof A
ι : Type u_2
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hAU : A ⊆ ⋃ (i : ι), U i
pos : ∀ (h : Nonempty ι), ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i
neg : ∀ (h : IsEmpty ι), ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i

Tactic:
by_cases! h : Nonempty ι

Premises used: Nonempty
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
hl : IsLindelof A
ι : Type u_2
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hAU : A ⊆ ⋃ (i : ι), U i
h : Nonempty ι
pos : ∀ (f : ℕ → ι) (hf : A ⊆ ⋃ (n : ℕ), U (f n)), ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i
⊢ ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i

Tactic:
obtain ⟨f, hf⟩ := hl.indexed_countable_subcover U hUo hAU

Premises used: IsLindelof.indexed_countable_subcover