awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ (↑f : Filter (X i)) → ∃ x ∈ s i, (↑f : Filter (X i)) ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} ∈ (↑f : Filter ((i : ι) → X i))
this : ∀ (i : ι), ∃ x ∈ s i, Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 x)
choose :
  ∀ (x : (i : ι) → X i) (hx : ∀ (i : ι), x i ∈ s i ∧ Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 (x i))),
    ∃ (x : (i : ι) → X i),
      Membership.mem (γ := Set ((i : ι) → X i)) {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} x ∧
        ∀ (i : ι), Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 (x i))
⊢ ∃ (x : (i : ι) → X i),
    Membership.mem (γ := Set ((i : ι) → X i)) {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} x ∧
      ∀ (i : ι), Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 (x i))

Tactic:
choose x hx using this
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ (↑f : Filter (X i)) → ∃ x ∈ s i, (↑f : Filter (X i)) ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} ∈ (↑f : Filter ((i : ι) → X i))
x : (i : ι) → X i
hx : ∀ (i : ι), x i ∈ s i ∧ Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 (x i))
⊢ ∃ (x : (i : ι) → X i),
    Membership.mem (γ := Set ((i : ι) → X i)) {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} x ∧
      ∀ (i : ι), Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 (x i))

Tactic:
⟨x, fun i => (hx i).left, fun i => (hx i).right⟩

Premises used: And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι) (f : Ultrafilter (X i)), s i ∈ (↑f : Filter (X i)) → ∃ x ∈ s i, (↑f : Filter (X i)) ≤ 𝓝 x
f : Ultrafilter ((i : ι) → X i)
hfs : {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} ∈ (↑f : Filter ((i : ι) → X i))
x : (i : ι) → X i
hx : ∀ (i : ι), x i ∈ s i ∧ Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 (x i))
⊢ ∃ (x : (i : ι) → X i),
    Membership.mem (γ := Set ((i : ι) → X i)) {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i} x ∧
      ∀ (i : ι), Tendsto (eval (β := X) i) (↑f : Filter ((i : ι) → X i)) (𝓝 (x i))

Tactic:
exact ⟨x, fun i => (hx i).left, fun i => (hx i).right⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι), IsCompact (s i)
⊢ IsCompact (X := (i : ι) → X i) {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i}

Tactic:
isCompact_pi_infinite h

Premises used: isCompact_pi_infinite
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι), IsCompact (s i)
h₁ : Set.pi (α := X) univ s = {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i}
⊢ IsCompact (Set.pi (α := X) univ s)

Tactic:
convert! isCompact_pi_infinite h

Premises used: isCompact_pi_infinite
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι), IsCompact (s i)
⊢ Set.pi (α := X) univ s = {x : (i : ι) → X i | ∀ (i : ι), x i ∈ s i}

Tactic:
simp only [← mem_univ_pi, setOf_mem_eq]

Premises used: Set.setOf_mem_eq, Set.mem_univ_pi
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
f : X_1 → Y
X : ι → Type u_2
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), CompactSpace.{u_2} (X i)
rw : IsCompact (X := (i : ι) → X i) (Set.pi (α := X) univ fun (i : ι) ↦ univ)
⊢ IsCompact (X := (i : ι) → X i) univ

Tactic:
rw [← pi_univ univ]

Premises used: Set.univ, Set.pi_univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
f : X_1 → Y
X : ι → Type u_2
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), CompactSpace.{u_2} (X i)
⊢ IsCompact (X := (i : ι) → X i) (Set.pi (α := X) univ fun (i : ι) ↦ univ)

Tactic:
isCompact_univ_pi fun i => isCompact_univ

Premises used: isCompact_univ_pi, isCompact_univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
f : X_1 → Y
X : ι → Type u_2
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), CompactSpace.{u_2} (X i)
⊢ IsCompact (X := (i : ι) → X i) (Set.pi (α := X) univ fun (i : ι) ↦ univ)

Tactic:
exact isCompact_univ_pi fun i => isCompact_univ

Premises used: isCompact_univ_pi, isCompact_univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X_1 : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
f : X_1 → Y
X : ι → Type u_2
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : CompactSpace Y
⊢ CompactSpace (ι → Y)

Tactic:
Pi.compactSpace

Premises used: Pi.compactSpace
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
mp : IsCompact s → ∀ (i : ι), IsCompact (eval (β := X) i '' s)
mpr : (∀ (i : ι), IsCompact (eval (β := X) i '' s)) → IsCompact s
⊢ IsCompact s ↔ ∀ (i : ι), IsCompact (eval (β := X) i '' s)

Tactic:
constructor
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
H : IsCompact s
⊢ ∀ (i : ι), IsCompact (eval (β := X) i '' s)

