α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ ordT5Nhd s t ⊓ ordT5Nhd t s ≤ ⊥
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ Disjoint (ordT5Nhd s t) (ordT5Nhd t s)
rw [disjoint_iff_inf_le]
case intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
hx₁ : x ∈ ordT5Nhd s t
hx₂ : x ∈ ordT5Nhd t s
⊢ x ∈ ⊥
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ ordT5Nhd s t ⊓ ordT5Nhd t s ≤ ⊥
rintro x ⟨hx₁, hx₂⟩
case intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
hx₁ : x ∈ ordT5Nhd s t
hx₂ : x ∈ ordT5Nhd t s
a : α
has : a ∈ s
ha : x ∈ ordConnectedComponent (tᶜ ∩ ordConnectedSection (ordSeparatingSet s t)ᶜ) a
⊢ x ∈ ⊥
case intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
hx₁ : x ∈ ordT5Nhd s t
hx₂ : x ∈ ordT5Nhd t s
⊢ x ∈ ⊥
rcases mem_iUnion₂.1 hx₁ with ⟨a, has, ha⟩
case intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
hx₂ : x ∈ ordT5Nhd t s
a : α
has : a ∈ s
ha : x ∈ ordConnectedComponent (tᶜ ∩ ordConnectedSection (ordSeparatingSet s t)ᶜ) a
⊢ x ∈ ⊥
case intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
hx₁ : x ∈ ordT5Nhd s t
hx₂ : x ∈ ordT5Nhd t s
a : α
has : a ∈ s
ha : x ∈ ordConnectedComponent (tᶜ ∩ ordConnectedSection (ordSeparatingSet s t)ᶜ) a
⊢ x ∈ ⊥
clear hx₁
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
hx₂ : x ∈ ordT5Nhd t s
a : α
has : a ∈ s
ha : x ∈ ordConnectedComponent (tᶜ ∩ ordConnectedSection (ordSeparatingSet s t)ᶜ) a
b : α
hbt : b ∈ t
hb : x ∈ ordConnectedComponent (sᶜ ∩ ordConnectedSection (ordSeparatingSet t s)ᶜ) b
⊢ x ∈ ⊥
case intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
hx₂ : x ∈ ordT5Nhd t s
a : α
has : a ∈ s
ha : x ∈ ordConnectedComponent (tᶜ ∩ ordConnectedSection (ordSeparatingSet s t)ᶜ) a
⊢ x ∈ ⊥
rcases mem_iUnion₂.1 hx₂ with ⟨b, hbt, hb⟩
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : x ∈ ordConnectedComponent (tᶜ ∩ ordConnectedSection (ordSeparatingSet s t)ᶜ) a
b : α
hbt : b ∈ t
hb : x ∈ ordConnectedComponent (sᶜ ∩ ordConnectedSection (ordSeparatingSet t s)ᶜ) b
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
hx₂ : x ∈ ordT5Nhd t s
a : α
has : a ∈ s
ha : x ∈ ordConnectedComponent (tᶜ ∩ ordConnectedSection (ordSeparatingSet s t)ᶜ) a
b : α
hbt : b ∈ t
hb : x ∈ ordConnectedComponent (sᶜ ∩ ordConnectedSection (ordSeparatingSet t s)ᶜ) b
⊢ x ∈ ⊥
clear hx₂
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : x ∈ ordConnectedComponent (tᶜ ∩ ordConnectedSection (ordSeparatingSet s t)ᶜ) a
b : α
hbt : b ∈ t
hb : x ∈ ordConnectedComponent (sᶜ ∩ ordConnectedSection (ordSeparatingSet t s)ᶜ) b
⊢ x ∈ ⊥
rw [mem_ordConnectedComponent, subset_inter_iff] at ha hb
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
hab : a ≤ b
⊢ x ∈ ⊥

case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
hab : b ≤ a
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
⊢ x ∈ ⊥
cases' le_total a b with hab hab
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
hab : a ≤ b
⊢ x ∈ ⊥

case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hab : a ≤ b
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
hab : a ≤ b
⊢ x ∈ ⊥

