α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
⊢ Set.Subsingleton s
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
⊢ Set.Subsingleton s
clear β
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : ¬x = y
⊢ False
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
⊢ Set.Subsingleton s
refine' fun x hx y hy => of_not_not fun hxy => _
case intro.intro
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : ¬x = y
U : Set α
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
⊢ False
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : ¬x = y
⊢ False
rcases exists_isOpen_xor'_mem hxy with ⟨U, hUo, hU⟩
case intro.intro.inr
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : ¬x = y
U : Set α
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
this :
  ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : T0Space α] {s : Set α},
    IsOpen s →
      (∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s) →
        ∀ (x : α),
          x ∈ s → ∀ (y : α), y ∈ s → ¬x = y → ∀ (U : Set α), IsOpen U → Xor' (x ∈ U) (y ∈ U) → x ∈ U ∧ ¬y ∈ U → False
h : ¬(x ∈ U ∧ ¬y ∈ U)
⊢ False

α✝ : Type u
inst✝² : TopologicalSpace α✝
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : ¬x = y
U : Set α
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
h : x ∈ U ∧ ¬y ∈ U
⊢ False
case intro.intro
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : ¬x = y
U : Set α
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
⊢ False
wlog h : x ∈ U ∧ y ∉ U
case intro
α✝ : Type u
inst✝² : TopologicalSpace α✝
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : ¬x = y
U : Set α
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : ¬y ∈ U
⊢ False
α✝ : Type u
inst✝² : TopologicalSpace α✝
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : ¬x = y
U : Set α
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
h : x ∈ U ∧ ¬y ∈ U
⊢ False
cases' h with hxU hyU
case intro
α✝ : Type u
inst✝² : TopologicalSpace α✝
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : ¬x = y
U : Set α
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : ¬y ∈ U
this : s ∩ U = s
⊢ False
case intro
α✝ : Type u
inst✝² : TopologicalSpace α✝
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : ¬x = y
U : Set α
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : ¬y ∈ U
⊢ False
have : s ∩ U = s := hmin (s ∩ U) (inter_subset_left _ _) ⟨x, hx, hxU⟩ (hs.inter hUo)
no goals
case intro
α✝ : Type u
inst✝² : TopologicalSpace α✝
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : ¬x = y
U : Set α
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
hxU : x ∈ U
hyU : ¬y ∈ U
this : s ∩ U = s
⊢ False
exact hyU (this.symm.subset hy).2
no goals
case intro.intro.inr
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : T0Space α
s : Set α
hs : IsOpen s
hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : ¬x = y
U : Set α
hUo : IsOpen U
hU : Xor' (x ∈ U) (y ∈ U)
this :
  ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : T0Space α] {s : Set α},
    IsOpen s →
      (∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s) →
        ∀ (x : α),
          x ∈ s → ∀ (y : α), y ∈ s → ¬x = y → ∀ (U : Set α), IsOpen U → Xor' (x ∈ U) (y ∈ U) → x ∈ U ∧ ¬y ∈ U → False
h : ¬(x ∈ U ∧ ¬y ∈ U)
⊢ False
exact this hs hmin y hy x hx (Ne.symm hxy) U hUo hU.symm (hU.resolve_left h)