awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
inst_1 : Countable ι
inst_2 : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hAU : A ⊆ ⋃ (i : ι), U i
hdU : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) U
h : ∀ (i : ι), ¬A ⊆ U i
⊢ False
have hdir : Directed (fun (x1 x2 : Filter E) ↦ x1 ≥ x2) fun (i : ι) ↦ 𝓟 (A \ U i)
Tactic: have hdir : Directed (· ≥ ·) fun i => 𝓟 (A \ U i) :=
    fun i j => (hdU i j).imp fun _ ⟨hi, hj⟩ => ⟨principal_mono.mpr <| diff_subset_diff_right hi,
      principal_mono.mpr <| diff_subset_diff_right hj⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
inst_1 : Countable ι
inst_2 : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hAU : A ⊆ ⋃ (i : ι), U i
hdU : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) U
h : ∀ (i : ι), ¬A ⊆ U i
hdir : Directed (fun (x1 x2 : Filter E) ↦ x1 ≥ x2) fun (i : ι) ↦ 𝓟 (A \ U i)
⊢ False
have this : NeBot.{u_2} (α := E) (⨅ (i : ι), 𝓟 (A \ U i))
Tactic: have : NeBot (⨅ i, 𝓟 (A \ U i)) :=
    iInf_neBot_of_directed' hdir fun i => (diff_nonempty.mpr (h i)).principal_neBot
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
inst_1 : Countable ι
inst_2 : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hAU : A ⊆ ⋃ (i : ι), U i
hdU : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) U
h : ∀ (i : ι), ¬A ⊆ U i
hdir : Directed (fun (x1 x2 : Filter E) ↦ x1 ≥ x2) fun (i : ι) ↦ 𝓟 (A \ U i)
this : NeBot.{u_2} (α := E) (⨅ (i : ι), 𝓟 (A \ U i))
⊢ False
have hle : ⨅ (i : ι), 𝓟 (A \ U i) ≤ 𝓟 A
Tactic: have hle : (⨅ i, 𝓟 (A \ U i)) ≤ 𝓟 A :=
    iInf_le_of_le ‹Nonempty ι›.some <| principal_mono.mpr diff_subset
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
inst_1 : Countable ι
inst_2 : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hAU : A ⊆ ⋃ (i : ι), U i
hdU : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) U
h : ∀ (i : ι), ¬A ⊆ U i
hdir : Directed (fun (x1 x2 : Filter E) ↦ x1 ≥ x2) fun (i : ι) ↦ 𝓟 (A \ U i)
this : NeBot.{u_2} (α := E) (⨅ (i : ι), 𝓟 (A \ U i))
hle : ⨅ (i : ι), 𝓟 (A \ U i) ≤ 𝓟 A
⊢ False
have rcases : ∀ (a : E) (ha : a ∈ A) (hac : ClusterPt a (⨅ (i : ι), 𝓟 (A \ U i))), False
Tactic: rcases hA hle with ⟨a, ha, hac⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
inst_1 : Countable ι
inst_2 : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hAU : A ⊆ ⋃ (i : ι), U i
hdU : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) U
h : ∀ (i : ι), ¬A ⊆ U i
hdir : Directed (fun (x1 x2 : Filter E) ↦ x1 ≥ x2) fun (i : ι) ↦ 𝓟 (A \ U i)
this : NeBot.{u_2} (α := E) (⨅ (i : ι), 𝓟 (A \ U i))
hle : ⨅ (i : ι), 𝓟 (A \ U i) ≤ 𝓟 A
a : E
ha : a ∈ A
hac : ClusterPt a (⨅ (i : ι), 𝓟 (A \ U i))
⊢ False
have rcases : ∀ (k : ι) (hk : a ∈ U k), False
Tactic: rcases mem_iUnion.mp (hAU ha) with ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Finset ℕ), A ⊆ ⋃ i ∈ t, U i
⊢ 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
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Finset ℕ), A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
⊢ ∃ a ∈ A, MapClusterPt a atTop x
have by_contra! : ∀ (hac : ∀ (a : E) (_ : a ∈ A), ¬MapClusterPt a atTop x), False
Tactic: by_contra! hac
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Finset ℕ), A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
hac : ∀ (a : E) (_ : a ∈ A), ¬MapClusterPt a atTop x
V : ℕ → Set E := fun (n : ℕ) ↦ (closure[inst] (x '' Ici n))ᶜ
⊢ False
have hVmono : Monotone V
Tactic: have hVmono : Monotone V := fun _ _ hmn =>
      compl_subset_compl.2 <| closure_mono <| image_mono <| Ici_subset_Ici.2 hmn
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Finset ℕ), A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
hac : ∀ (a : E) (_ : a ∈ A), ¬MapClusterPt a atTop x
V : ℕ → Set E := fun (n : ℕ) ↦ (closure[inst] (x '' Ici n))ᶜ
hVmono : Monotone V
⊢ False
have hac₁ : ∀ (a : E) (_ : a ∈ A), ∃ (x_1 : ℕ), a ∉ closure[inst] (x '' Ici x_1)
Tactic: simp only [mapClusterPt_atTop_iff_forall_mem_closure, not_forall] at hac
Cleared hypotheses: hac
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Finset ℕ), A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
V : ℕ → Set E := fun (n : ℕ) ↦ (closure[inst] (x '' Ici n))ᶜ
hVmono : Monotone V
hac : ∀ (a : E) (_ : a ∈ A), ∃ (x_1 : ℕ), a ∉ closure[inst] (x '' Ici x_1)
⊢ False
have hAV : A ⊆ ⋃ (n : ℕ), V n
Tactic: have hAV : A ⊆ ⋃ n, V n := fun a haA => mem_iUnion.2 (hac a haA)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Finset ℕ), A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
V : ℕ → Set E := fun (n : ℕ) ↦ (closure[inst] (x '' Ici n))ᶜ
hVmono : Monotone V
hac : ∀ (a : E) (_ : a ∈ A), ∃ (x_1 : ℕ), a ∉ closure[inst] (x '' Ici x_1)
hAV : A ⊆ ⋃ (n : ℕ), V n
⊢ False
have obtain : ∀ (t : Finset ℕ) (ht : A ⊆ ⋃ i ∈ t, V i), False
Tactic: obtain ⟨t, ht⟩ := h V (fun _ => isClosed_closure.isOpen_compl) hAV
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Finset ℕ), A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
V : ℕ → Set E := fun (n : ℕ) ↦ (closure[inst] (x '' Ici n))ᶜ
hVmono : Monotone V
hac : ∀ (a : E) (_ : a ∈ A), ∃ (x_1 : ℕ), a ∉ closure[inst] (x '' Ici x_1)
hAV : A ⊆ ⋃ (n : ℕ), V n
t : Finset ℕ
ht : A ⊆ ⋃ i ∈ t, V i
⊢ False
have obtain : ∀ (N : ℕ) (hN : ∀ b ≥ N, x b ∈ A), False
Tactic: obtain ⟨N, hN⟩ := eventually_atTop.mp hx
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Finset ℕ), A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
V : ℕ → Set E := fun (n : ℕ) ↦ (closure[inst] (x '' Ici n))ᶜ
hVmono : Monotone V
hac : ∀ (a : E) (_ : a ∈ A), ∃ (x_1 : ℕ), a ∉ closure[inst] (x '' Ici x_1)
hAV : A ⊆ ⋃ (n : ℕ), V n
t : Finset ℕ
ht : A ⊆ ⋃ i ∈ t, V i
N : ℕ
hN : ∀ b ≥ N, x b ∈ A
m : ℕ := max N (t.sup id)
⊢ False
have obtain : ∀ (j : ℕ) (hjt : j ∈ t) (hjV : x m ∈ V j), False
Tactic: obtain ⟨j, hjt, hjV⟩ := mem_iUnion₂.mp (ht (hN m (le_max_left _ _)))
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Finset ℕ), A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
V : ℕ → Set E := fun (n : ℕ) ↦ (closure[inst] (x '' Ici n))ᶜ
hVmono : Monotone V
hac : ∀ (a : E) (_ : a ∈ A), ∃ (x_1 : ℕ), a ∉ closure[inst] (x '' Ici x_1)
hAV : A ⊆ ⋃ (n : ℕ), V n
t : Finset ℕ
ht : A ⊆ ⋃ i ∈ t, V i
N : ℕ
hN : ∀ b ≥ N, x b ∈ A
m : ℕ := max N (t.sup id)
j : ℕ
hjt : j ∈ t
hjV : x m ∈ V j
⊢ False
have hxmV : x m ∈ V m
Tactic: have hxmV : x m ∈ V m := hVmono ((Finset.le_sup hjt).trans (le_max_right _ _)) hjV
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
hb : b.Countable
U : ι → Set E
hUo : ∀ i ∈ b, IsOpen[inst] (U i)
hAU : A ⊆ ⋃ i ∈ b, U i
⊢ ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
have this : Countable.{u_1 + 1} (↑b : Type u_1)
Tactic: have := hb.to_subtype
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
hb : b.Countable
U : ι → Set E
hUo : ∀ i ∈ b, IsOpen[inst] (U i)
hAU : A ⊆ ⋃ i ∈ b, U i
this : Countable.{u_1 + 1} (↑b : Type u_1)
⊢ ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
have obtain : ∀ (t : Finset (↑b : Type u_1)) (ht : A ⊆ ⋃ i ∈ t, U (↑i : ι)), ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
Tactic: obtain ⟨t, ht⟩ := hA.elim_finite_subcover (fun (i : b) ↦ hUo i i.prop) (by simpa using hAU)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
hb : b.Countable
U : ι → Set E
hUo : ∀ i ∈ b, IsOpen[inst] (U i)
hAU : A ⊆ ⋃ i ∈ b, U i
this : Countable.{u_1 + 1} (↑b : Type u_1)
t : Finset (↑b : Type u_1)
ht : A ⊆ ⋃ i ∈ t, U (↑i : ι)
⊢ ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
have hUo₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))
Tactic: simp only [Subtype.forall', biUnion_eq_iUnion] at hUo hAU
Cleared hypotheses: hUo, hAU
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
hb : b.Countable
U : ι → Set E
hUo : ∀ i ∈ b, IsOpen[inst] (U i)
hAU : A ⊆ ⋃ i ∈ b, U i
this : Countable.{u_1 + 1} (↑b : Type u_1)
t : Finset (↑b : Type u_1)
ht : A ⊆ ⋃ i ∈ t, U (↑i : ι)
hUo₁ : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))
⊢ ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
have hAU₁ : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι)
Tactic: simp only [Subtype.forall', biUnion_eq_iUnion] at hUo hAU
Cleared hypotheses: hUo, hAU
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
U : ι → Set E
this : Countable.{u_1 + 1} (↑b : Type u_1)
t : Finset (↑b : Type u_1)
ht : A ⊆ ⋃ i ∈ t, U (↑i : ι)
hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))
hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι)
hb : Countable.{u_1 + 1} (↑b : Type u_1)
⊢ ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
have obtain : ∀ (d : Finset { a : ι // a ∈ b }) (hd : A ⊆ ⋃ i ∈ d, U (↑i : ι)), ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
Tactic: obtain ⟨d, hd⟩ := hA.elim_finite_subcover hUo hAU
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
U : ι → Set E
this : Countable.{u_1 + 1} (↑b : Type u_1)
t : Finset (↑b : Type u_1)
ht : A ⊆ ⋃ i ∈ t, U (↑i : ι)
hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))
hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι)
hb : Countable.{u_1 + 1} (↑b : Type u_1)
d : Finset { a : ι // a ∈ b }
hd : A ⊆ ⋃ i ∈ d, U (↑i : ι)
⊢ ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
have refine_1 : Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)) ⊆ b
Tactic: refine ⟨Subtype.val '' (d : Set b), ?_, d.finite_toSet.image _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
U : ι → Set E
this : Countable.{u_1 + 1} (↑b : Type u_1)
t : Finset (↑b : Type u_1)
ht : A ⊆ ⋃ i ∈ t, U (↑i : ι)
hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))
hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι)
hb : Countable.{u_1 + 1} (↑b : Type u_1)
d : Finset { a : ι // a ∈ b }
hd : A ⊆ ⋃ i ∈ d, U (↑i : ι)
refine_1 : Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)) ⊆ b
⊢ ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
have refine_2 : A ⊆ ⋃ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)), U i
Tactic: refine ⟨Subtype.val '' (d : Set b), ?_, d.finite_toSet.image _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
U : ι → Set E
this : Countable.{u_1 + 1} (↑b : Type u_1)
t : Finset (↑b : Type u_1)
ht : A ⊆ ⋃ i ∈ t, U (↑i : ι)
hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))
hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι)
hb : Countable.{u_1 + 1} (↑b : Type u_1)
d : Finset { a : ι // a ∈ b }
hd : A ⊆ ⋃ i ∈ d, U (↑i : ι)
⊢ A ⊆ ⋃ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)), U i
have refine_2 : A ⊆ ⋃ y ∈ (↑d : Set (↑b : Type u_1)), U (↑y : ι)
Tactic: rwa [biUnion_image]
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
hb : b.Countable
U : ι → Set E
hUo : ∀ i ∈ b, IsOpen[inst] (U i)
hAU : A ⊆ ⋃ i ∈ b, U i
this : Countable.{u_1 + 1} (↑b : Type u_1)
t : Finset (↑b : Type u_1)
ht : A ⊆ ⋃ i ∈ t, U (↑i : ι)
⊢ ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
have simp : ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι)),
  ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
