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

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
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x✝ y✝ z : α
x y : ↑s
⊢ ordConnectedProj s x = ordConnectedProj s y ↔ [[↑x, ↑y]] ⊆ s
constructor <;> intro h
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
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
rw [← mem_ordConnectedComponent, ← ordConnectedComponent_ordConnectedProj, h,
  ordConnectedComponent_ordConnectedProj, self_mem_ordConnectedComponent]
no goals
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
exact y.2
no goals
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
simp only [ordConnectedProj, ordConnectedComponent_eq h]