awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsCompact s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Finset X
left : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, {x}
⊢ s ⊆ (↑t : Set X)

Tactic:
simp only [← t.set_biUnion_coe, biUnion_of_singleton] at hst

Premises used: Finset.set_biUnion_coe, Set.biUnion_of_singleton
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsCompact s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Finset X
left : ∀ x ∈ t, x ∈ s
hst : s ⊆ (↑t : Set X)
⊢ s.Finite

Tactic:
t.finite_toSet.subset hst

Premises used: Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
hs : IsCompact s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Finset X
left : ∀ x ∈ t, x ∈ s
hst : s ⊆ (↑t : Set X)
⊢ s.Finite

Tactic:
exact t.finite_toSet.subset hst

Premises used: Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : DiscreteTopology X
⊢ IsCompact s ↔ s.Finite

Tactic:
⟨fun h => h.finite_of_discrete, fun h => h.isCompact⟩

Premises used: Set.Finite.isCompact, Iff.intro, IsCompact.finite_of_discrete
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
rw : IsCompact.{u} (X := X) (⋃ (b : Bool), bif b then s else t)
⊢ IsCompact (s ∪ t)

Tactic:
rw [union_eq_iUnion]

Premises used: Set.union_eq_iUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
b : Bool
false : IsCompact (bif Bool.false then s else t)
true : IsCompact (bif Bool.true then s else t)
⊢ IsCompact (bif b then s else t)

Tactic:
cases b
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (bif false then s else t)

Tactic:
assumption
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (bif true then s else t)

Tactic:
assumption
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact.{u} (X := X) (⋃ (b : Bool), bif b then s else t)

Tactic:
exact isCompact_iUnion fun b => by cases b <;> assumption

Premises used: isCompact_iUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
a : X
⊢ IsCompact (insert a s)

Tactic:
isCompact_singleton.union hs

Premises used: Set.insert, Set.Mem, setOf, isCompact_singleton, Set.singleton, IsCompact.union
-- Module: Mathlib.Topology.Compactness.Compact
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
obtain : ∀ (W : Set X) (hsubW : ⋂ (i : ι), V i ⊆ W) (W_op : IsOpen[inst] W) (hWU : W ⊆ U), ∃ (i : ι), V i ⊆ U
⊢ ∃ (i : ι), V i ⊆ U

Tactic:
obtain ⟨W, hsubW, W_op, hWU⟩ := exists_open_set_nhds hU

Premises used: exists_open_set_nhds
-- Module: Mathlib.Topology.Compactness.Compact
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
suffices : ∃ (i : ι), V i ⊆ W
⊢ ∃ (i : ι), V i ⊆ U

Tactic:
suffices ∃ i, V i ⊆ W from this.imp fun i hi => hi.trans hWU
-- Module: Mathlib.Topology.Compactness.Compact
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
by_contra! : ∀ (H : ∀ (i : ι), ¬V i ⊆ W), False
⊢ ∃ (i : ι), V i ⊆ W

Tactic:
by_contra! H
-- Module: Mathlib.Topology.Compactness.Compact
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
⊢ ∀ (i : ι), (V i ∩ Wᶜ).Nonempty

Tactic:
replace H : ∀ i, (V i ∩ Wᶜ).Nonempty := fun i => Set.inter_compl_nonempty_iff.mpr (H i)
-- Module: Mathlib.Topology.Compactness.Compact
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
⊢ Set.Nonempty.{u} (α := X) (⋂ (i : ι), V i ∩ Wᶜ)

Tactic:
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

Premises used: IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, IsOpen.isClosed_compl, IsCompact.inter_right, IsClosed.inter
-- Module: Mathlib.Topology.Compactness.Compact
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 : ι),
    ∃ (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ᶜ)
⊢ Set.Nonempty.{u} (α := X) (⋂ (i : ι), V i ∩ Wᶜ)

Tactic:
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

Premises used: IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, IsOpen.isClosed_compl, IsCompact.inter_right, IsClosed.inter
-- Module: Mathlib.Topology.Compactness.Compact
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 : ι
rcases :
  ∀ (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ᶜ)
⊢ ∃ (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ᶜ)

Tactic:
rcases hV i j with ⟨k, hki, hkj⟩
-- Module: Mathlib.Topology.Compactness.Compact
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ᶜ)

Tactic:
⟨k, ⟨fun x => ?_, fun x => ?_⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Compact
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ᶜ
refine_2 : ∀ x ∈ V k ∩ Wᶜ, x ∈ V j ∩ 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ᶜ)