Tactic: classical
  simp only [Subtype.forall', biUnion_eq_iUnion] at hUo hAU
  replace hb := hb.to_subtype
  obtain ⟨d, hd⟩ := hA.elim_finite_subcover hUo hAU
  refine ⟨Subtype.val '' (d : Set b), ?_, d.finite_toSet.image _, ?_⟩
  · simp
  · rwa [biUnion_image]
Cleared hypotheses: hUo, hAU
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
hb : b.Countable
U : ι → Set E
hUo : ∀ i ∈ b, IsOpen[inst] (U i)
hAU : A ⊆ ⋃ i ∈ b, U i
this : Countable.{u_1 + 1} (↑b : Type u_1)
t : Finset (↑b : Type u_1)
ht : A ⊆ ⋃ i ∈ t, U (↑i : ι)
simp :
  ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι)),
    ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
⊢ ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
have simp₁ : ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι))
  (hb : Countable.{u_1 + 1} (↑b : Type u_1)), ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
Tactic: classical
  simp only [Subtype.forall', biUnion_eq_iUnion] at hUo hAU
  replace hb := hb.to_subtype
  obtain ⟨d, hd⟩ := hA.elim_finite_subcover hUo hAU
  refine ⟨Subtype.val '' (d : Set b), ?_, d.finite_toSet.image _, ?_⟩
  · simp
  · rwa [biUnion_image]
Cleared hypotheses: hb, hUo, hAU
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
hb : b.Countable
U : ι → Set E
hUo : ∀ i ∈ b, IsOpen[inst] (U i)
hAU : A ⊆ ⋃ i ∈ b, U i
this : Countable.{u_1 + 1} (↑b : Type u_1)
t : Finset (↑b : Type u_1)
ht : A ⊆ ⋃ i ∈ t, U (↑i : ι)
simp :
  ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι)),
    ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
