case intro.intro.intro.intro
α✝ : Type u
β : Type v
inst✝³ : TopologicalSpace α✝
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T0Space α
inst✝ : CompactSpace α
S : Set α
hS : IsClosed S
hne : Set.Nonempty S
V : Set α
Vsub : V ⊆ S
Vne : Set.Nonempty V
Vcls : IsClosed V
hV : ∀ (V' : Set α), V' ⊆ V → Set.Nonempty V' → IsClosed V' → V' = V
⊢ ∃ x, x ∈ S ∧ IsClosed {x}
α✝ : Type u
β : Type v
inst✝³ : TopologicalSpace α✝
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T0Space α
inst✝ : CompactSpace α
S : Set α
hS : IsClosed S
hne : Set.Nonempty S
⊢ ∃ x, x ∈ S ∧ IsClosed {x}
obtain ⟨V, Vsub, Vne, Vcls, hV⟩ := hS.exists_minimal_nonempty_closed_subset hne
case intro.intro.intro.intro.intro
α✝ : Type u
β : Type v
inst✝³ : TopologicalSpace α✝
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T0Space α
inst✝ : CompactSpace α
S : Set α
hS : IsClosed S
hne : Set.Nonempty S
x : α
Vsub : {x} ⊆ S
Vne : Set.Nonempty {x}
Vcls : IsClosed {x}
hV : ∀ (V' : Set α), V' ⊆ {x} → Set.Nonempty V' → IsClosed V' → V' = {x}
⊢ ∃ x, x ∈ S ∧ IsClosed {x}
case intro.intro.intro.intro
α✝ : Type u
β : Type v
inst✝³ : TopologicalSpace α✝
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T0Space α
inst✝ : CompactSpace α
S : Set α
hS : IsClosed S
hne : Set.Nonempty S
V : Set α
Vsub : V ⊆ S
Vne : Set.Nonempty V
Vcls : IsClosed V
hV : ∀ (V' : Set α), V' ⊆ V → Set.Nonempty V' → IsClosed V' → V' = V
⊢ ∃ x, x ∈ S ∧ IsClosed {x}
rcases minimal_nonempty_closed_eq_singleton Vcls Vne hV with ⟨x, rfl⟩
no goals
case intro.intro.intro.intro.intro
α✝ : Type u
β : Type v
inst✝³ : TopologicalSpace α✝
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : T0Space α
inst✝ : CompactSpace α
S : Set α
hS : IsClosed S
hne : Set.Nonempty S
x : α
Vsub : {x} ⊆ S
Vne : Set.Nonempty {x}
Vcls : IsClosed {x}
hV : ∀ (V' : Set α), V' ⊆ {x} → Set.Nonempty V' → IsClosed V' → V' = {x}
⊢ ∃ x, x ∈ S ∧ IsClosed {x}
exact ⟨x, Vsub (mem_singleton x), Vcls⟩