-- Mathlib/Topology/Separation/Basic.lean
theorem exists_isOpen_singleton_of_isOpen_finite [T0Space X] {s : Set X} (hfin : s.Finite)
    (hne : s.Nonempty) (ho : IsOpen s) : ∃ x ∈ s, IsOpen ({x} : Set X)

Proof state:
case intro.a.inl.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
t : Finset X
hts : t ⊂ s
htne : t.Nonempty
hto : IsOpen ↑t
x : X
hxt : x ∈ ↑t
hxo : IsOpen {x}
⊢ ∃ x ∈ ↑s, IsOpen {x}

Tactic:
exact ⟨x, hts.1 hxt, hxo⟩

Result:
no goals

Proof state:
case intro.a.inr.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t
x : X
hx : ↑s = {x}
⊢ ∃ x ∈ ↑s, IsOpen {x}

Tactic:
exact ⟨x, hx.symm ▸ rfl, hx ▸ ho⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t
⊢ ∀ t ⊆ ↑s, t.Nonempty → IsOpen t → t = ↑s

Tactic:
refine fun t hts htne hto => of_not_not fun hts' => ht ?_

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t
t : Set X
hts : t ⊆ ↑s
htne : t.Nonempty
hto : IsOpen t
hts' : ¬t = ↑s
⊢ ∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t

Proof state:
case intro.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
⊢ ∃ x ∈ ↑s, IsOpen {x}

Tactic:
rcases em (∃ t, t ⊂ s ∧ t.Nonempty ∧ IsOpen (t : Set X)) with (⟨t, hts, htne, hto⟩ | ht)

Result:
case intro.a.inl.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
t : Finset X
hts : t ⊂ s
htne : t.Nonempty
hto : IsOpen ↑t
⊢ ∃ x ∈ ↑s, IsOpen {x}

case intro.a.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t
⊢ ∃ x ∈ ↑s, IsOpen {x}

Proof state:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
hne : (↑s).Nonempty
ho : IsOpen ↑s
⊢ ∃ x ∈ ↑s, IsOpen {x}

Tactic:
induction s using Finset.strongInductionOn

Result:
case intro.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s✝ : Finset X
a✝ : ∀ t ⊂ s✝, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s✝).Nonempty
ho : IsOpen ↑s✝
⊢ ∃ x ∈ ↑s✝, IsOpen {x}

Proof state:
case intro.a.inl.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
t : Finset X
hts : t ⊂ s
htne : t.Nonempty
hto : IsOpen ↑t
⊢ ∃ x ∈ ↑s, IsOpen {x}

Tactic:
rcases ihs t hts htne hto with ⟨x, hxt, hxo⟩

Result:
case intro.a.inl.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
t : Finset X
hts : t ⊂ s
htne : t.Nonempty
hto : IsOpen ↑t
x : X
hxt : x ∈ ↑t
hxo : IsOpen {x}
⊢ ∃ x ∈ ↑s, IsOpen {x}

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hfin : s.Finite
hne : s.Nonempty
ho : IsOpen s
⊢ ∃ x ∈ s, IsOpen {x}

Tactic:
lift s to Finset X using hfin

Result:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
hne : (↑s).Nonempty
ho : IsOpen ↑s
⊢ ∃ x ∈ ↑s, IsOpen {x}

Proof state:
case intro.a.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t
⊢ ∃ x ∈ ↑s, IsOpen {x}

Tactic:
rsuffices ⟨x, hx⟩ : ∃ x, s.toSet = {x}

Result:
case intro.a.inr.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t
x : X
hx : ↑s = {x}
⊢ ∃ x ∈ ↑s, IsOpen {x}

X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t
⊢ ∃ x, ↑s = {x}

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t
t : Set X
hts : t ⊆ ↑s
htne : t.Nonempty
hto : IsOpen t
hts' : ¬t = ↑s
⊢ ∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t

Tactic:
lift t to Finset X using s.finite_toSet.subset hts

Result:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t
t : Finset X
hts : ↑t ⊆ ↑s
htne : (↑t).Nonempty
hto : IsOpen ↑t
hts' : ¬↑t = ↑s
⊢ ∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t

Proof state:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t
t : Finset X
hts : ↑t ⊆ ↑s
htne : (↑t).Nonempty
hto : IsOpen ↑t
hts' : ¬↑t = ↑s
⊢ ∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t

Tactic:
exact ⟨t, ssubset_iff_subset_ne.2 ⟨hts, mt Finset.coe_inj.2 hts'⟩, htne, hto⟩

Result:
no goals

Proof state:
case intro.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s✝ : Finset X
a✝ : ∀ t ⊂ s✝, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s✝).Nonempty
ho : IsOpen ↑s✝
⊢ ∃ x ∈ ↑s✝, IsOpen {x}

Tactic:
rename_i s ihs

Result:
case intro.a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
⊢ ∃ x ∈ ↑s, IsOpen {x}

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t
⊢ ∃ x, ↑s = {x}

Tactic:
refine minimal_nonempty_open_eq_singleton ho hne ?_

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen ↑t → ∃ x ∈ ↑t, IsOpen {x}
hne : (↑s).Nonempty
ho : IsOpen ↑s
ht : ¬∃ t ⊂ s, t.Nonempty ∧ IsOpen ↑t
⊢ ∀ t ⊆ ↑s, t.Nonempty → IsOpen t → t = ↑s