Tactic:
refine ⟨k, ⟨fun x => ?_, fun x => ?_⟩⟩
-- Module: Mathlib.Topology.Compactness.Compact
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 : x ∈ V k → x ∉ W → x ∈ V i ∧ x ∉ W
⊢ x ∈ V k ∩ Wᶜ → x ∈ V i ∩ Wᶜ

Tactic:
simp only [and_imp, mem_inter_iff, mem_compl_iff]

Premises used: and_imp, Set.mem_inter_iff, Set.mem_compl_iff
-- Module: Mathlib.Topology.Compactness.Compact
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 : x ∈ V k → x ∉ W → x ∈ V j ∧ x ∉ W
⊢ x ∈ V k ∩ Wᶜ → x ∈ V j ∩ Wᶜ

Tactic:
simp only [and_imp, mem_inter_iff, mem_compl_iff]

Premises used: and_imp, Set.mem_inter_iff, Set.mem_compl_iff
-- Module: Mathlib.Topology.Compactness.Compact
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
refine_1₃ : x ∈ V k → x ∉ W → x ∉ W
refine_1₄ refine_1₅ refine_1₆ refine_1₇ refine_1₈ : x ∈ V k → x ∉ W → x ∈ V i
⊢ x ∈ V k → x ∉ W → x ∈ V i ∧ x ∉ W

Tactic:
tauto
-- Module: Mathlib.Topology.Compactness.Compact
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
refine_2₃ : x ∈ V k → x ∉ W → x ∉ W
refine_2₄ refine_2₅ refine_2₆ refine_2₇ refine_2₈ : x ∈ V k → x ∉ W → x ∈ V j
⊢ x ∈ V k → x ∉ W → x ∈ V j ∧ x ∉ W

Tactic:
tauto
-- Module: Mathlib.Topology.Compactness.Compact
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
⊢ 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
-- Module: Mathlib.Topology.Compactness.Compact
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ᶜ)
⊢ ¬⋂ (i : ι), V i ⊆ W

Tactic:
simpa [← iInter_inter, inter_compl_nonempty_iff]

Premises used: Set.iInter_inter, Set.inter_compl_nonempty_iff
-- Module: Mathlib.Topology.Compactness.Compact
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ᶜ)
⊢ ¬⋂ (i : ι), V i ⊆ W

Tactic:
have : ¬⋂ i : ι, V i ⊆ W := by simpa [← iInter_inter, inter_compl_nonempty_iff]
-- Module: Mathlib.Topology.Compactness.Compact
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_1 : Set.Nonempty.{u} (α := X) (⋂ (i : ι), V i ∩ Wᶜ)
this : ¬⋂ (i : ι), V i ⊆ W
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Topology.Compactness.Compact
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
rw : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
⊢ IsCompact s

Tactic:
rw [isCompact_iff_ultrafilter_le_nhds', hTS]

Premises used: isCompact_iff_ultrafilter_le_nhds'
-- Module: Mathlib.Topology.Compactness.Compact
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
by_contra : ∀ (hF : ¬∃ x ∈ s, (↑F : Filter X) ≤ 𝓝 x), False
⊢ ∃ x ∈ s, (↑F : Filter X) ≤ 𝓝 x

Tactic:
by_contra hF
-- Module: Mathlib.Topology.Compactness.Compact
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
⊢ ∀ x ∈ s, ∃ (t : Set X), x ∈ t ∧ t ∈ S ∧ t ∉ F

Tactic:
simpa [nhds_generateFrom] using hF

Premises used: TopologicalSpace.nhds_generateFrom
-- Module: Mathlib.Topology.Compactness.Compact
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
⊢ ∀ 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
-- Module: Mathlib.Topology.Compactness.Compact
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
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
⊢ False

Tactic:
choose! U hxU hSU hUF using hSF
-- Module: Mathlib.Topology.Compactness.Compact
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
⊢ U '' s ⊆ S

Tactic:
simpa [Set.subset_def]

Premises used: Set.subset_def
-- Module: Mathlib.Topology.Compactness.Compact
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
x : X
hx : x ∈ s
⊢ U x ∈ U '' s

Tactic:
grind
-- Module: Mathlib.Topology.Compactness.Compact
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
obtain : ∀ (Q : Set (Set X)) (hQU : Q ⊆ U '' s) (hQ : Q.Finite) (hsQ : s ⊆ ⋃₀ Q), False
⊢ 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))

