[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
⊢ ↑toDual x ∈ ordConnectedComponent (↑ofDual ⁻¹' s) (↑toDual x✝) ↔ ↑toDual x ∈ ↑ofDual ⁻¹' ordConnectedComponent s x✝
[PROOFSTEP]
rw [mem_ordConnectedComponent, dual_uIcc]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x : α
⊢ ↑ofDual ⁻¹' [[x✝, x]] ⊆ ↑ofDual ⁻¹' s ↔ ↑toDual x ∈ ↑ofDual ⁻¹' ordConnectedComponent s x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ x ∈ ordConnectedComponent s x ↔ x ∈ s
[PROOFSTEP]
rw [mem_ordConnectedComponent, uIcc_self, singleton_subset_iff]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ ordConnectedComponent s x = ∅ ↔ ¬x ∈ s
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, nonempty_ordConnectedComponent]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ ordConnectedComponent univ x = univ
[PROOFSTEP]
simp [ordConnectedComponent]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s✝ t✝ : Set α
x✝ y z : α
s t : Set α
x : α
⊢ ordConnectedComponent (s ∩ t) x = ordConnectedComponent s x ∩ ordConnectedComponent t x
[PROOFSTEP]
simp [ordConnectedComponent, setOf_and]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ y ∈ ordConnectedComponent s x ↔ x ∈ ordConnectedComponent s y
[PROOFSTEP]
rw [mem_ordConnectedComponent, mem_ordConnectedComponent, uIcc_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z : α
x y : ↑s
⊢ ordConnectedProj s x = ordConnectedProj s y ↔ [[↑x, ↑y]] ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z : α
x y : ↑s
⊢ ordConnectedProj s x = ordConnectedProj s y → [[↑x, ↑y]] ⊆ s
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z : α
x y : ↑s
⊢ [[↑x, ↑y]] ⊆ s → ordConnectedProj s x = ordConnectedProj s y
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z : α
x y : ↑s
h : ordConnectedProj s x = ordConnectedProj s y
⊢ [[↑x, ↑y]] ⊆ s
[PROOFSTEP]
rw [← mem_ordConnectedComponent, ← ordConnectedComponent_ordConnectedProj, h, ordConnectedComponent_ordConnectedProj,
  self_mem_ordConnectedComponent]
[GOAL]
case mp
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z : α
x y : ↑s
h : ordConnectedProj s x = ordConnectedProj s y
⊢ ↑y ∈ s
[PROOFSTEP]
exact y.2
[GOAL]
case mpr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z : α
x y : ↑s
h : [[↑x, ↑y]] ⊆ s
⊢ ordConnectedProj s x = ordConnectedProj s y
[PROOFSTEP]
simp only [ordConnectedProj, ordConnectedComponent_eq h]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s✝ t : Set α
x y z : α
s : Set α
⊢ ordConnectedSection (↑ofDual ⁻¹' s) = ↑ofDual ⁻¹' ordConnectedSection s
[PROOFSTEP]
simp_rw [ordConnectedSection, ordConnectedProj]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s✝ t : Set α
x y z : α
s : Set α
⊢ (range fun x => Nonempty.some (_ : Set.Nonempty (ordConnectedComponent (↑ofDual ⁻¹' s) ↑x))) =
    ↑ofDual ⁻¹' range fun x => Nonempty.some (_ : Set.Nonempty (ordConnectedComponent s ↑x))
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝ : LinearOrder α
s✝ t : Set α
x✝ y z : α
s : Set α
x : αᵒᵈ
⊢ (x ∈ range fun x => Nonempty.some (_ : Set.Nonempty (ordConnectedComponent (↑ofDual ⁻¹' s) ↑x))) ↔
    x ∈ ↑ofDual ⁻¹' range fun x => Nonempty.some (_ : Set.Nonempty (ordConnectedComponent s ↑x))
[PROOFSTEP]
simp [dual_ordConnectedComponent]
[GOAL]
case h
α : Type u_1
inst✝ : LinearOrder α
s✝ t : Set α
x✝ y z : α
s : Set α
x : αᵒᵈ
⊢ (∃ a h, Nonempty.some (_ : Set.Nonempty (↑ofDual ⁻¹' ordConnectedComponent s a)) = x) ↔
    ∃ a h, Nonempty.some (_ : Set.Nonempty (ordConnectedComponent s ↑{ val := a, property := (_ : a ∈ s) })) = ↑ofDual x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
hx : x ∈ ordConnectedSection s
hy : y ∈ ordConnectedSection s
h : [[x, y]] ⊆ s
⊢ x = y
[PROOFSTEP]
rcases hx with ⟨x, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
y z : α
hy : y ∈ ordConnectedSection s
x : ↑s
h : [[ordConnectedProj s x, y]] ⊆ s
⊢ ordConnectedProj s x = y
[PROOFSTEP]
rcases hy with ⟨y, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
z : α
x y : ↑s
h : [[ordConnectedProj s x, ordConnectedProj s y]] ⊆ s
⊢ ordConnectedProj s x = ordConnectedProj s y
[PROOFSTEP]
exact
  ordConnectedProj_eq.2
    (mem_ordConnectedComponent_trans
      (mem_ordConnectedComponent_trans (ordConnectedProj_mem_ordConnectedComponent _ _) h)
      (mem_ordConnectedComponent_ordConnectedProj _ _))
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ ordSeparatingSet (↑ofDual ⁻¹' s) (↑ofDual ⁻¹' t) = ↑ofDual ⁻¹' ordSeparatingSet s t
[PROOFSTEP]
simp only [ordSeparatingSet, mem_preimage, ← toDual.surjective.iUnion_comp, ofDual_toDual, dual_ordConnectedComponent, ←
  preimage_compl, preimage_inter, preimage_iUnion]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ Disjoint (ordT5Nhd s t) (ordT5Nhd t s)
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x y z : α
⊢ ordT5Nhd s t ⊓ ordT5Nhd t s ≤ ⊥
[PROOFSTEP]
rintro x ⟨hx₁, hx₂⟩
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
rcases mem_iUnion₂.1 hx₁ with ⟨a, has, ha⟩
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
clear hx₁
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
rcases mem_iUnion₂.1 hx₂ with ⟨b, hbt, hb⟩
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
clear hx₂
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
rw [mem_ordConnectedComponent, subset_inter_iff] at ha hb 
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
cases' le_total a b with hab hab
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
on_goal 2 => swap_var a ↔ b, s ↔ t, ha ↔ hb, has ↔ hbt
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
on_goal 2 => swap_var a ↔ b, s ↔ t, ha ↔ hb, has ↔ hbt
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
swap_var a ↔ b, s ↔ t, ha ↔ hb, has ↔ hbt
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
all_goals
  -- porting note: wlog not implemented yet, the following replaces the three previous lines
  -- wlog (discharger := tactic.skip) hab : a ≤ b := le_total a b using a b s t, b a t s
  cases' ha with ha ha'
  cases' hb with hb hb'
  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'
  clear ha' hb'
  cases' le_total x a with hxa hax
  · exact hb (Icc_subset_uIcc' ⟨hxa, hab⟩) has
  cases' le_total b x with hbx hxb
  · exact ha (Icc_subset_uIcc ⟨hab, hbx⟩) hbt
  have h' : x ∈ ordSeparatingSet s t :=
    ⟨mem_iUnion₂.2 ⟨a, has, ha⟩, mem_iUnion₂.2 ⟨b, hbt, hb⟩⟩
      -- porting note: lift not implemented yet
          -- lift x to ordSeparatingSet s t using this
  suffices : ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
  exact hsub (this <| ordConnectedProj_mem_ordConnectedComponent _ ⟨x, h'⟩) (mem_range_self _)
  rintro y (hy : [[x, y]] ⊆ ordSeparatingSet s t)
  rw [uIcc_of_le hab, mem_Icc, ← not_lt, ← not_lt]
  have sol1 := fun (hya : y < a) =>
    (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_left_ordSeparatingSet has
      (hy <| Icc_subset_uIcc' ⟨hya.le, hax⟩)
  have sol2 := fun (hby : b < y) =>
    (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_right_ordSeparatingSet hbt
      (hy <| Icc_subset_uIcc ⟨hxb, hby.le⟩)
  exact ⟨sol1, sol2⟩
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
cases' ha with ha ha'
[GOAL]
case intro.intro.intro.intro.intro.inl.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (ordConnectedSection (ordSeparatingSet t s))ᶜ
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
⊢ x ∈ ⊥
[PROOFSTEP]
cases' hb with hb hb'
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
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 ∈ ⊥
[PROOFSTEP]
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'
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
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))ᶜ
[PROOFSTEP]
rw [ordSeparatingSet_comm, uIcc_comm] at hb' 
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
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))ᶜ
[PROOFSTEP]
calc
  [[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
  _ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
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 ∈ ⊥
[PROOFSTEP]
clear ha' hb'
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
⊢ x ∈ ⊥
[PROOFSTEP]
cases' le_total x a with hxa hax
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hxa : x ≤ a
⊢ x ∈ ⊥
[PROOFSTEP]
exact hb (Icc_subset_uIcc' ⟨hxa, hab⟩) has
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (ordConnectedSection (ordSeparatingSet s t))ᶜ
hax : a ≤ x
⊢ x ∈ ⊥
[PROOFSTEP]
cases' le_total b x with hbx hxb
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro.inr.inl
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
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 ∈ ⊥
[PROOFSTEP]
exact ha (Icc_subset_uIcc ⟨hab, hbx⟩) hbt
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
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 ∈ ⊥
[PROOFSTEP]
have h' : x ∈ ordSeparatingSet s t :=
  ⟨mem_iUnion₂.2 ⟨a, has, ha⟩, mem_iUnion₂.2 ⟨b, hbt, hb⟩⟩
    -- porting note: lift not implemented yet
        -- lift x to ordSeparatingSet s t using this
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
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 ∈ ⊥
[PROOFSTEP]
suffices : ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
[GOAL]
case intro.intro.intro.intro.intro.inl.intro.intro.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
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 α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
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]]
[PROOFSTEP]
exact hsub (this <| ordConnectedProj_mem_ordConnectedComponent _ ⟨x, h'⟩) (mem_range_self _)
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
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]]
[PROOFSTEP]
rintro y (hy : [[x, y]] ⊆ ordSeparatingSet s t)
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
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]]
[PROOFSTEP]
rw [uIcc_of_le hab, mem_Icc, ← not_lt, ← not_lt]
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
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
[PROOFSTEP]
have sol1 := fun (hya : y < a) =>
  (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_left_ordSeparatingSet has
    (hy <| Icc_subset_uIcc' ⟨hya.le, hax⟩)
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
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
[PROOFSTEP]
have sol2 := fun (hby : b < y) =>
  (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_right_ordSeparatingSet hbt
    (hy <| Icc_subset_uIcc ⟨hxb, hby.le⟩)
[GOAL]
case this
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z x a : α
has : a ∈ s
b : α
hbt : b ∈ t
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
[PROOFSTEP]
exact ⟨sol1, sol2⟩
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
cases' ha with ha ha'
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
cases' hb with hb hb'
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
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'
[GOAL]
α : 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))ᶜ
[PROOFSTEP]
rw [ordSeparatingSet_comm, uIcc_comm] at hb' 
[GOAL]
α : 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))ᶜ
[PROOFSTEP]
calc
  [[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
  _ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
clear ha' hb'
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
cases' le_total x a with hxa hax
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
exact hb (Icc_subset_uIcc' ⟨hxa, hab⟩) has
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
cases' le_total b x with hbx hxb
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
exact ha (Icc_subset_uIcc ⟨hab, hbx⟩) hbt
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
have h' : x ∈ ordSeparatingSet s t :=
  ⟨mem_iUnion₂.2 ⟨a, has, ha⟩, mem_iUnion₂.2 ⟨b, hbt, hb⟩⟩
    -- porting note: lift not implemented yet
        -- lift x to ordSeparatingSet s t using this
[GOAL]
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 ∈ ⊥
[PROOFSTEP]
suffices : ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]]
[GOAL]
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]]
[PROOFSTEP]
exact hsub (this <| ordConnectedProj_mem_ordConnectedComponent _ ⟨x, h'⟩) (mem_range_self _)
[GOAL]
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]]
[PROOFSTEP]
rintro y (hy : [[x, y]] ⊆ ordSeparatingSet s t)
[GOAL]
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]]
[PROOFSTEP]
rw [uIcc_of_le hab, mem_Icc, ← not_lt, ← not_lt]
[GOAL]
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
[PROOFSTEP]
have sol1 := fun (hya : y < a) =>
  (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_left_ordSeparatingSet has
    (hy <| Icc_subset_uIcc' ⟨hya.le, hax⟩)
[GOAL]
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
[PROOFSTEP]
have sol2 := fun (hby : b < y) =>
  (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_right_ordSeparatingSet hbt
    (hy <| Icc_subset_uIcc ⟨hxb, hby.le⟩)
[GOAL]
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
[PROOFSTEP]
exact ⟨sol1, sol2⟩
