split
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
⊢ (if x = z then eq else gt) ≠ gt
case isTrue
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
h✝ : x = z
⊢ eq ≠ gt

case isFalse
α : Type u_1
inst✝⁴ : LT α
inst✝³ : DecidableRel fun x x_1 => x < x_1
inst✝² : DecidableEq α
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y z : α
cxy : (if x < y then lt else if x = y then eq else gt) ≠ gt
cyz : (if y < z then lt else if y = z then eq else gt) ≠ gt
nxz : ¬x < z
h✝ : ¬x = z
⊢ gt ≠ gt