awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀
U : Set X
hU : U ∈ c
U' : Set X
hU' : U' ∈ c
h :
  ∀ (V : Set X) (hVc : V ∈ c) (hVU : U ⊆ V) (hVU' : U' ⊆ V),
    ∃ (z : { U : Set X // U ∈ c }),
      (fun (x1 x2 : Set X) ↦ x1 ⊇ x2)
          ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) (Subtype.mk (p := fun (U : Set X) ↦ U ∈ c) U hU))
          ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) z) ∧
        (fun (x1 x2 : Set X) ↦ x1 ⊇ x2)
          ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) (Subtype.mk (p := fun (U : Set X) ↦ U ∈ c) U' hU'))
          ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) z)
⊢ ∃ (z : { U : Set X // U ∈ c }),
    (fun (x1 x2 : Set X) ↦ x1 ⊇ x2)
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) (Subtype.mk (p := fun (U : Set X) ↦ U ∈ c) U hU))
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) z) ∧
      (fun (x1 x2 : Set X) ↦ x1 ⊇ x2)
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) (Subtype.mk (p := fun (U : Set X) ↦ U ∈ c) U' hU'))
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) z)

Tactic:
obtain ⟨V, hVc, hVU, hVU'⟩ := hz.directedOn U hU U' hU'

Premises used: IsChain.directedOn
-- 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₀
U : Set X
hU : U ∈ c
U' : Set X
hU' : U' ∈ c
V : Set X
hVc : V ∈ c
hVU : U ⊆ V
hVU' : U' ⊆ V
⊢ ∃ (z : { U : Set X // U ∈ c }),
    (fun (x1 x2 : Set X) ↦ x1 ⊇ x2)
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) (Subtype.mk (p := fun (U : Set X) ↦ U ∈ c) U hU))
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) z) ∧
      (fun (x1 x2 : Set X) ↦ x1 ⊇ x2)
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) (Subtype.mk (p := fun (U : Set X) ↦ U ∈ c) U' hU'))
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) z)

Tactic:
⟨⟨V, hVc⟩, Set.compl_subset_compl.mpr hVU, Set.compl_subset_compl.mpr hVU'⟩