simp₁ :
  ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι))
    (hb : Countable.{u_1 + 1} (↑b : Type u_1)), ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
⊢ ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
have simp₂ : ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι))
  (hb : Countable.{u_1 + 1} (↑b : Type u_1)) (d : Finset { a : ι // a ∈ b }) (hd : A ⊆ ⋃ i ∈ d, U (↑i : ι)),
  ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
Tactic: classical
  simp only [Subtype.forall', biUnion_eq_iUnion] at hUo hAU
  replace hb := hb.to_subtype
  obtain ⟨d, hd⟩ := hA.elim_finite_subcover hUo hAU
  refine ⟨Subtype.val '' (d : Set b), ?_, d.finite_toSet.image _, ?_⟩
  · simp
  · rwa [biUnion_image]
Cleared hypotheses: hb, hUo, hAU
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
hb : b.Countable
U : ι → Set E
hUo : ∀ i ∈ b, IsOpen[inst] (U i)
hAU : A ⊆ ⋃ i ∈ b, U i
this : Countable.{u_1 + 1} (↑b : Type u_1)
t : Finset (↑b : Type u_1)
ht : A ⊆ ⋃ i ∈ t, U (↑i : ι)
simp :
  ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι)),
    ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
simp₁ :
  ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι))
    (hb : Countable.{u_1 + 1} (↑b : Type u_1)), ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
