awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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)
⊢ IsCountablyCompact A ↔ IsCountablyCompact.{u_2} (E := (↑A : Type u_2)) univ
have rw₁ : IsCountablyCompact A ↔
  IsCountablyCompact.{u_2} (E := E) (range (ι := { x : E // x ∈ A }) (Subtype.val (p := fun (x : E) ↦ x ∈ A)))
Tactic: rw [Subtype.isCountablyCompact_iff, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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)))
⊢ IsCountablyCompact A ↔ IsCountablyCompact.{u_2} (E := (↑A : Type u_2)) univ
have rw₂ : IsCountablyCompact A ↔ IsCountablyCompact A
Tactic: rw [Subtype.isCountablyCompact_iff, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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
⊢ SeqCompactSpace E
have by_contra : ∀ (this : ¬SeqCompactSpace E), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
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
⊢ False
have this₁ : ∃ (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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)
⊢ False
have obtain : ∀ (x : ℕ → E) (hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)), False
Tactic: obtain ⟨x, hx⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
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}
⊢ False
have this : IsCountablyCompact A
Tactic: have : IsCountablyCompact A :=
    (isClosed_iUnion_closure_singleton_of_not_tendsto hx).isCountablyCompact
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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
have refine : ∀ (n : ℕ), x n ∈ A
Tactic: refine isCountablyCompact_iff_seq_clusterPt.1 this _ (.of_forall fun n => ?_)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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
⊢ False
have obtain : ∀ (a : E) (ha : a ∈ A ∧ MapClusterPt a atTop x), 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)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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 : ℕ), ∀ n > k, a ∉ closure[inst] {x n}
have by_contra! : ∀ (this : ∀ (k : ℕ), ∃ n > k, Membership.mem (γ := Set E) (closure[inst] {x n}) a), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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
⊢ False
have obtain : ∀ (φ : ℕ → ℕ) (hφ1 : StrictMono φ) (hφ2 : ∀ (n : ℕ), Membership.mem (γ := Set E) (closure[inst] {x (φ n)}) a), False
Tactic: obtain ⟨φ, hφ1, hφ2⟩ := Nat.exists_strictMono_subsequence this
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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
have refine : ∀ (U : Set E) (ha : a ∈ U) (hUo : IsOpen[inst] U) (n : ℕ), 0 ≤ n → (x ∘ φ) n ∈ U
Tactic: refine hx a φ hφ1 (tendsto_atTop_nhds.2 fun U ha hUo => ⟨0, fun n _ => ?_⟩)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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
⊢ False
have obtain : ∀ (k : ℕ) (hk : ∀ n > k, a ∉ closure[inst] {x n}), 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
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
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}
⊢ False
have this₁ : 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)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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))}
⊢ False
have apply : Membership.mem (γ := Set E) (⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}) a
Tactic: apply this
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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))}
⊢ Membership.mem (γ := Set E) (⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}) a
have suffices : closure[inst] (x '' Ici (k + 1)) ⊆ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}
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)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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))}
have refine_1 : ∀ (l : E) (φ : ℕ → ℕ) (hφ : StrictMono φ), ¬Tendsto ((fun (i : ℕ) ↦ x (i + (k + 1))) ∘ φ) atTop (𝓝 l)
Tactic: refine (IsClosed.closure_subset_iff
    (isClosed_iUnion_closure_singleton_of_not_tendsto fun l φ hφ => ?_)).2 ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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)
⊢ closure[inst] (x '' Ici (k + 1)) ⊆ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}
have refine_2 : 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 ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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))}
⊢ x '' Ici (k + 1) ⊆ ⋃ (i : ℕ), closure[inst] {x (i + (k + 1))}
have refine_2 : Subset.{u_2} (α := Set E) (⋃ (i : ℕ), {x (i + (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)]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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
⊢ ∃ a ∈ f '' A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
have choose : ∀ (y : (n : ℕ) → E) (hy : ∀ (n : ℕ), y n ∈ A ∧ f (y n) = x n),
  ∃ a ∈ f '' A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
Tactic: choose y hy using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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 ∈ f '' A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
have obtain : ∀ (a : E) (ha : a ∈ A) (φ : ℕ → ℕ) (hφ : StrictMono φ ∧ Tendsto (y ∘ φ) atTop (𝓝 a)),
  ∃ a ∈ f '' A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
Tactic: obtain ⟨a, ha, ⟨φ, hφ⟩⟩ := hA (fun n => (hy n).1)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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)
have refine : Tendsto (x ∘ φ) atTop (𝓝 (f a))
Tactic: refine ⟨f a, mem_image_of_mem f ha, φ, hφ.1, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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)
⊢ Tendsto (x ∘ φ) atTop (𝓝 (f a))
have suffices : f ∘ y ∘ φ = x ∘ φ
Tactic: suffices f ∘ y ∘ φ = x ∘ φ from this ▸ (hf.continuous.tendsto a).comp hφ.2
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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
⊢ ∃ a ∈ A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
have obtain : ∀ (fa : F) (hfa : fa ∈ f '' A) (φ : ℕ → ℕ) (hφ : StrictMono φ ∧ Tendsto ((fun (n : ℕ) ↦ f (x n)) ∘ φ) atTop (𝓝 fa)),
  ∃ a ∈ A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
