-- Mathlib/Topology/Order/Compact.lean
theorem IsCompact.exists_isLeast [ClosedIicTopology α] {s : Set α} (hs : IsCompact s)
    (ne_s : s.Nonempty) : ∃ x, IsLeast s x

Proof state:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
H : ¬(s ∩ ⋂ x, Iic ↑x).Nonempty
⊢ False

Tactic:
rw [not_nonempty_iff_eq_empty] at H

Result:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
H : s ∩ ⋂ x, Iic ↑x = ∅
⊢ False

Proof state:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
⊢ (s ∩ ⋂ x, Iic ↑x).Nonempty

Tactic:
by_contra H

Result:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
H : ¬(s ∩ ⋂ x, Iic ↑x).Nonempty
⊢ False

Proof state:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
⊢ ∃ x, IsLeast s x

Tactic:
haveI : Nonempty s := ne_s.to_subtype

Result:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
⊢ ∃ x, IsLeast s x

Proof state:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
⊢ ∃ x, IsLeast s x

Tactic:
suffices (s ∩ ⋂ x ∈ s, Iic x).Nonempty from
  ⟨this.choose, this.choose_spec.1, mem_iInter₂.mp this.choose_spec.2⟩

Result:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
⊢ (s ∩ ⋂ x ∈ s, Iic x).Nonempty

Proof state:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
H : s ∩ ⋂ x, Iic ↑x = ∅
⊢ False

Tactic:
rcases hs.elim_directed_family_closed (fun x : s => Iic ↑x) (fun x => isClosed_Iic) H
    (Monotone.directed_ge fun _ _ h => Iic_subset_Iic.mpr h) with ⟨x, hx⟩

Result:
case intro
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
H : s ∩ ⋂ x, Iic ↑x = ∅
x : ↑s
hx : s ∩ Iic ↑x = ∅
⊢ False

Proof state:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
⊢ (s ∩ ⋂ x ∈ s, Iic x).Nonempty

Tactic:
rw [biInter_eq_iInter]

Result:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
⊢ (s ∩ ⋂ x, Iic ↑x).Nonempty

Proof state:
case intro
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
H : s ∩ ⋂ x, Iic ↑x = ∅
x : ↑s
hx : s ∩ Iic ↑x = ∅
⊢ False

Tactic:
exact not_nonempty_iff_eq_empty.mpr hx ⟨x, x.2, le_rfl⟩

Result:
no goals