-- Mathlib/Topology/Separation/Basic.lean
theorem minimal_nonempty_open_subsingleton [T0Space X] {s : Set X} (hs : IsOpen s)
    (hmin : ∀ t, t ⊆ s → t.Nonempty → IsOpen t → t = s) : s.Subsingleton

Proof state:
case intro.intro.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
this :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T0Space X] {s : Set X},
    IsOpen s →
      (∀ t ⊆ s, t.Nonempty → IsOpen t → t = s) →
        ∀ x ∈ s, ∀ y ∈ s, ¬x = y → ∀ (U : Set X), IsOpen U → Xor' (x ∈ U) (y ∈ U) → x ∈ U ∧ y ∉ U → False
h : ¬(x ∈ U ∧ y ∉ U)
⊢ False

Tactic:
exact this hs hmin y hy x hx (Ne.symm hxy) U hUo hU.symm (hU.resolve_left h)

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
⊢ False

Tactic:
rcases exists_isOpen_xor'_mem hxy with ⟨U, hUo, hU⟩

Result:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
⊢ False

Proof state:
case intro
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : y ∉ U
this : s ∩ U = s
⊢ False

Tactic:
exact hyU (this.symm.subset hy).2

Result:
no goals

Proof state:
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
h : x ∈ U ∧ y ∉ U
⊢ False

Tactic:
obtain ⟨hxU, hyU⟩ := h

Result:
case intro
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : y ∉ U
⊢ False

Proof state:
case intro
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : y ∉ U
⊢ False

Tactic:
have : s ∩ U = s := hmin (s ∩ U) inter_subset_left ⟨x, hx, hxU⟩ (hs.inter hUo)

Result:
case intro
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : y ∉ U
this : s ∩ U = s
⊢ False

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s
⊢ s.Subsingleton

Tactic:
refine fun x hx y hy => of_not_not fun hxy => ?_

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
⊢ False

Proof state:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
⊢ False

Tactic:
wlog h : x ∈ U ∧ y ∉ U

Result:
case intro.intro.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
this :
  ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T0Space X] {s : Set X},
    IsOpen s →
      (∀ t ⊆ s, t.Nonempty → IsOpen t → t = s) →
        ∀ x ∈ s, ∀ y ∈ s, ¬x = y → ∀ (U : Set X), IsOpen U → Xor' (x ∈ U) (y ∈ U) → x ∈ U ∧ y ∉ U → False
h : ¬(x ∈ U ∧ y ∉ U)
⊢ False

X✝ : Type u_1
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Set X
hs : IsOpen s
hmin : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = s
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hxy : ¬x = y
U : Set X
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
h : x ∈ U ∧ y ∉ U
⊢ False