Premises used: Set.mem_sUnion_of_mem, Set.image
-- Module: Mathlib.Topology.Compactness.Compact
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
⊢ ∀ s ∈ Q, s ∉ F

Tactic:
have : ∀ s ∈ Q, s ∉ F := fun s hsQ ↦ (hQU hsQ).choose_spec.2 ▸ hUF _ (hQU hsQ).choose_spec.1
-- Module: Mathlib.Topology.Compactness.Compact
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
⊢ ⋂₀ (compl '' Q) ∈ (↑F : Filter X).sets

Tactic:
simpa [Filter.biInter_mem hQ, F.compl_mem_iff_notMem]

Premises used: Filter.biInter_mem, Ultrafilter.compl_mem_iff_notMem
-- Module: Mathlib.Topology.Compactness.Compact
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
⊢ ⋂₀ (compl '' Q) ∈ (↑F : Filter X).sets

Tactic:
have hQF : ⋂₀ (compl '' Q) ∈ F.sets := by simpa [Filter.biInter_mem hQ, F.compl_mem_iff_notMem]
-- Module: Mathlib.Topology.Compactness.Compact
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
⊢ ⋃₀ Q ∉ F

Tactic:
simpa [-Set.sInter_image, ← Set.compl_sUnion, hsQ, F.compl_mem_iff_notMem] using hQF

Premises used: Set.compl_sUnion, Set.sInter_image, Ultrafilter.compl_mem_iff_notMem
-- Module: Mathlib.Topology.Compactness.Compact
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
⊢ ⋃₀ Q ∉ F

Tactic:
have : ⋃₀ Q ∉ F := by
    simpa [-Set.sInter_image, ← Set.compl_sUnion, hsQ, F.compl_mem_iff_notMem] using hQF
-- Module: Mathlib.Topology.Compactness.Compact
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_1 : ∀ s ∈ Q, s ∉ F
hQF : ⋂₀ (compl '' Q) ∈ (↑F : Filter X).sets
this : ⋃₀ Q ∉ F
⊢ False

Tactic:
this (F.mem_of_superset hsF hsQ)

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.Compactness.Compact
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_1 : ∀ s ∈ Q, s ∉ F
hQF : ⋂₀ (compl '' Q) ∈ (↑F : Filter X).sets
this : ⋃₀ Q ∉ F
⊢ False

Tactic:
exact this (F.mem_of_superset hsF hsQ)

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h :
  ∀ (ι : Type u) (U : ι → (↑S : Type u)),
    s ⊆ ⋃ (i : ι), (↑(U i) : Set X) → ∃ (J : Set ι), J.Finite ∧ s ⊆ ⋃ i ∈ J, (↑(U i) : Set X)
P : Set (Set X)
hP : P ⊆ S
hs : s ⊆ ⋃₀ P
J : Set (↑P : Type u)
hJ : J.Finite
cover : s ⊆ ⋃ i ∈ J, (↑(Subtype.mk (p := fun (x : Set X) ↦ x ∈ S) (↑i : Set X) ⋯) : Set X)
⊢ (fun (x : (↑P : Type u)) ↦ (↑x : Set X)) '' J ⊆ P

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h :
  ∀ (ι : Type u) (U : ι → (↑S : Type u)),
    s ⊆ ⋃ (i : ι), (↑(U i) : Set X) → ∃ (J : Set ι), J.Finite ∧ s ⊆ ⋃ i ∈ J, (↑(U i) : Set X)
P : Set (Set X)
hP : P ⊆ S
hs : s ⊆ ⋃₀ P
J : Set (↑P : Type u)
hJ : J.Finite
cover : s ⊆ ⋃ i ∈ J, (↑(Subtype.mk (p := fun (x : Set X) ↦ x ∈ S) (↑i : Set X) ⋯) : Set X)
⊢ s ⊆ ⋃₀ ((fun (x : (↑P : Type u)) ↦ (↑x : Set X)) '' J)

Tactic:
aesop
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
⊢ (cocompact X).HasBasis IsCompact compl

Tactic:
hasBasis_biInf_principal'
    (fun s hs t ht =>
      ⟨s ∪ t, hs.union ht, compl_subset_compl.2 subset_union_left,
        compl_subset_compl.2 subset_union_right⟩)
    ⟨∅, isCompact_empty⟩

Premises used: Iff.mpr, Set.subset_union_right, Set.compl_subset_compl, Filter.cocompact, Set.subset_union_left, Filter.hasBasis_biInf_principal', And.intro, Exists.intro, IsCompact.union, Union.union, EmptyCollection.emptyCollection, isCompact_empty