simp₂ :
  ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι))
    (hb : Countable.{u_1 + 1} (↑b : Type u_1)) (d : Finset { a : ι // a ∈ b }) (hd : A ⊆ ⋃ i ∈ d, U (↑i : ι)),
    ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
⊢ ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
have refine_1 : ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι))
  (hb : Countable.{u_1 + 1} (↑b : Type u_1)) (d : Finset { a : ι // a ∈ b }) (hd : A ⊆ ⋃ i ∈ d, U (↑i : ι)),
  Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)) ⊆ b
Tactic: classical
  simp only [Subtype.forall', biUnion_eq_iUnion] at hUo hAU
  replace hb := hb.to_subtype
  obtain ⟨d, hd⟩ := hA.elim_finite_subcover hUo hAU
  refine ⟨Subtype.val '' (d : Set b), ?_, d.finite_toSet.image _, ?_⟩
  · simp
  · rwa [biUnion_image]
Cleared hypotheses: hb, hUo, hAU
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
b : Set ι
hb : b.Countable
U : ι → Set E
hUo : ∀ i ∈ b, IsOpen[inst] (U i)
hAU : A ⊆ ⋃ i ∈ b, U i
this : Countable.{u_1 + 1} (↑b : Type u_1)
t : Finset (↑b : Type u_1)
ht : A ⊆ ⋃ i ∈ t, U (↑i : ι)
simp :
  ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι)),
    ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
