next =>
  split
  next heq =>
    split
    next hlt =>
      absurd hlt
      rw [heq]
      exact Irreflexive.irrfl
    next =>
      split
      next => rfl
      next hne =>
        absurd hne
        symmetry
        assumption
  next hne =>
    split
    next => rfl
    next =>
      split
      next =>
        absurd hne
        symmetry
        assumption
      next =>
        cases Connex.connex (r:=(.<.)) hne with
        | inl _ => contradiction
        | inr _ => contradiction
case isFalse
α : Type u_1
inst✝⁵ : LT α
inst✝⁴ : DecidableRel fun x x_1 => x < x_1
inst✝³ : DecidableEq α
inst✝² : Irreflexive fun x x_1 => x < x_1
inst✝¹ : Transitive fun x x_1 => x < x_1
inst✝ : Connex fun x x_1 => x < x_1
x y : α
h✝ : ¬x < y
⊢ (if x = y then eq else gt).swap = if y < x then lt else if y = x then eq else gt
no goals