Premises used: Iff.mpr, Set.compl_subset_compl, Subtype.mk, 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₀
U : Set X
hU : U ∈ c
U' : Set X
hU' : U' ∈ c
V : Set X
hVc : V ∈ c
hVU : U ⊆ V
hVU' : U' ⊆ V
⊢ ∃ (z : { U : Set X // U ∈ c }),
    (fun (x1 x2 : Set X) ↦ x1 ⊇ x2)
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) (Subtype.mk (p := fun (U : Set X) ↦ U ∈ c) U hU))
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) z) ∧
      (fun (x1 x2 : Set X) ↦ x1 ⊇ x2)
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) (Subtype.mk (p := fun (U : Set X) ↦ U ∈ c) U' hU'))
        ((fun (i : { U : Set X // U ∈ c }) ↦ (↑i : Set X)ᶜ) z)

Tactic:
exact ⟨⟨V, hVc⟩, Set.compl_subset_compl.mpr hVU, Set.compl_subset_compl.mpr hVU'⟩
-- 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₀
⊢ ∀ (i : { U : Set X // U ∈ c }), (↑i : Set X)ᶜ.Nonempty

Tactic:
fun U => (hc U.2).2.2

Premises used: And.right, Subtype.property
-- 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₀
⊢ ∀ (i : { U : Set X // U ∈ c }), (↑i : Set X)ᶜ.Nonempty

Tactic:
exact fun U => (hc U.2).2.2

Premises used: And.right
-- 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₀
⊢ ∀ (i : { U : Set X // U ∈ c }), IsCompact (↑i : Set X)ᶜ

Tactic:
fun U => (hc U.2).2.1.isClosed_compl.isCompact

Premises used: IsOpen.isClosed_compl, And.right, And.left, IsClosed.isCompact, Subtype.property
-- 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₀
⊢ ∀ (i : { U : Set X // U ∈ c }), IsCompact (↑i : Set X)ᶜ

Tactic:
exact fun U => (hc U.2).2.1.isClosed_compl.isCompact

Premises used: IsOpen.isClosed_compl, And.right, And.left, IsClosed.isCompact
-- 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₀
⊢ ∀ (i : { U : Set X // U ∈ c }), IsClosed[inst] (↑i : Set X)ᶜ

Tactic:
fun U => (hc U.2).2.1.isClosed_compl

Premises used: IsOpen.isClosed_compl, And.right, And.left, Subtype.property
-- 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₀
⊢ ∀ (i : { U : Set X // U ∈ c }), IsClosed[inst] (↑i : Set X)ᶜ

Tactic:
exact fun U => (hc U.2).2.1.isClosed_compl

Premises used: IsOpen.isClosed_compl, And.right, And.left
-- 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
h : Sᶜ ∈ opens ∧ ∀ s ∈ c, s ⊆ Sᶜ
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub

Tactic:
use Sᶜ
-- 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
⊢ Sᶜ ∈ opens ∧ ∀ s ∈ c, s ⊆ Sᶜ

Tactic:
⟨⟨Set.Subset.refl _, isOpen_compl_iff.mpr hS, ?_⟩, fun U Uc => (hcne ⟨U, Uc⟩).elim⟩

Premises used: Iff.mpr, Set.Subset.refl, False.elim, And.intro, Exists.intro, isOpen_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
hcne : ¬c.Nonempty
h : Sᶜᶜ.Nonempty
⊢ Sᶜ ∈ opens ∧ ∀ s ∈ c, s ⊆ Sᶜ

Tactic:
refine ⟨⟨Set.Subset.refl _, isOpen_compl_iff.mpr hS, ?_⟩, fun U Uc => (hcne ⟨U, Uc⟩).elim⟩
-- 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
h : S.Nonempty
⊢ Sᶜᶜ.Nonempty

Tactic:
rw [compl_compl]

Premises used: compl_compl
-- 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
⊢ S.Nonempty

Tactic:
hne
-- 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
⊢ S.Nonempty

Tactic:
exact hne
-- 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}
obtain :
  ∀ (U : Set X) (h : Maximal (fun (x : Set X) ↦ x ∈ opens) U),
    ∃ V ⊆ S, V.Nonempty ∧ IsClosed[inst] V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst] V' → V' = V
⊢ ∃ V ⊆ S, V.Nonempty ∧ IsClosed[inst] V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst] V' → V' = V

Tactic:
obtain ⟨U, h⟩ :=
    zorn_subset opens fun c hc hz => by
      by_cases hcne : c.Nonempty
      · obtain ⟨U₀, hU₀⟩ := hcne
        haveI : Nonempty { U // U ∈ c } := ⟨⟨U₀, hU₀⟩⟩
        obtain ⟨U₀compl, -, -⟩ := hc hU₀
        use ⋃₀ c
        refine ⟨⟨?_, ?_, ?_⟩, fun U hU _ hx => ⟨U, hU, hx⟩⟩
        · exact fun _ hx => ⟨U₀, hU₀, U₀compl hx⟩
        · exact isOpen_sUnion fun _ h => (hc h).2.1
        · convert_to (⋂ U : { U // U ∈ c }, U.1ᶜ).Nonempty
          · ext
            simp only [not_exists, not_and, Set.mem_iInter, Subtype.forall,
              mem_compl_iff, mem_sUnion]
          apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
          · rintro ⟨U, hU⟩ ⟨U', hU'⟩
            obtain ⟨V, hVc, hVU, hVU'⟩ := hz.directedOn U hU U' hU'
            exact ⟨⟨V, hVc⟩, Set.compl_subset_compl.mpr hVU, Set.compl_subset_compl.mpr hVU'⟩
          · exact fun U => (hc U.2).2.2
          · exact fun U => (hc U.2).2.1.isClosed_compl.isCompact
          · exact fun U => (hc U.2).2.1.isClosed_compl
      · use Sᶜ
        refine ⟨⟨Set.Subset.refl _, isOpen_compl_iff.mpr hS, ?_⟩, fun U Uc => (hcne ⟨U, Uc⟩).elim⟩
        rw [compl_compl]
        exact hne

Premises used: zorn_subset
-- 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}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
⊢ Sᶜ ⊆ U

Tactic:
obtain ⟨Uc, Uo, Ucne⟩ := h.prop

Premises used: Maximal.prop
-- 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}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
⊢ IsOpen[inst] U

Tactic:
obtain ⟨Uc, Uo, Ucne⟩ := h.prop

Premises used: Maximal.prop
-- 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}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
⊢ Uᶜ.Nonempty

Tactic:
obtain ⟨Uc, Uo, Ucne⟩ := h.prop

Premises used: Maximal.prop
-- 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}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
⊢ ∃ V ⊆ S, V.Nonempty ∧ IsClosed[inst] V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst] V' → V' = V

Tactic:
⟨Uᶜ, Set.compl_subset_comm.mp Uc, Ucne, Uo.isClosed_compl, ?_⟩

Premises used: Compl.compl, Set.compl_subset_comm, IsOpen.isClosed_compl, And.intro, Exists.intro, Iff.mp
-- 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}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
refine : ∀ V' ⊆ Uᶜ, V'.Nonempty → IsClosed[inst] V' → V' = Uᶜ
⊢ ∃ V ⊆ S, V.Nonempty ∧ IsClosed[inst] V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed[inst] V' → V' = V

Tactic:
refine ⟨Uᶜ, Set.compl_subset_comm.mp Uc, Ucne, Uo.isClosed_compl, ?_⟩
-- 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}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst] V'
⊢ V'ᶜ = U

Tactic:
h.eq_of_ge ⟨?_, isOpen_compl_iff.mpr V'cls, ?_⟩ (subset_compl_comm.2 V'sub)

Premises used: Iff.mpr, Set.subset_compl_comm, Maximal.eq_of_ge, And.intro, isOpen_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}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst] V'
refine_1 : Sᶜ ⊆ V'ᶜ
refine_2 : V'ᶜᶜ.Nonempty
⊢ V'ᶜ = U

Tactic:
refine h.eq_of_ge ⟨?_, isOpen_compl_iff.mpr V'cls, ?_⟩ (subset_compl_comm.2 V'sub)

Premises used: Iff.mpr, Set.subset_compl_comm, Maximal.eq_of_ge, And.intro, isOpen_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}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst] V'
⊢ Sᶜ ⊆ V'ᶜ

Tactic:
Set.Subset.trans Uc (Set.subset_compl_comm.mp V'sub)

Premises used: Set.Subset.trans, Set.subset_compl_comm, Iff.mp
-- 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}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst] V'
⊢ Sᶜ ⊆ V'ᶜ

Tactic:
exact Set.Subset.trans Uc (Set.subset_compl_comm.mp V'sub)

Premises used: Set.Subset.trans, Set.subset_compl_comm, Iff.mp
-- 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}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst] V'
⊢ V'ᶜᶜ.Nonempty