Tactic: obtain ⟨fa, hfa, ⟨φ, hφ⟩⟩ := hA (fun n => mem_image_of_mem f (hx n))
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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)
⊢ ∃ a ∈ A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
have choose : ∀ (a : E) (ha : a ∈ A ∧ f a = fa), ∃ a ∈ A, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)
Tactic: choose a ha using hfa
Cleared hypotheses: hfa
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
⊢ IsSeqCompact A ↔ IsSeqCompact.{u_2} (X := (↑A : Type u_2)) univ
have rw : IsSeqCompact A ↔
  IsSeqCompact.{u_2} (X := E) (image (α := { x : E // x ∈ A }) (Subtype.val (p := fun (x : E) ↦ x ∈ A)) univ)
Tactic: rw [Subtype.isSeqCompact_iff, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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)
⊢ IsSeqCompact A ↔ IsSeqCompact.{u_2} (X := (↑A : Type u_2)) univ
have rw₁ : IsSeqCompact A ↔ IsSeqCompact.{u_2} (X := E) (range (ι := { x : E // x ∈ A }) (Subtype.val (p := fun (x : E) ↦ x ∈ A)))
Tactic: rw [Subtype.isSeqCompact_iff, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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)))
⊢ IsSeqCompact A ↔ IsSeqCompact.{u_2} (X := (↑A : Type u_2)) univ
have rw₂ : IsSeqCompact A ↔ IsSeqCompact A
Tactic: rw [Subtype.isSeqCompact_iff, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
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))
⊢ ∃ a ∈ A, AccPt a (𝓟 B)
have hx_inj : Function.Injective x
Tactic: have hx_inj : Function.Injective x := Subtype.val_injective.comp f.injective
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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 ∈ A, AccPt a (𝓟 B)
have obtain : ∀ (a : E) (haA : a ∈ A) (hac : MapClusterPt a atTop x), ∃ a ∈ A, AccPt a (𝓟 B)
Tactic: obtain ⟨a, haA, hac⟩ :=
    IsCountablyCompact.seq_clusterPt hA x (Eventually.of_forall (fun n => hBA (f n).2))
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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)
have refine_1 : map x atTop ≤ 𝓟 {a}ᶜ
Tactic: refine ⟨a, haA, accPt_iff_clusterPt.2 <| ClusterPt.mono hac <| le_inf ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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}ᶜ
⊢ ∃ a ∈ A, AccPt a (𝓟 B)
have refine_2 : map x atTop ≤ 𝓟 B
Tactic: refine ⟨a, haA, accPt_iff_clusterPt.2 <| ClusterPt.mono hac <| le_inf ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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
have refine : ∀ (x : ℕ → E) (hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A), ∃ a ∈ A, MapClusterPt a atTop x
Tactic: refine IsCountablyCompact.of_seq_clusterPt fun x hx => ?_
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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
⊢ ∃ a ∈ A, MapClusterPt a atTop x
have rw : ∀ (hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A), ∃ a ∈ A, MapClusterPt a cofinite x
Tactic: rw [← Nat.cofinite_eq_atTop] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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
⊢ ∃ a ∈ A, MapClusterPt a cofinite x
have pos : ∀ (hfin : (range x).Finite), ∃ a ∈ A, MapClusterPt a cofinite x
Tactic: by_cases! hfin : (Set.range x).Finite
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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
⊢ ∃ a ∈ A, MapClusterPt a cofinite x
have neg : ∀ (hfin : (range x).Infinite), ∃ a ∈ A, MapClusterPt a cofinite x
Tactic: by_cases! hfin : (Set.range x).Finite
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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 ∈ A, MapClusterPt a cofinite x
have pos : ∃ a ∈ range x ∩ A, MapClusterPt a cofinite x
Tactic: suffices ∃ a ∈ range x ∩ A, MapClusterPt a cofinite x by aesop
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
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
⊢ (range x ∩ A).Infinite
have hx₁ : Set.Finite (α := ℕ) {a : ℕ | x a ∉ A}
Tactic: rw [eventually_iff, mem_cofinite, compl_setOf] at hx
Cleared hypotheses: hx, hfin
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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 ∈ A, MapClusterPt a cofinite x
have neg : ∀ (a : E) (haA : a ∈ A) (hacc : AccPt a (𝓟 (range x ∩ A))), ∃ 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))
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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
have neg : MapClusterPt a cofinite x
Tactic: refine ⟨a, haA, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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))
⊢ MapClusterPt a cofinite x
have neg : ∀ s ∈ 𝓝 a, Set.Infinite (α := ℕ) {a : ℕ | x a ∈ s}
Tactic: simp_rw [mapClusterPt_iff_frequently, frequently_cofinite_iff_infinite]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
hl : IsLindelof A
⊢ IsCompact A
have 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
Tactic: refine isCompact_of_finite_subcover fun {ι} U hUo hAU => ?_