-- Mathlib/Topology/Compactness/Compact.lean
theorem IsClosed.exists_minimal_nonempty_closed_subset [CompactSpace X] {S : Set X}
    (hS : IsClosed S) (hne : S.Nonempty) :
    ∃ V : Set X, V ⊆ S ∧ V.Nonempty ∧ IsClosed V ∧
      ∀ V' : Set X, V' ⊆ V → V'.Nonempty → IsClosed V' → V' = V

Proof state:
case h.refine_3.htd.mk.mk
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 => x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
U : Set X
hU : U ∈ c
U' : Set X
hU' : U' ∈ c
⊢ ∃ z,
    (fun x1 x2 => x1 ⊇ x2) ((fun i => (↑i)ᶜ) ⟨U, hU⟩) ((fun i => (↑i)ᶜ) z) ∧
      (fun x1 x2 => x1 ⊇ x2) ((fun i => (↑i)ᶜ) ⟨U', hU'⟩) ((fun i => (↑i)ᶜ) z)

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

Result:
case h.refine_3.htd.mk.mk.intro.intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 => x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // 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,
    (fun x1 x2 => x1 ⊇ x2) ((fun i => (↑i)ᶜ) ⟨U, hU⟩) ((fun i => (↑i)ᶜ) z) ∧
      (fun x1 x2 => x1 ⊇ x2) ((fun i => (↑i)ᶜ) ⟨U', hU'⟩) ((fun i => (↑i)ᶜ) z)

Proof state:
case intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x => x ∈ opens) U
⊢ ∃ V ⊆ S, V.Nonempty ∧ IsClosed V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed V' → V' = V

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

Result:
case intro.intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x => x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen U
Ucne : Uᶜ.Nonempty
⊢ ∃ V ⊆ S, V.Nonempty ∧ IsClosed V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed V' → V' = V

Proof state:
case h.refine_3.htc
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 => x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ ∀ (i : { U // U ∈ c }), IsCompact (↑i)ᶜ

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

Result:
no goals

Proof state:
case pos.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 => x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub

Tactic:
haveI : Nonempty { U // U ∈ c } := ⟨⟨U₀, hU₀⟩⟩

Result:
case pos.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 => x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub

Proof state:
case intro.intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x => x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed V'
this : V'ᶜ = U
⊢ V' = Uᶜ

Tactic:
rw [← this, compl_compl]

Result:
no goals

Proof state:
case h
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 => x1 ⊆ x2) c
hcne : ¬c.Nonempty
⊢ Sᶜᶜ.Nonempty

Tactic:
rw [compl_compl]

Result:
case h
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 => x1 ⊆ x2) c
hcne : ¬c.Nonempty
⊢ S.Nonempty

Proof state:
case refine_1
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x => x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen U
Ucne : Uᶜ.Nonempty
V' : Set X
V'sub : V' ⊆ Uᶜ
V'ne : V'.Nonempty
V'cls : IsClosed V'
⊢ Sᶜ ⊆ V'ᶜ

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

Result:
no goals

Proof state:
case h.refine_3.htn
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 => x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ ∀ (i : { U // U ∈ c }), (↑i)ᶜ.Nonempty

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

Result:
no goals

Proof state:
case h.refine_2
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 => x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ IsOpen (⋃₀ c)

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

Result:
no goals

Proof state:
case intro.intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x => x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen U
Ucne : Uᶜ.Nonempty
⊢ ∃ V ⊆ S, V.Nonempty ∧ IsClosed V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed V' → V' = V

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

Result:
case intro.intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
U : Set X
h : Maximal (fun x => x ∈ opens) U
Uc : Sᶜ ⊆ U
Uo : IsOpen U
Ucne : Uᶜ.Nonempty
⊢ ∀ V' ⊆ Uᶜ, V'.Nonempty → IsClosed V' → V' = Uᶜ

Proof state:
case h.refine_3.htd.mk.mk.intro.intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 => x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // 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,
    (fun x1 x2 => x1 ⊇ x2) ((fun i => (↑i)ᶜ) ⟨U, hU⟩) ((fun i => (↑i)ᶜ) z) ∧
      (fun x1 x2 => x1 ⊇ x2) ((fun i => (↑i)ᶜ) ⟨U', hU'⟩) ((fun i => (↑i)ᶜ) z)

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

Result:
no goals

Proof state:
case neg
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 => x1 ⊆ x2) c
hcne : ¬c.Nonempty
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub

Tactic:
use Sᶜ

Result:
case h
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 => x1 ⊆ x2) c
hcne : ¬c.Nonempty
⊢ Sᶜ ∈ opens ∧ ∀ s ∈ c, s ⊆ Sᶜ