fix: remove accidental instance for lexOrd (#9739)

This PR removes the `instance` attribute from `lexOrd` that was
accidentally applied in `Std.Classes.Ord.Basic`.

src/Std/Classes/Ord/Basic.lean

@@ -610,22 +610,20 @@ instance {α β} {f : α → β} [Ord β] [TransOrd β] :
     TransCmp (compareOn f) where
   isLE_trans := TransOrd.isLE_trans (α := β)
 
-attribute [instance] lexOrd in
+attribute [local instance] lexOrd
+
 instance {α β} [Ord α] [Ord β] [ReflOrd α] [ReflOrd β] :
     ReflOrd (α × β) :=
   inferInstanceAs <| ReflCmp (compareLex _ _)
 
-attribute [instance] lexOrd in
 instance {α β} [Ord α] [Ord β] [OrientedOrd α] [OrientedOrd β] :
     OrientedOrd (α × β) :=
   inferInstanceAs <| OrientedCmp (compareLex _ _)
 
-attribute [instance] lexOrd in
 instance {α β} [Ord α] [Ord β] [TransOrd α] [TransOrd β] :
     TransOrd (α × β) :=
   inferInstanceAs <| TransCmp (compareLex _ _)
 
-attribute [instance] lexOrd in
 instance {α β} [Ord α] [Ord β] [LawfulEqOrd α] [LawfulEqOrd β] : LawfulEqOrd (α × β) where
   eq_of_compare {a b} h := by
     simp only [lexOrd, compareLex_eq_eq, compareOn] at h

src/Std/Time/Date/ValidDate.lean

@@ -29,6 +29,8 @@ is valid only if `leap` is `true`.
 instance : Inhabited (ValidDate l) where
   default := ⟨⟨1, 1⟩, (by cases l <;> decide)⟩
 
+attribute [local instance] lexOrd
+
 instance : DecidableEq (ValidDate leap) := Subtype.instDecidableEq
 
 instance : Ord (ValidDate leap) where