Tactic:
simp only [compl_compl, V'ne]

Premises used: compl_compl
-- 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}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst] V'
⊢ V'ᶜ = U

Tactic:
have : V'ᶜ = U := by
    refine h.eq_of_ge ⟨?_, isOpen_compl_iff.mpr V'cls, ?_⟩ (subset_compl_comm.2 V'sub)
    · exact Set.Subset.trans Uc (Set.subset_compl_comm.mp V'sub)
    · simp only [compl_compl, V'ne]
-- 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}
U : Set X
h : Maximal (fun (x : Set X) ↦ x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen[inst] U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed[inst] V'
this : V'ᶜ = U
rw : V' = V'ᶜᶜ
rw₁ rw₂ : V' = V'
⊢ V' = Uᶜ

Tactic:
rw [← this, compl_compl]

Premises used: compl_compl
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
C : ℕ → Set α
hC : ∀ (i : ℕ), C i ∈ S
contrapose! : (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), dissipate C n = ∅

Tactic:
contrapose!
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
C : ℕ → Set α
hC : ∀ (i : ℕ), C i ∈ S
⊢ (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)

Tactic:
h C hC
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
h :
  ∀ (C : ℕ → Set α),
    (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
C : ℕ → Set α
hC : ∀ (i : ℕ), C i ∈ S
⊢ (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)

Tactic:
exact h C hC
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hp : IsCompactSystem S
C : ℕ → Set α
hC : ∀ (i : ℕ), C i ∈ S
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
revert : ∀ (h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty), Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)

Tactic:
revert h_nonempty
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hp : IsCompactSystem S
C : ℕ → Set α
hC : ∀ (i : ℕ), C i ∈ S
contrapose! : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), dissipate C n = ∅
⊢ ∀ (h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty), Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)

Tactic:
contrapose!
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hp : IsCompactSystem S
C : ℕ → Set α
hC : ∀ (i : ℕ), C i ∈ S
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), dissipate C n = ∅

