DecidableEq on Ordering

Stream: lean4

[Yakov Pechersky]

What's the right way to provide the instance here? I couldn't find it in the current core

import Lean

open Ordering

instance : DecidableEq Ordering
| lt, lt => isTrue rfl
| eq, eq => isTrue rfl
| gt, gt => isTrue rfl
| x, y => isFalse (λ h => Ordering.noConfusion h) -- Sort error here

-- Lean 3 style, also doesn't work
-- instance : DecidableEq Ordering := λ a b =>
--   match a, b with
--     | lt, lt => isTrue rfl
--     | eq, eq => isTrue rfl
--     | gt, gt => isTrue rfl
--     | x, y => isFalse (λ h => Ordering.noConfusion h)

[Mario Carneiro]

here's one option

instance : DecidableEq Ordering := by
  intro x y
  cases x <;> cases y <;> first
  | exact isTrue rfl
  | exact isFalse (λ h => Ordering.noConfusion h)

[Yakov Pechersky]

Why does this work but the term mode doesn't?

[Mario Carneiro]

Using match, the final case is only elaborated once and has to work for general x, y