awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a atTop x
f : Filter E
h : f.NeBot
h_1 : f.IsCountablyGenerated
hle : f ≤ 𝓟 A
x : ℕ → E
hx : Tendsto x atTop f
obtain : ∀ (a : E) (ha : a ∈ A) (hxa : MapClusterPt a atTop x), ∃ a ∈ A, ClusterPt a f
⊢ ∃ a ∈ A, ClusterPt a f

Tactic:
obtain ⟨a, ha, hxa⟩ := hA x (by simpa using hx.mono_right hle)
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a atTop x
f : Filter E
h : f.NeBot
h_1 : f.IsCountablyGenerated
hle : f ≤ 𝓟 A
x : ℕ → E
hx : Tendsto x atTop f
a : E
ha : a ∈ A
hxa : MapClusterPt a atTop x
⊢ ∃ a ∈ A, ClusterPt a f

Tactic:
⟨a, ha, hxa.clusterPt.mono hx⟩

Premises used: ClusterPt.mono, MapClusterPt.clusterPt, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a atTop x
f : Filter E
h : f.NeBot
h_1 : f.IsCountablyGenerated
hle : f ≤ 𝓟 A
x : ℕ → E
hx : Tendsto x atTop f
a : E
ha : a ∈ A
hxa : MapClusterPt a atTop x
⊢ ∃ a ∈ A, ClusterPt a f

Tactic:
exact ⟨a, ha, hxa.clusterPt.mono hx⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
by_contra! : ∀ (h : ∀ (i : ι), ¬A ⊆ U i), False
⊢ ∃ (i : ι), A ⊆ U i

Tactic:
by_contra! h
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
⊢ 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⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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)
⊢ 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
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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))
⊢ ⨅ (i : ι), 𝓟 (A \ U i) ≤ 𝓟 A

Tactic:
have hle : (⨅ i, 𝓟 (A \ U i)) ≤ 𝓟 A :=
    iInf_le_of_le ‹Nonempty ι›.some <| principal_mono.mpr diff_subset
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
rcases : ∀ (a : E) (ha : a ∈ A) (hac : ClusterPt a (⨅ (i : ι), 𝓟 (A \ U i))), False
⊢ False

Tactic:
rcases hA hle with ⟨a, ha, hac⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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))
rcases : ∀ (k : ι) (hk : a ∈ U k), False
⊢ False

Tactic:
rcases mem_iUnion.mp (hAU ha) with ⟨k, hk⟩

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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))
k : ι
hk : a ∈ U k
⊢ False

Tactic:
closure_minimal (fun _ hx => hx.2) (hUo k).isClosed_compl
    (hac.mono (iInf_le _ k)).mem_closure hk

Premises used: ClusterPt.mono, closure_minimal, IsOpen.isClosed_compl, ClusterPt.mem_closure, iInf_le
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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))
k : ι
hk : a ∈ U k
⊢ False

Tactic:
exact closure_minimal (fun _ hx => hx.2) (hUo k).isClosed_compl
    (hac.mono (iInf_le _ k)).mem_closure hk

Premises used: ClusterPt.mono, closure_minimal, IsOpen.isClosed_compl, ClusterPt.mem_closure, iInf_le
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
ι : Type u_1
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
inst_1 : Countable ι
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hAU : A ⊆ ⋃ (i : ι), U i
⊢ ∃ (t : Finset ι), A ⊆ ⋃ i ∈ t, U i

Tactic:
hA.elim_directed_cover _ (fun _ => isOpen_biUnion fun i _ => hUo i)
    (iUnion_eq_iUnion_finset U ▸ hAU)
    (directed_of_isDirected_le fun _ _ h => biUnion_subset_biUnion_left h)

Premises used: IsCountablyCompact.elim_directed_cover, Eq.rec, directed_of_isDirected_le, Set.iUnion_eq_iUnion_finset, Set.biUnion_subset_biUnion_left, isOpen_biUnion
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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

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
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Finset ℕ), A ⊆ ⋃ i ∈ t, U i
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
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
by_contra! : ∀ (hac : ∀ (a : E) (_ : a ∈ A), ¬MapClusterPt a atTop x), False
⊢ ∃ a ∈ A, MapClusterPt a atTop x

Tactic:
by_contra! hac
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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))ᶜ
⊢ Monotone V

Tactic:
have hVmono : Monotone V := fun _ _ hmn =>
      compl_subset_compl.2 <| closure_mono <| image_mono <| Ici_subset_Ici.2 hmn
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
⊢ ∀ (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

Premises used: mapClusterPt_atTop_iff_forall_mem_closure, Classical.not_forall
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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)
⊢ A ⊆ ⋃ (n : ℕ), V n

Tactic:
have hAV : A ⊆ ⋃ n, V n := fun a haA => mem_iUnion.2 (hac a haA)
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
obtain : ∀ (t : Finset ℕ) (ht : A ⊆ ⋃ i ∈ t, V i), False
⊢ False

Tactic:
obtain ⟨t, ht⟩ := h V (fun _ => isClosed_closure.isOpen_compl) hAV

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
obtain : ∀ (N : ℕ) (hN : ∀ b ≥ N, x b ∈ A), False
⊢ False

Tactic:
obtain ⟨N, hN⟩ := eventually_atTop.mp hx

