fix: remove explicit Ord Range

src/Init/Data/Ord.lean

@@ -12,14 +12,6 @@ inductive Ordering where
   | lt | eq | gt
 deriving Inhabited, BEq
 
-namespace Ordering
-
-def lexOrdering (orderings : List Ordering) : Ordering :=
-  orderings.foldr (init := Ordering.eq) fun ordering result =>
-    if ordering == Ordering.eq then result else ordering
-
-end Ordering
-
 
 class Ord (α : Type u) where
   compare : α → α → Ordering

src/Lean/Data/Lsp/Basic.lean

@@ -42,10 +42,7 @@ instance : LE Position := leOfOrd
 structure Range where
   start : Position
   «end» : Position
-  deriving Inhabited, BEq, Hashable, ToJson, FromJson
-
-instance : Ord Range where
-  compare a b := Ordering.lexOrdering [compare a.start b.start, compare a.end b.end]
+  deriving Inhabited, BEq, Hashable, ToJson, FromJson, Ord
 
 instance : LT Range := ltOfOrd
 instance : LE Range := leOfOrd