by_cases x ≤ y, y ≤ x with
| isTrue _, isTrue _ => split <;> rfl
| isTrue _, isFalse _ => split <;> rfl
| isFalse _, isTrue _ => split <;> rfl
| isFalse _, isFalse _ =>
  cases Total.total (r:=(.≤.)) x y with
  | inl hxy => absurd hxy; assumption
  | inr hyx => absurd hyx; assumption
α : Type u_1
inst✝² : LE α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : Total fun x x_1 => x ≤ x_1
x y : α
⊢ (if x ≤ y then if y ≤ x then eq else lt else gt).swap = if y ≤ x then if x ≤ y then eq else lt else gt
no goals