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

Proof state:
case intro.intro
α✝ : 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' : [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
⊢ x ∈ ⊥

Tactic:
clear ha' hb'

Result:
case intro.intro
α✝ : 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ᶜ
⊢ x ∈ ⊥

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x : α
hx₂ : x ∈ t.ordT5Nhd s
a : α
has : a ∈ s
ha : x ∈ (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent a
b : α
hbt : b ∈ t
hb : x ∈ (sᶜ ∩ (t.ordSeparatingSet s).ordConnectedSectionᶜ).ordConnectedComponent b
⊢ x ∈ ⊥

Tactic:
clear hx₂

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : x ∈ (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent a
b : α
hbt : b ∈ t
hb : x ∈ (sᶜ ∩ (t.ordSeparatingSet s).ordConnectedSectionᶜ).ordConnectedComponent b
⊢ x ∈ ⊥

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x : α
hx₁ : x ∈ s.ordT5Nhd t
hx₂ : x ∈ t.ordT5Nhd s
⊢ x ∈ ⊥

Tactic:
rcases mem_iUnion₂.1 hx₁ with ⟨a, has, ha⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x : α
hx₁ : x ∈ s.ordT5Nhd t
hx₂ : x ∈ t.ordT5Nhd s
a : α
has : a ∈ s
ha : x ∈ (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent a
⊢ x ∈ ⊥

Proof state:
case intro.intro
α✝ : 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ᶜ
⊢ x ∈ ⊥

Tactic:
rcases le_total x a with hxa | hax

Result:
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 ∈ ⊥

case intro.intro.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
⊢ x ∈ ⊥

Proof state:
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
b : α
hbt : b ∈ t
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
H :
  ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α} ⦃x : α⦄,
    ∀ a ∈ s,
      [[a, x]] ⊆ tᶜ ∧ [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ →
        ∀ b ∈ t, [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ → a ≤ b → x ∈ ⊥
hab : ¬a ≤ b
⊢ x ∈ ⊥

Tactic:
exact H b hbt hb a has ha (le_of_not_le hab)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
⊢ s.ordT5Nhd t ⊓ t.ordT5Nhd s ≤ ⊥

Tactic:
rintro x ⟨hx₁, hx₂⟩

Result:
case intro
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x : α
hx₁ : x ∈ s.ordT5Nhd t
hx₂ : x ∈ t.ordT5Nhd s
⊢ x ∈ ⊥

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

Tactic:
obtain ⟨ha, ha'⟩ := ha

Result:
case intro
α✝ : 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
hb : [[b, x]] ⊆ sᶜ ∧ [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
⊢ x ∈ ⊥

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
sol1 : y < a → False
⊢ ¬y < a ∧ ¬b < y

Tactic:
have sol2 := fun (hby : b < y) =>
    (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_right_ordSeparatingSet hbt
      (hy <| Icc_subset_uIcc ⟨hxb, hby.le⟩)

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
sol1 : y < a → False
sol2 : b < y → False
⊢ ¬y < a ∧ ¬b < y

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
sol1 : y < a → False
sol2 : b < y → False
⊢ ¬y < a ∧ ¬b < y

Tactic:
exact ⟨sol1, sol2⟩

Result:
no goals

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
h' : x ∈ s.ordSeparatingSet t
⊢ x ∈ ⊥

Tactic:
lift x to ordSeparatingSet s t using h'

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
⊢ ↑x ∈ ⊥

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 < y

Tactic:
have sol1 := fun (hya : y < a) =>
    (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_left_ordSeparatingSet has
      (hy <| Icc_subset_uIcc' ⟨hya.le, hax⟩)

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
sol1 : y < a → False
⊢ ¬y < a ∧ ¬b < y