case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
hab : b ≤ a
⊢ x ∈ ⊥
on_goal 2 => swap_var a ↔ b, s ↔ t, ha ↔ hb, has ↔ hbt
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hab : a ≤ b
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
hab : b ≤ a
⊢ x ∈ ⊥
swap_var a ↔ b, s ↔ t, ha ↔ hb, has ↔ hbt
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hab : a ≤ b
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
hab : b ≤ a
⊢ x ∈ ⊥
swap_var a ↔ b, s ↔ t, ha ↔ hb, has ↔ hbt
case intro.intro.intro.intro.intro.inr.intro
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hab : a ≤ b
⊢ x ∈ ⊥
cases' ha with ha ha'
case intro.intro.intro.intro.intro.inr.intro.intro
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro.inr.intro
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
⊢ x ∈ ⊥
cases' hb with hb hb'
case intro.intro.intro.intro.intro.inr.intro.intro
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro.inr.intro.intro
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
⊢ x ∈ ⊥
have hsub : [[a, b]] ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := by
  rw [ordSeparatingSet_comm, uIcc_comm] at hb'
  calc
    [[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
    _ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'
case intro.intro.intro.intro.intro.inr.intro.intro
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro.inr.intro.intro
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
⊢ x ∈ ⊥
clear ha' hb'
case intro.intro.intro.intro.intro.inr.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hxa : x ≤ a
⊢ x ∈ ⊥

case intro.intro.intro.intro.intro.inr.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro.inr.intro.intro
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
⊢ x ∈ ⊥
cases' le_total x a with hxa hax
case intro.intro.intro.intro.intro.inr.intro.intro.inr.inl
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hbx : b ≤ x
⊢ x ∈ ⊥

case intro.intro.intro.intro.intro.inr.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro.inr.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
⊢ x ∈ ⊥
cases' le_total b x with hbx hxb
case intro.intro.intro.intro.intro.inr.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
⊢ x ∈ ⊥
case intro.intro.intro.intro.intro.inr.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
⊢ x ∈ ⊥
have h' : x ∈ ordSeparatingSet s t := ⟨mem_iUnion₂.2 ⟨a, has, ha⟩, mem_iUnion₂.2 ⟨b, hbt, hb⟩⟩
case intro.intro.intro.intro.intro.inr.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
this : ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
⊢ x ∈ ⊥

case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
⊢ ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
case intro.intro.intro.intro.intro.inr.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
⊢ x ∈ ⊥
suffices : ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
⊢ ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
case intro.intro.intro.intro.intro.inr.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
this : ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
⊢ x ∈ ⊥

case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
⊢ ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
exact hsub (this <| ordConnectedProj_mem_ordConnectedComponent _ ⟨x, h'⟩) (mem_range_self _)
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y✝ z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
⊢ y ∈ [[a, b]]
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
⊢ ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
rintro y (hy : [[x, y]] ⊆ ordSeparatingSet s t)
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y✝ z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
⊢ ¬y < a ∧ ¬b < y
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y✝ z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
⊢ y ∈ [[a, b]]
rw [uIcc_of_le hab, mem_Icc, ← not_lt, ← not_lt]
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y✝ z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
sol1 : y < a → False
⊢ ¬y < a ∧ ¬b < y
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y✝ z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
⊢ ¬y < a ∧ ¬b < y
have sol1 := fun (hya : y < a) =>
    (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_left_ordSeparatingSet has
      (hy <| Icc_subset_uIcc' ⟨hya.le, hax⟩)
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y✝ z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
sol1 : y < a → False
sol2 : b < y → False
⊢ ¬y < a ∧ ¬b < y
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y✝ z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
sol1 : y < a → False
⊢ ¬y < a ∧ ¬b < y
have sol2 := fun (hby : b < y) =>
    (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_right_ordSeparatingSet hbt
      (hy <| Icc_subset_uIcc ⟨hxb, hby.le⟩)
no goals
case this
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y✝ z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ ordSeparatingSet s t
y : α
hy : [[x, y]] ⊆ ordSeparatingSet s t
sol1 : y < a → False
sol2 : b < y → False
⊢ ¬y < a ∧ ¬b < y
exact ⟨sol1, sol2⟩
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[x, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
⊢ [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[b, x]] ⊆ ordConnectedSection (ordSeparatingSet t s)ᶜ
⊢ [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
rw [ordSeparatingSet_comm, uIcc_comm] at hb'
no goals
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[x, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
⊢ [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
calc
  [[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
  _ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'
no goals
case intro.intro.intro.intro.intro.inr.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hxa : x ≤ a
⊢ x ∈ ⊥
exact hb (Icc_subset_uIcc' ⟨hxa, hab⟩) has
no goals
case intro.intro.intro.intro.intro.inr.intro.intro.inr.inl
α : Type u_1
inst✝ : LinearOrder α
t s : Set α
x✝ y z x b : α
hbt : b ∈ t
a : α
has : a ∈ s
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ ordConnectedSection (ordSeparatingSet s t)ᶜ
hax : a ≤ x
hbx : b ≤ x
⊢ x ∈ ⊥
exact ha (Icc_subset_uIcc ⟨hab, hbx⟩) hbt