Premises used: Iff.mp, Filter.eventually_atTop
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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)
obtain : ∀ (j : ℕ) (hjt : j ∈ t) (hjV : x m ∈ V j), False
⊢ False

Tactic:
obtain ⟨j, hjt, hjV⟩ := mem_iUnion₂.mp (ht (hN m (le_max_left _ _)))

Premises used: Set.mem_iUnion₂, Iff.mp, le_max_left
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
⊢ x m ∈ V m

Tactic:
have hxmV : x m ∈ V m := hVmono ((Finset.le_sup hjt).trans (le_max_right _ _)) hjV
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
hxmV : x m ∈ V m
⊢ False

Tactic:
hxmV (subset_closure ⟨m, mem_Ici.mpr le_rfl, rfl⟩)

Premises used: Iff.mpr, le_rfl, subset_closure, And.intro, Set.mem_Ici, Exists.intro, rfl
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
hxmV : x m ∈ V m
⊢ False

Tactic:
exact hxmV (subset_closure ⟨m, mem_Ici.mpr le_rfl, rfl⟩)

Premises used: Iff.mpr, le_rfl, subset_closure, And.intro, Set.mem_Ici, Exists.intro, rfl
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
⊢ Countable.{u_1 + 1} (↑b : Type u_1)

Tactic:
have := hb.to_subtype
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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)
⊢ A ⊆ ⋃ (i : (↑b : Type u_1)), U (↑i : ι)

Tactic:
simpa using hAU
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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)
obtain : ∀ (t : Finset (↑b : Type u_1)) (ht : A ⊆ ⋃ i ∈ t, U (↑i : ι)), ∃ t ⊆ b, t.Finite ∧ 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)

Premises used: IsCountablyCompact.elim_finite_subcover, Subtype.prop, Subtype.val
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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 : ι)
⊢ ∀ (x : { a : ι // a ∈ b }), IsOpen[inst] (U (↑x : ι))

Tactic:
simp only [Subtype.forall', biUnion_eq_iUnion] at hUo hAU

Premises used: Set.biUnion_eq_iUnion, Subtype.forall'
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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 : ι))
⊢ A ⊆ ⋃ (x : (↑b : Type u_1)), U (↑x : ι)

Tactic:
simp only [Subtype.forall', biUnion_eq_iUnion] at hUo hAU

Premises used: Set.biUnion_eq_iUnion, Subtype.forall'
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
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 : ι)
⊢ Countable.{u_1 + 1} (↑b : Type u_1)

Tactic:
replace hb := hb.to_subtype
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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)
obtain : ∀ (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

Tactic:
obtain ⟨d, hd⟩ := hA.elim_finite_subcover hUo hAU

Premises used: IsCountablyCompact.elim_finite_subcover
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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

Tactic:
⟨Subtype.val '' (d : Set b), ?_, d.finite_toSet.image _, ?_⟩

Premises used: Set.Finite.image, SetLike.coe, And.intro, Exists.intro, Set.image, Finset.finite_toSet, Subtype.val
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
refine_2 : A ⊆ ⋃ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)), U i
⊢ ∃ t ⊆ b, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i

Tactic:
refine ⟨Subtype.val '' (d : Set b), ?_, d.finite_toSet.image _, ?_⟩
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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 : ι)
⊢ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)) ⊆ b

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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_2 refine_2₁ refine_2₂ refine_2₃ : A ⊆ ⋃ y ∈ (↑d : Set (↑b : Type u_1)), U (↑y : ι)
⊢ A ⊆ ⋃ i ∈ Subtype.val (p := fun (x : ι) ↦ x ∈ b) '' (↑d : Set (↑b : Type u_1)), U i

Tactic:
rwa [biUnion_image]

Premises used: Set.biUnion_image
-- Module: Mathlib.Topology.Compactness.CountablyCompact
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
refine_2 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
⊢ ∃ 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]

Premises used: Set.biUnion_eq_iUnion, Subtype.forall', Set.biUnion_image
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
⊢ IsCountablyCompact A ↔
    ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst] (U i)) → A ⊆ ⋃ (i : ℕ), U i → ∃ (t : Set ℕ), t.Finite ∧ A ⊆ ⋃ i ∈ t, U i

Tactic:
simp [isCountablyCompact_iff_countable_open_cover, Finset.exists]

Premises used: isCountablyCompact_iff_countable_open_cover, Finset.exists
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : IsCompact A
⊢ IsCountablyCompact A

Tactic:
fun _ _ _ hle => hA hle

Premises used: IsCountablyCompact
-- 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
obtain :
  ∀ (a : E) (ha : a ∈ A) (φ : ℕ → ℕ) (hφ : StrictMono φ) (hφa : Tendsto (x ∘ φ) atTop (𝓝 a)),
    ∃ a ∈ A, MapClusterPt a atTop x
⊢ ∃ a ∈ A, MapClusterPt a atTop x

Tactic:
obtain ⟨a, ha, φ, hφ, hφa⟩ := hA.subseq_of_frequently_in hx.frequently

Premises used: IsSeqCompact.subseq_of_frequently_in, Filter.Eventually.frequently
-- 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:
⟨a, ha, hφa.mapClusterPt.of_comp hφ.tendsto_atTop⟩

Premises used: Filter.Tendsto.mapClusterPt, StrictMono.tendsto_atTop, And.intro, Exists.intro, MapClusterPt.of_comp