diff --git a/src/Std/Classes/Ord/Basic.lean b/src/Std/Classes/Ord/Basic.lean
index 041b87b932..7f7f99d5d0 100644
--- a/src/Std/Classes/Ord/Basic.lean
+++ b/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
diff --git a/src/Std/Time/Date/ValidDate.lean b/src/Std/Time/Date/ValidDate.lean
index e47acc2dbd..e4338e0415 100644
--- a/src/Std/Time/Date/ValidDate.lean
+++ b/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