-- Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
theorem disjoint_ordT5Nhd : Disjoint (ordT5Nhd s t) (ordT5Nhd t s)

Proof state:
case intro.intro.inr.inr.intro
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x // x ∈ s.ordSeparatingSet t }
ha : [[a, ↑x]] ⊆ tᶜ
hb : [[b, ↑x]] ⊆ sᶜ
hax : a ≤ ↑x
hxb : ↑x ≤ b
⊢ ↑x ∈ ⊥

Tactic:
suffices ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]] from
  hsub (this <| ordConnectedProj_mem_ordConnectedComponent _ x) (mem_range_self _)

Result:
case intro.intro.inr.inr.intro
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x // x ∈ s.ordSeparatingSet t }
ha : [[a, ↑x]] ⊆ tᶜ
hb : [[b, ↑x]] ⊆ sᶜ
hax : a ≤ ↑x
hxb : ↑x ≤ b
⊢ (s.ordSeparatingSet t).ordConnectedComponent ↑x ⊆ [[a, b]]

Proof state:
case intro.intro.inl
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hxa : x ≤ a
⊢ x ∈ ⊥

Tactic:
exact hb (Icc_subset_uIcc' ⟨hxa, hab⟩) has

Result:
no goals

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

Tactic:
exact ha (Icc_subset_uIcc ⟨hab, hbx⟩) hbt

Result:
no goals

Proof state:
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[x, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
⊢ [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ

Tactic:
calc
  [[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
  _ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'

Result:
no goals

Proof state:
case intro.intro.inr.inr.intro
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x // x ∈ s.ordSeparatingSet t }
ha : [[a, ↑x]] ⊆ tᶜ
hb : [[b, ↑x]] ⊆ sᶜ
hax : a ≤ ↑x
hxb : ↑x ≤ b
y : α
hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent ↑x
⊢ y ∈ [[a, b]]

Tactic:
rw [uIcc_of_le hab, mem_Icc, ← not_lt, ← not_lt]

Result:
case intro.intro.inr.inr.intro
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x // x ∈ s.ordSeparatingSet t }
ha : [[a, ↑x]] ⊆ tᶜ
hb : [[b, ↑x]] ⊆ sᶜ
hax : a ≤ ↑x
hxb : ↑x ≤ b
y : α
hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent ↑x
⊢ ¬y < a ∧ ¬b < y

Proof state:
case intro.intro.inr.inr
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hax : a ≤ x
hxb : x ≤ b
⊢ x ∈ ⊥

Tactic:
have h' : x ∈ ordSeparatingSet s t := ⟨mem_iUnion₂.2 ⟨a, has, ha⟩, mem_iUnion₂.2 ⟨b, hbt, hb⟩⟩

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