Tactic:
hp C hC
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
hp : IsCompactSystem S
C : ℕ → Set α
hC : ∀ (i : ℕ), C i ∈ S
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), C i) ∅ → ∃ (n : ℕ), dissipate C n = ∅

Tactic:
exact hp C hC
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
⊢ IsCompactSystem S ↔
    ∀ (C : ℕ → Set α),
      (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → Set.Nonempty.{u_1} (α := α) (⋂ (i : ℕ), C i)

Tactic:
⟨nonempty_iInter, of_nonempty_iInter⟩

Premises used: Iff.intro, IsCompactSystem.nonempty_iInter, IsCompactSystem.of_nonempty_iInter
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
inst : IsEmpty α
S : Set (Set α)
⊢ IsCompactSystem S

Tactic:
fun s _ _ ↦ ⟨0, Set.eq_empty_of_isEmpty (dissipate s 0)⟩

Premises used: Set.dissipate, IsCompactSystem, Exists.intro, OfNat.ofNat, Set.eq_empty_of_isEmpty
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S T : Set (Set α)
hT : IsCompactSystem T
hST : S ⊆ T
⊢ IsCompactSystem S

Tactic:
fun C hC1 hC2 ↦ hT C (fun i ↦ hST (hC1 i)) hC2

Premises used: IsCompactSystem
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) ∅
pos : ∀ (g : ∃ (n : ℕ), s n = ∅), ∃ (n : ℕ), dissipate s n = ∅
neg : ∀ (g : ∀ (n : ℕ), (s n).Nonempty), ∃ (n : ℕ), dissipate s n = ∅
⊢ ∃ (n : ℕ), dissipate s n = ∅

Tactic:
by_cases! g : ∃ n, s n = ∅
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) ∅
g : ∃ (n : ℕ), s n = ∅
h₁ : dissipate s (g.choose (p := fun (n : ℕ) ↦ s n = ∅)) = ∅
⊢ ∃ (n : ℕ), dissipate s n = ∅

Tactic:
use g.choose

Premises used: Exists.choose
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) ∅
g : ∃ (n : ℕ), s n = ∅
h₁ :
  ∀ (hd : Subset.{u_1} (α := Set α) (⋂ (i : ℕ), s i) ∅) (g : ∃ (n : ℕ), s n = ∅),
    dissipate s (g.choose (p := fun (n : ℕ) ↦ s n = ∅)) ⊆ ∅
⊢ dissipate s (g.choose (p := fun (n : ℕ) ↦ s n = ∅)) = ∅

Tactic:
rw [← subset_empty_iff] at hd ⊢

Premises used: Set.subset_empty_iff
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : Subset.{u_1} (α := Set α) (⋂ (i : ℕ), s i) ∅
g : ∃ (n : ℕ), s n = ∅
⊢ dissipate s (g.choose (p := fun (n : ℕ) ↦ s n = ∅)) ⊆ ∅

Tactic:
(dissipate_subset le_rfl).trans g.choose_spec.le

Premises used: Exists.choose_spec, le_rfl, HasSubset.Subset.trans, Eq.le, Set.dissipate_subset
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : Subset.{u_1} (α := Set α) (⋂ (i : ℕ), s i) ∅
g : ∃ (n : ℕ), s n = ∅
⊢ dissipate s (g.choose (p := fun (n : ℕ) ↦ s n = ∅)) ⊆ ∅

Tactic:
exact (dissipate_subset le_rfl).trans g.choose_spec.le

Premises used: Exists.choose_spec, le_rfl, HasSubset.Subset.trans, Eq.le, Set.dissipate_subset
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) ∅
g : ∀ (n : ℕ), (s n).Nonempty
⊢ ∃ (n : ℕ), dissipate s n = ∅

Tactic:
h s (fun i ↦ (mem_of_mem_insert_of_ne (h' i) (g i).ne_empty)) hd

Premises used: Set.mem_of_mem_insert_of_ne, Set.Nonempty.ne_empty
-- Module: Mathlib.Topology.Compactness.CompactSystem
Goal:
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ℕ), s i) ∅
g : ∀ (n : ℕ), (s n).Nonempty
⊢ ∃ (n : ℕ), dissipate s n = ∅

Tactic:
exact h s (fun i ↦ (mem_of_mem_insert_of_ne (h' i) (g i).ne_empty)) hd

Premises used: Set.mem_of_mem_insert_of_ne, Set.Nonempty.ne_empty