awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
⊢ ∃ (z : ι),
    (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) (V i ∩ Wᶜ) (V z ∩ Wᶜ) ∧ (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) (V j ∩ Wᶜ) (V z ∩ Wᶜ)
have refine_1 : ∀ x ∈ V k ∩ Wᶜ, x ∈ V i ∩ Wᶜ
Tactic: refine ⟨k, ⟨fun x => ?_, fun x => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
refine_1 : ∀ x ∈ V k ∩ Wᶜ, x ∈ V i ∩ Wᶜ
⊢ ∃ (z : ι),
    (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) (V i ∩ Wᶜ) (V z ∩ Wᶜ) ∧ (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) (V j ∩ Wᶜ) (V z ∩ Wᶜ)
have refine_2 : ∀ x ∈ V k ∩ Wᶜ, x ∈ V j ∩ Wᶜ
Tactic: refine ⟨k, ⟨fun x => ?_, fun x => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
⊢ x ∈ V k ∩ Wᶜ → x ∈ V i ∩ Wᶜ
have refine_1 : x ∈ V k → x ∉ W → x ∈ V i ∧ x ∉ W
Tactic: simp only [and_imp, mem_inter_iff, mem_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
⊢ x ∈ V k ∩ Wᶜ → x ∈ V j ∩ Wᶜ
have refine_2 : x ∈ V k → x ∉ W → x ∈ V j ∧ x ∉ W
Tactic: simp only [and_imp, mem_inter_iff, mem_compl_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
refine_1 refine_1₁ : x ∈ V k → x ∉ W → x ∈ V i ∧ x ∉ W
⊢ x ∈ V k → x ∉ W → x ∈ V i ∧ x ∉ W
have refine_1₂ : x ∈ V k → x ∉ W → x ∈ V i
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
refine_1 refine_1₁ : x ∈ V k → x ∉ W → x ∈ V i ∧ x ∉ W
refine_1₂ : x ∈ V k → x ∉ W → x ∈ V i
⊢ x ∈ V k → x ∉ W → x ∈ V i ∧ x ∉ W
have refine_1₃ : x ∈ V k → x ∉ W → x ∉ W
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
refine_2 refine_2₁ : x ∈ V k → x ∉ W → x ∈ V j ∧ x ∉ W
⊢ x ∈ V k → x ∉ W → x ∈ V j ∧ x ∉ W
have refine_2₂ : x ∈ V k → x ∉ W → x ∈ V j
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
refine_2 refine_2₁ : x ∈ V k → x ∉ W → x ∈ V j ∧ x ∉ W
refine_2₂ : x ∈ V k → x ∉ W → x ∈ V j
⊢ x ∈ V k → x ∉ W → x ∈ V j ∧ x ∉ W
have refine_2₃ : x ∈ V k → x ∉ W → x ∉ W
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
⊢ False
have this : Set.Nonempty.{u} (α := X) (⋂ (i : ι), V i ∩ Wᶜ)
Tactic: have : (⋂ i, V i ∩ Wᶜ).Nonempty := by
    refine
      IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ (fun i j => ?_) H
        (fun i => (hV_cpct i).inter_right W_op.isClosed_compl) fun i =>
        (hV_closed i).inter W_op.isClosed_compl
    rcases hV i j with ⟨k, hki, hkj⟩
    refine ⟨k, ⟨fun x => ?_, fun x => ?_⟩⟩ <;> simp only [and_imp, mem_inter_iff, mem_compl_iff] <;>
      tauto
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
W : Set X
hsubW : ⋂ (i : ι), V i ⊆ W
W_op : IsOpen[inst] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
this : Set.Nonempty.{u} (α := X) (⋂ (i : ι), V i ∩ Wᶜ)
⊢ False
have this₁ : ¬⋂ (i : ι), V i ⊆ W
Tactic: have : ¬⋂ i : ι, V i ⊆ W := by simpa [← iInter_inter, inter_compl_nonempty_iff]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
⊢ IsCompact s
have rw : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
Tactic: rw [isCompact_iff_ultrafilter_le_nhds', hTS]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
⊢ ∃ x ∈ s, (↑F : Filter X) ≤ 𝓝 x
have by_contra : ∀ (hF : ¬∃ x ∈ s, (↑F : Filter X) ≤ 𝓝 x), False
Tactic: by_contra hF
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, (↑F : Filter X) ≤ 𝓝 x
⊢ False
have hSF : ∀ x ∈ s, ∃ (t : Set X), x ∈ t ∧ t ∈ S ∧ t ∉ F
Tactic: have hSF : ∀ x ∈ s, ∃ t, x ∈ t ∧ t ∈ S ∧ t ∉ F := by simpa [nhds_generateFrom] using hF
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, (↑F : Filter X) ≤ 𝓝 x
hSF : ∀ x ∈ s, ∃ (t : Set X), x ∈ t ∧ t ∈ S ∧ t ∉ F
⊢ False
have choose! : ∀ (U : (x : X) → Set X) (hxU : ∀ x ∈ s, x ∈ U x) (hSU : ∀ x ∈ s, U x ∈ S) (hUF : ∀ x ∈ s, U x ∉ F), False
Tactic: choose! U hxU hSU hUF using hSF
Cleared hypotheses: hSF
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, (↑F : Filter X) ≤ 𝓝 x
U : (x : X) → Set X
hxU : ∀ x ∈ s, x ∈ U x
hSU : ∀ x ∈ s, U x ∈ S
hUF : ∀ x ∈ s, U x ∉ F
⊢ False
have obtain : ∀ (Q : Set (Set X)) (hQU : Q ⊆ U '' s) (hQ : Q.Finite) (hsQ : s ⊆ ⋃₀ Q), False
Tactic: obtain ⟨Q, hQU, hQ, hsQ⟩ := h (U '' s) (by simpa [Set.subset_def])
    (fun x hx ↦ Set.mem_sUnion_of_mem (hxU _ hx) (by grind))
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, (↑F : Filter X) ≤ 𝓝 x
U : (x : X) → Set X
hxU : ∀ x ∈ s, x ∈ U x
hSU : ∀ x ∈ s, U x ∈ S
hUF : ∀ x ∈ s, U x ∉ F
Q : Set (Set X)
hQU : Q ⊆ U '' s
hQ : Q.Finite
hsQ : s ⊆ ⋃₀ Q
⊢ False
have this : ∀ s ∈ Q, s ∉ F
Tactic: have : ∀ s ∈ Q, s ∉ F := fun s hsQ ↦ (hQU hsQ).choose_spec.2 ▸ hUF _ (hQU hsQ).choose_spec.1
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, (↑F : Filter X) ≤ 𝓝 x
U : (x : X) → Set X
hxU : ∀ x ∈ s, x ∈ U x
hSU : ∀ x ∈ s, U x ∈ S
hUF : ∀ x ∈ s, U x ∉ F
Q : Set (Set X)
hQU : Q ⊆ U '' s
hQ : Q.Finite
hsQ : s ⊆ ⋃₀ Q
this : ∀ s ∈ Q, s ∉ F
⊢ False
have hQF : ⋂₀ (compl '' Q) ∈ (↑F : Filter X).sets
Tactic: have hQF : ⋂₀ (compl '' Q) ∈ F.sets := by simpa [Filter.biInter_mem hQ, F.compl_mem_iff_notMem]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, (↑F : Filter X) ≤ 𝓝 x
U : (x : X) → Set X
hxU : ∀ x ∈ s, x ∈ U x
hSU : ∀ x ∈ s, U x ∈ S
hUF : ∀ x ∈ s, U x ∉ F
Q : Set (Set X)
hQU : Q ⊆ U '' s
hQ : Q.Finite
hsQ : s ⊆ ⋃₀ Q
this : ∀ s ∈ Q, s ∉ F
hQF : ⋂₀ (compl '' Q) ∈ (↑F : Filter X).sets
⊢ False
have this₁ : ⋃₀ Q ∉ F
Tactic: have : ⋃₀ Q ∉ F := by
    simpa [-Set.sInter_image, ← Set.compl_sUnion, hsQ, F.compl_mem_iff_notMem] using hQF
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
f : Filter X
⊢ Disjoint (cocompact X) f ↔ ∃ K ∈ f, IsCompact K
have simp_rw : (∃ (i : Set X), IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K
Tactic: simp_rw [hasBasis_cocompact.disjoint_iff_left, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
f : Filter X
⊢ (∃ (i : Set X), IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K
have mp : (∃ (i : Set X), IsCompact i ∧ i ∈ f) → ∃ K ∈ f, IsCompact K
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
f : Filter X
mp : (∃ (i : Set X), IsCompact i ∧ i ∈ f) → ∃ K ∈ f, IsCompact K
⊢ (∃ (i : Set X), IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K
have mpr : (∃ K ∈ f, IsCompact K) → ∃ (i : Set X), IsCompact i ∧ i ∈ f
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
f : Filter X
mp : (∃ (i : Set X), IsCompact i ∧ i ∈ f) → ∃ K ∈ f, IsCompact K
mpr : (∃ K ∈ f, IsCompact K) → ∃ (i : Set X), IsCompact i ∧ i ∈ f
⊢ (∃ (i : Set X), IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K
have mp₁ : ∀ (w : Set X), IsCompact w → w ∈ f → ∃ K ∈ f, IsCompact K
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
f : Filter X
mp : (∃ (i : Set X), IsCompact i ∧ i ∈ f) → ∃ K ∈ f, IsCompact K
mpr : (∃ K ∈ f, IsCompact K) → ∃ (i : Set X), IsCompact i ∧ i ∈ f
mp₁ mp₂ mp₃ : ∀ (w : Set X), IsCompact w → w ∈ f → ∃ K ∈ f, IsCompact K
⊢ (∃ (i : Set X), IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K
have mpr₁ : ∀ w ∈ f, IsCompact w → ∃ (i : Set X), IsCompact i ∧ i ∈ f
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
f : Filter X
⊢ Disjoint f (cocompact X) ↔ ∃ K ∈ f, IsCompact K
have simp_rw : (∃ (i : Set X), IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K
Tactic: simp_rw [hasBasis_cocompact.disjoint_iff_right, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
have pos : ∀ (hy : ClusterPt y l), ∃ x ∈ insert y (range f), ClusterPt x l
Tactic: by_cases hy : ClusterPt y l
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
pos : ∀ (hy : ClusterPt y l), ∃ x ∈ insert y (range f), ClusterPt x l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
have neg : ∀ (hy : ¬ClusterPt y l), ∃ x ∈ insert y (range f), ClusterPt x l
Tactic: by_cases hy : ClusterPt y l
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
hy : ¬ClusterPt y l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
have hy₁ : ∃ (x : Set Y) (_ : x ∈ 𝓝 y) (x_1 : Set Y) (_ : x_1 ∈ l), Disjoint x x_1
Tactic: simp only [clusterPt_iff_nonempty, not_forall, ← not_disjoint_iff_nonempty_inter, not_not] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
hy : ∃ (x : Set Y) (_ : x ∈ 𝓝 y) (x_1 : Set Y) (_ : x_1 ∈ l), Disjoint x x_1
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
have neg : ∀ (s : Set Y) (hsy : s ∈ 𝓝 y) (t : Set Y) (htl : t ∈ l) (hd : Disjoint s t), ∃ x ∈ insert y (range f), ClusterPt x l
Tactic: rcases hy with ⟨s, hsy, t, htl, hd⟩
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
have neg : ∀ (K : Set X) (hKc : IsCompact K) (hKs : Kᶜ ⊆ f ⁻¹' s), ∃ x ∈ insert y (range f), ClusterPt x l
Tactic: rcases mem_cocompact.1 (hf hsy) with ⟨K, hKc, hKs⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
⊢ f '' K ∈ l
have h : ∀ (y_1 : Y) (hyt : y_1 ∈ t) (hyf : y_1 ∈ insert y (range f)), y_1 ∈ f '' K
Tactic: filter_upwards [htl, le_principal_iff.1 hle] with y hyt hyf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y_1 : Y
hf : Tendsto f (cocompact X) (𝓝 y_1)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y_1 (range f))
s : Set Y
hsy : s ∈ 𝓝 y_1
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hyf : y ∈ insert y_1 (range f)
⊢ y ∈ f '' K
have h : ∀ (hf : Tendsto f (cocompact X) (𝓝 y)) (hle : l ≤ 𝓟 (insert y (range f))) (hsy : s ∈ 𝓝 y), y ∈ f '' K
Tactic: rcases hyf with (rfl | ⟨x, rfl⟩)
Cleared hypotheses: y_1, hf, hle, hsy, hyf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y_1 : Y
hf : Tendsto f (cocompact X) (𝓝 y_1)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y_1 (range f))
s : Set Y
hsy : s ∈ 𝓝 y_1
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
y : Y
hyt : y ∈ t
hyf : y ∈ insert y_1 (range f)
h : ∀ (hf : Tendsto f (cocompact X) (𝓝 y)) (hle : l ≤ 𝓟 (insert y (range f))) (hsy : s ∈ 𝓝 y), y ∈ f '' K
⊢ y ∈ f '' K
have h₁ : ∀ (x : X) (hyt : f x ∈ t), f x ∈ f '' K
Tactic: rcases hyf with (rfl | ⟨x, rfl⟩)
Cleared hypotheses: y, hyt, hyf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
have this : f '' K ∈ l
Tactic: have : f '' K ∈ l := by
    filter_upwards [htl, le_principal_iff.1 hle] with y hyt hyf
    rcases hyf with (rfl | ⟨x, rfl⟩)
    exacts [(hd.le_bot ⟨mem_of_mem_nhds hsy, hyt⟩).elim,
      mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst, inst_1] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
this : f '' K ∈ l
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
have neg : ∀ (y_1 : Y) (hy : y_1 ∈ f '' K) (hyl : ClusterPt y_1 l), ∃ x ∈ insert y (range f), ClusterPt x l
Tactic: rcases hKc.image hfc (le_principal_iff.2 this) with ⟨y, hy, hyl⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
this : TopologicalSpace ι := ⊥
⊢ IsCompact (insert x (range f))
have h : DiscreteTopology ι
Tactic: haveI h : DiscreteTopology ι := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
this : TopologicalSpace ι := ⊥
h : DiscreteTopology ι
⊢ IsCompact (insert x (range f))
have hf₁ : Tendsto f (cocompact ι) (𝓝 x)
Tactic: rw [← cocompact_eq_cofinite ι] at hf
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
⊢ (coclosedCompact X).HasBasis (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsCompact s) compl
have simp : HasBasis (⨅ (s : Set X), ⨅ (_ : IsClosed[inst] s ∧ IsCompact s), 𝓟 sᶜ)
  (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsCompact s) compl
Tactic: simp only [Filter.coclosedCompact, iInf_and']
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
⊢ HasBasis (⨅ (s : Set X), ⨅ (_ : IsClosed[inst] s ∧ IsCompact s), 𝓟 sᶜ)
    (fun (s : Set X) ↦ IsClosed[inst] s ∧ IsCompact s) compl
have refine : ∀ (i : Set X),
  IsClosed[inst] i ∧ IsCompact i →
    ∀ (j : Set X), IsClosed[inst] j ∧ IsCompact j → ∃ (k : Set X), (IsClosed[inst] k ∧ IsCompact k) ∧ kᶜ ⊆ iᶜ ∧ kᶜ ⊆ jᶜ
Tactic: refine hasBasis_biInf_principal' ?_ ⟨∅, isClosed_empty, isCompact_empty⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ s ∈ coclosedCompact X ↔ IsCompact (closure[inst] sᶜ)
have refine_1 : (∃ (i : Set X), (IsClosed[inst] i ∧ IsCompact i) ∧ iᶜ ⊆ s) → IsCompact (closure[inst] sᶜ)
Tactic: refine hasBasis_coclosedCompact.mem_iff.trans ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
refine_1 : (∃ (i : Set X), (IsClosed[inst] i ∧ IsCompact i) ∧ iᶜ ⊆ s) → IsCompact (closure[inst] sᶜ)
⊢ s ∈ coclosedCompact X ↔ IsCompact (closure[inst] sᶜ)
have refine_2 : ∀ (h : IsCompact (closure[inst] sᶜ)), ∃ (i : Set X), (IsClosed[inst] i ∧ IsCompact i) ∧ iᶜ ⊆ s
Tactic: refine hasBasis_coclosedCompact.mem_iff.trans ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ sᶜ ∈ coclosedCompact X ↔ IsCompact (closure[inst] s)
have rw : IsCompact (closure[inst] sᶜᶜ) ↔ IsCompact (closure[inst] s)
Tactic: rw [mem_coclosedCompact_iff, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : IsCompact (closure[inst] sᶜᶜ) ↔ IsCompact (closure[inst] s)
⊢ sᶜ ∈ coclosedCompact X ↔ IsCompact (closure[inst] s)
have rw₁ : IsCompact (closure[inst] s) ↔ IsCompact (closure[inst] s)
Tactic: rw [mem_coclosedCompact_iff, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ sᶜ ∈ cocompact X ↔ ∃ (t : Set X), IsCompact t ∧ s ⊆ t
have rw : (∃ (t : Set X), IsCompact t ∧ tᶜ ⊆ sᶜ) ↔ ∃ (t : Set X), IsCompact t ∧ s ⊆ t
Tactic: rw [Filter.mem_cocompact]
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
hf : ∀ (x : X), ∃ t ∈ 𝓝 x, IsBounded (f '' t)
⊢ IsBounded (f '' s)
have choose : ∀ (U : (x : X) → Set X) (hU : ∀ (x : X), U x ∈ 𝓝 x ∧ IsBounded (f '' U x)), IsBounded (f '' s)
Tactic: choose U hU using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (goal)
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
U : (x : X) → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x ∧ IsBounded (f '' U x)
⊢ IsBounded (f '' s)
have obtain : ∀ (I : Finset X) (hI : (∀ x ∈ I, x ∈ s) ∧ s ⊆ ⋃ x ∈ I, U x), IsBounded (f '' s)
Tactic: obtain ⟨I, hI⟩ := hs.elim_nhds_subcover U (fun x _ => (hU x).1)
-- Lean 4 proof step from Mathlib.Topology.Compactness.Compact (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type u_2
inst_1 : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
U : (x : X) → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x ∧ IsBounded (f '' U x)
I : Finset X
hI : (∀ x ∈ I, x ∈ s) ∧ s ⊆ ⋃ x ∈ I, U x
⊢ IsBounded (f '' s)
have this : f '' ⋃ x ∈ I, U x = ⋃ x ∈ I, f '' U x
Tactic: have : f '' ⋃ x ∈ I, U x = ⋃ x ∈ I, f '' U x := by simp [Set.image_iUnion₂]