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
α : 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
rcases hx with ⟨x, rfl⟩
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
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
rcases hy with ⟨y, rfl⟩
no goals
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
exact
  ordConnectedProj_eq.2
    (mem_ordConnectedComponent_trans
      (mem_ordConnectedComponent_trans (ordConnectedProj_mem_ordConnectedComponent _ _) h)
      (mem_ordConnectedComponent_ordConnectedProj _ _))