simp₁ :
  ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι))
    (hb : Countable.{u_1 + 1} (↑b : Type u_1)), ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
simp₂ :
  ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι))
    (hb : Countable.{u_1 + 1} (↑b : Type u_1)) (d : Finset { a : ι // a ∈ b }) (hd : A ⊆ ⋃ i ∈ d, U (↑i : ι)),
    ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
refine_1 :
  ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι))
    (hb : Countable.{u_1 + 1} (↑b : Type u_1)) (d : Finset { a : ι // a ∈ b }) (hd : A ⊆ ⋃ i ∈ d, U (↑i : ι)),
    Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)) ⊆ b
⊢ ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
have refine_2 : ∀ (hUo : ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))) (hAU : A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι))
  (hb : Countable.{u_1 + 1} (↑b : Type u_1)) (d : Finset { a : ι // a ∈ b }) (hd : A ⊆ ⋃ i ∈ d, U (↑i : ι)),
  A ⊆ ⋃ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)), U i
Tactic: classical
  simp only [Subtype.forall', biUnion_eq_iUnion] at hUo hAU
  replace hb := hb.to_subtype
  obtain ⟨d, hd⟩ := hA.elim_finite_subcover hUo hAU
  refine ⟨Subtype.val '' (d : Set b), ?_, d.finite_toSet.image _, ?_⟩
  · simp
  · rwa [biUnion_image]
Cleared hypotheses: hb, hUo, hAU
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsSeqCompact A
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
⊢ ∃ a ∈ A, MapClusterPt a atTop x
have obtain : ∀ (a : E) (ha : a ∈ A) (φ : ℕ → ℕ) (hφ : StrictMono φ) (hφa : Tendsto (x ∘ φ) atTop (𝓝 a)),
  ∃ a ∈ A, MapClusterPt a atTop x
Tactic: obtain ⟨a, ha, φ, hφ, hφa⟩ := hA.subseq_of_frequently_in hx.frequently
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
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)
⊢ ∃ a ∈ f '' A, ClusterPt a l
have this : (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)
-- 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
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
⊢ ∃ a ∈ f '' A, ClusterPt a l
have obtain : ∀ (x : E) (hxA : x ∈ A) (hx : ClusterPt x (comap f l ⊓ 𝓟 A)), ∃ a ∈ f '' A, ClusterPt a l
Tactic: obtain ⟨x, hxA, hx⟩ := hA (f := l.comap f ⊓ 𝓟 A) inf_le_right
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (hypothesis)
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)
⊢ ∃ a ∈ f '' A, ClusterPt a l
have this₁ : (𝓝 x ⊓ comap f l).NeBot
Tactic: have := (hx.mono inf_le_left).neBot
-- 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 : IsInducing f
⊢ IsCountablyCompact A ↔ IsCountablyCompact (f '' A)
have 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
Tactic: refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot Fc F_le => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
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
⊢ ∃ a ∈ A, ClusterPt a F
have obtain : ∀ (x : E) (x_in : x ∈ A) (hx : ClusterPt (f x) (map f 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)
-- Lean 4 proof step from Mathlib.Topology.Compactness.CountablyCompact (goal)
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
⊢ IsCountablyCompact A ↔ IsCountablyCompact.{u_2} (E := (↑A : Type u_2)) univ
have rw : IsCountablyCompact A ↔
  IsCountablyCompact.{u_2} (E := E) (image (α := { x : E // x ∈ A }) (Subtype.val (p := fun (x : E) ↦ x ∈ A)) univ)
Tactic: rw [Subtype.isCountablyCompact_iff, image_univ, Subtype.range_coe]