[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h : x ≠ y
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ ¬y ∈ U
[PROOFSTEP]
obtain h | h := h.not_le_or_not_le
[GOAL]
case inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬x ≤ y
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ ¬y ∈ U
[PROOFSTEP]
exact (exists_clopen_upper_of_not_le h).imp fun _ ↦ And.imp_right <| And.imp_left Or.inl
[GOAL]
case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬y ≤ x
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ ¬y ∈ U
[PROOFSTEP]
obtain ⟨U, hU, hU', hy, hx⟩ := exists_clopen_lower_of_not_le h
[GOAL]
case inr.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬y ≤ x
U : Set α
hU : IsClopen U
hU' : IsLowerSet U
hy : ¬y ∈ U
hx : x ∈ U
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ ¬y ∈ U
[PROOFSTEP]
exact ⟨U, hU, Or.inr hU', hx, hy⟩