Tactic:
fun i ↦ H.image <| continuous_apply i

Premises used: continuous_apply, IsCompact.image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
H : IsCompact s
⊢ ∀ (i : ι), IsCompact (eval (β := X) i '' s)

Tactic:
exact fun i ↦ H.image <| continuous_apply i

Premises used: continuous_apply, IsCompact.image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
H : ∀ (i : ι), IsCompact (eval (β := X) i '' s)
⊢ IsCompact s

Tactic:
IsCompact.of_isClosed_subset (isCompact_univ_pi H) hs (subset_pi_eval_image univ s)

Premises used: Set.univ, isCompact_univ_pi, IsCompact.of_isClosed_subset, Set.subset_pi_eval_image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
H : ∀ (i : ι), IsCompact (eval (β := X) i '' s)
⊢ IsCompact s

Tactic:
exact IsCompact.of_isClosed_subset (isCompact_univ_pi H) hs (subset_pi_eval_image univ s)

Premises used: Set.univ, isCompact_univ_pi, IsCompact.of_isClosed_subset, Set.subset_pi_eval_image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
mp :
  (∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K) →
    ∀ (i : ι), ∃ (Ki : Set (X i)), IsCompact Ki ∧ s ⊆ eval (β := X) i ⁻¹' Ki
mpr :
  (∀ (i : ι), ∃ (Ki : Set (X i)), IsCompact Ki ∧ s ⊆ eval (β := X) i ⁻¹' Ki) →
    ∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K
⊢ (∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K) ↔
    ∀ (i : ι), ∃ (Ki : Set (X i)), IsCompact Ki ∧ s ⊆ eval (β := X) i ⁻¹' Ki

Tactic:
constructor
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s K : Set ((i : ι) → X i)
hK : IsCompact K
hsK : s ⊆ K
i : ι
⊢ ∃ (Ki : Set (X i)), IsCompact Ki ∧ s ⊆ eval (β := X) i ⁻¹' Ki

Tactic:
⟨eval i '' K, hK.image <| continuous_apply i, hsK.trans <| K.subset_preimage_image _⟩

Premises used: HasSubset.Subset.trans, Function.eval, And.intro, Exists.intro, continuous_apply, Set.image, IsCompact.image, Set.subset_preimage_image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s K : Set ((i : ι) → X i)
hK : IsCompact K
hsK : s ⊆ K
i : ι
⊢ ∃ (Ki : Set (X i)), IsCompact Ki ∧ s ⊆ eval (β := X) i ⁻¹' Ki

Tactic:
exact ⟨eval i '' K, hK.image <| continuous_apply i, hsK.trans <| K.subset_preimage_image _⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
H : ∀ (i : ι), ∃ (Ki : Set (X i)), IsCompact Ki ∧ s ⊆ eval (β := X) i ⁻¹' Ki
mpr :
  ∀ (K : (i : ι) → Set (X i)) (hK : ∀ (i : ι), IsCompact (K i)) (hsK : ∀ (i : ι), s ⊆ eval (β := X) i ⁻¹' K i),
    ∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K
⊢ ∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K

Tactic:
choose K hK hsK using H
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
K : (i : ι) → Set (X i)
hK : ∀ (i : ι), IsCompact (K i)
hsK : ∀ (i : ι), s ⊆ eval (β := X) i ⁻¹' K i
⊢ ∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K

Tactic:
⟨pi univ K, isCompact_univ_pi hK, fun _ hx i _ ↦ hsK i hx⟩

Premises used: Set.univ, isCompact_univ_pi, And.intro, Exists.intro, Set.pi
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
K : (i : ι) → Set (X i)
hK : ∀ (i : ι), IsCompact (K i)
hsK : ∀ (i : ι), s ⊆ eval (β := X) i ⁻¹' K i
⊢ ∃ (K : Set ((i : ι) → X i)), IsCompact K ∧ s ⊆ K

Tactic:
exact ⟨pi univ K, isCompact_univ_pi hK, fun _ hx i _ ↦ hsK i hx⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_3
inst : (d : ι) → TopologicalSpace (X d)
⊢ Eq (α := Filter ((i : ι) → X i)) (Filter.coprodᵢ (α := X) fun (d : ι) ↦ cocompact (X d)) (cocompact ((d : ι) → X d))

Tactic:
le_antisymm (iSup_le fun i => Filter.comap_cocompact_le (continuous_apply i)) ?_

Premises used: Filter.comap_cocompact_le, le_antisymm, iSup_le, continuous_apply
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_3
inst : (d : ι) → TopologicalSpace (X d)
refine :
  LE.le (α := Filter ((i : ι) → X i)) (cocompact ((d : ι) → X d))
    (Filter.coprodᵢ (α := X) fun (d : ι) ↦ cocompact (X d))
⊢ Eq (α := Filter ((i : ι) → X i)) (Filter.coprodᵢ (α := X) fun (d : ι) ↦ cocompact (X d)) (cocompact ((d : ι) → X d))

Tactic:
refine le_antisymm (iSup_le fun i => Filter.comap_cocompact_le (continuous_apply i)) ?_

Premises used: Filter.comap_cocompact_le, le_antisymm, iSup_le, continuous_apply
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_3
inst : (d : ι) → TopologicalSpace (X d)
⊢ LE.le (α := Filter ((i : ι) → X i)) (cocompact ((d : ι) → X d))
    (Filter.coprodᵢ (α := X) fun (d : ι) ↦ cocompact (X d))

Tactic:
compl_surjective.forall.2 fun s H => ?_

Premises used: Iff.mpr, Function.Surjective.forall, compl_surjective
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_3
inst : (d : ι) → TopologicalSpace (X d)
refine :
  ∀ (s : Set ((i : ι) → X i))
    (H : Membership.mem (γ := Filter ((i : ι) → X i)) (Filter.coprodᵢ (α := X) fun (d : ι) ↦ cocompact (X d)) sᶜ),
    Membership.mem (γ := Filter ((i : ι) → X i)) (cocompact ((d : ι) → X d)) sᶜ
⊢ LE.le (α := Filter ((i : ι) → X i)) (cocompact ((d : ι) → X d))
    (Filter.coprodᵢ (α := X) fun (d : ι) ↦ cocompact (X d))

Tactic:
refine compl_surjective.forall.2 fun s H => ?_

Premises used: Iff.mpr, Function.Surjective.forall, compl_surjective
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_3
inst : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
H : Membership.mem (γ := Filter ((i : ι) → X i)) (Filter.coprodᵢ (α := X) fun (d : ι) ↦ cocompact (X d)) sᶜ
simp :
  ∀ (H : ∀ (i : ι), ∃ (t : Set (X i)), IsCompact t ∧ s ⊆ eval (β := X) i ⁻¹' t),
    ∃ (t : Set ((d : ι) → X d)), IsCompact t ∧ s ⊆ t
⊢ Membership.mem (γ := Filter ((i : ι) → X i)) (cocompact ((d : ι) → X d)) sᶜ

Tactic:
simp only [compl_mem_coprodᵢ, Filter.mem_cocompact, compl_subset_compl, image_subset_iff] at H ⊢

Premises used: Filter.compl_mem_coprodᵢ, Set.compl_subset_compl, Set.image_subset_iff, Filter.mem_cocompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_3
inst : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
H : ∀ (i : ι), ∃ (t : Set (X i)), IsCompact t ∧ s ⊆ eval (β := X) i ⁻¹' t
choose :
  ∀ (K : (i : ι) → Set (X i)) (hKc : ∀ (i : ι), IsCompact (K i)) (htK : ∀ (i : ι), s ⊆ eval (β := X) i ⁻¹' K i),
    ∃ (t : Set ((d : ι) → X d)), IsCompact t ∧ s ⊆ t
⊢ ∃ (t : Set ((d : ι) → X d)), IsCompact t ∧ s ⊆ t

Tactic:
choose K hKc htK using H
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_3
inst : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
K : (i : ι) → Set (X i)
hKc : ∀ (i : ι), IsCompact (K i)
htK : ∀ (i : ι), s ⊆ eval (β := X) i ⁻¹' K i
⊢ ∃ (t : Set ((d : ι) → X d)), IsCompact t ∧ s ⊆ t

Tactic:
⟨Set.pi univ K, isCompact_univ_pi hKc, fun f hf i _ => htK i hf⟩

Premises used: Set.univ, isCompact_univ_pi, And.intro, Exists.intro, Set.pi
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
ι : Type u_1
X : ι → Type u_3
inst : (d : ι) → TopologicalSpace (X d)
s : Set ((i : ι) → X i)
K : (i : ι) → Set (X i)
hKc : ∀ (i : ι), IsCompact (K i)
htK : ∀ (i : ι), s ⊆ eval (β := X) i ⁻¹' K i
⊢ ∃ (t : Set ((d : ι) → X d)), IsCompact t ∧ s ⊆ t

Tactic:
exact ⟨Set.pi univ K, isCompact_univ_pi hKc, fun f hf i _ => htK i hf⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
r : X → X → Prop
inst_2 : CompactSpace X
rw : IsCompact (range (mk r))
⊢ IsCompact.{u} (X := Quot r) univ

Tactic:
rw [← range_quot_mk]

Premises used: Set.range_quot_mk
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
r : X → X → Prop
inst_2 : CompactSpace X
⊢ IsCompact (range (mk r))

Tactic:
isCompact_range continuous_quot_mk

Premises used: isCompact_range, continuous_quot_mk
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
r : X → X → Prop
inst_2 : CompactSpace X
⊢ IsCompact (range (mk r))

Tactic:
exact isCompact_range continuous_quot_mk

Premises used: isCompact_range, continuous_quot_mk
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s_1 t : Set X
f : X → Y
s : Setoid X
inst_2 : CompactSpace X
⊢ CompactSpace.{u} (Quotient s)

Tactic:
Quot.compactSpace

Premises used: Quotient, Quotient.mk', Quot.compactSpace
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
pos : ∀ (hcne : c.Nonempty), ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
neg : ∀ (hcne : ¬c.Nonempty), ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub

Tactic:
by_cases hcne : c.Nonempty

Premises used: Set.Nonempty
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
hcne : c.Nonempty
pos : ∀ (U₀ : Set X) (hU₀ : U₀ ∈ c), ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub

Tactic:
obtain ⟨U₀, hU₀⟩ := hcne
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
⊢ Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }

Tactic:
haveI : Nonempty { U // U ∈ c } := ⟨⟨U₀, hU₀⟩⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
⊢ Sᶜ ⊆ U₀

Tactic:
obtain ⟨U₀compl, -, -⟩ := hc hU₀
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
h : ⋃₀ c ∈ opens ∧ ∀ s ∈ c, s ⊆ ⋃₀ c
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub

Tactic:
use ⋃₀ c
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ ⋃₀ c ∈ opens ∧ ∀ s ∈ c, s ⊆ ⋃₀ c

Tactic:
⟨⟨?_, ?_, ?_⟩, fun U hU _ hx => ⟨U, hU, hx⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
h : Sᶜ ⊆ ⋃₀ c
h₁ : IsOpen[inst] (⋃₀ c)
h₂ : (⋃₀ c)ᶜ.Nonempty
⊢ ⋃₀ c ∈ opens ∧ ∀ s ∈ c, s ⊆ ⋃₀ c

Tactic:
refine ⟨⟨?_, ?_, ?_⟩, fun U hU _ hx => ⟨U, hU, hx⟩⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ Sᶜ ⊆ ⋃₀ c

Tactic:
fun _ hx => ⟨U₀, hU₀, U₀compl hx⟩

Premises used: Set.Mem, setOf, Set.sUnion, Set.Subset, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ Sᶜ ⊆ ⋃₀ c

Tactic:
exact fun _ hx => ⟨U₀, hU₀, U₀compl hx⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ IsOpen[inst] (⋃₀ c)

Tactic:
isOpen_sUnion fun _ h => (hc h).2.1

Premises used: And.right, And.left, isOpen_sUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ IsOpen[inst] (⋃₀ c)

Tactic:
exact isOpen_sUnion fun _ h => (hc h).2.1

Premises used: And.right, And.left, isOpen_sUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
h : (⋃₀ c)ᶜ = ⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ
h₁ : Set.Nonempty.{u} (α := X) (⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ)
⊢ (⋃₀ c)ᶜ.Nonempty

Tactic:
convert_to (⋂ U : { U // U ∈ c }, U.1ᶜ).Nonempty

Premises used: Set.iInter, Compl.compl, Set.Nonempty, Subtype.val
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
h : ∀ (x : X), x ∈ (⋃₀ c)ᶜ ↔ Membership.mem (γ := Set X) (⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ) x
⊢ (⋃₀ c)ᶜ = ⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ

Tactic:
ext
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
x : X
⊢ x ∈ (⋃₀ c)ᶜ ↔ Membership.mem (γ := Set X) (⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ) x

Tactic:
simp only [not_exists, not_and, Set.mem_iInter, Subtype.forall,
              mem_compl_iff, mem_sUnion]

Premises used: not_exists, Subtype.forall, Set.mem_iInter, Set.mem_sUnion, not_and, Set.mem_compl_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
S : Set X
hS : IsClosed[inst] S
hne : S.Nonempty
opens : Set (Set X) := {U : Set X | Sᶜ ⊆ U ∧ IsOpen[inst] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty.{max 1 (u + 1)} { U : Set X // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
h : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ
h₁ : ∀ (i : { U : Set X // U ∈ c }), (↑i : Set X)ᶜ.Nonempty
h₂ : ∀ (i : { U : Set X // U ∈ c }), IsCompact (↑i : Set X)ᶜ
h₃ : ∀ (i : { U : Set X // U ∈ c }), IsClosed[inst] (↑i : Set X)ᶜ
⊢ Set.Nonempty.{u} (α := X) (⋂ (U : { U : Set X // U ∈ c }), (↑U : Set X)ᶜ)

Tactic:
apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed

Premises used: IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed