unfold compareOfLT
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
⊢ compareOfLT x y = eq → x = y
α : Type u_1
inst : LT α
inst✝² : DecidableRel fun x x_1 => x < x_1
x y : α
inst✝¹ : StableEq α
inst✝ : Connex fun x x_1 => x < x_1
⊢ (if x < y then lt else if y < x then gt else eq) = eq → x = y