diff --git a/Std/Classes/Order.lean b/Std/Classes/Order.lean
index 1fa92576f9..c5f70db253 100644
--- a/Std/Classes/Order.lean
+++ b/Std/Classes/Order.lean
@@ -90,6 +90,12 @@ theorem cmp_congr_right [TransCmp cmp] (yz : cmp y z = .eq) : cmp x y = cmp x z
 
 end TransCmp
 
+end Std
+
+namespace Ordering
+
+open Std
+
 /-- Pull back a comparator by a function `f`, by applying the comparator to both arguments. -/
 @[inline] def byKey (f : α → β) (cmp : β → β → Ordering) (a b : α) : Ordering := cmp (f a) (f b)
 
@@ -102,6 +108,8 @@ instance (f : α → β) (cmp : β → β → Ordering) [TransCmp cmp] : TransCm
 instance (f : α → β) (cmp : β → β → Ordering) [TransCmp cmp] : TransCmp (byKey f cmp) where
   le_trans h₁ h₂ := TransCmp.le_trans (α := β) h₁ h₂
 
+end Ordering
+
 @[simp] theorem ge_iff_le [LE α] {x y : α} : x ≥ y ↔ y ≤ x := Iff.rfl
 
 @[simp] theorem gt_iff_lt [LT α] {x y : α} : x > y ↔ y < x := Iff.rfl
diff --git a/Std/Data/RBMap/Alter.lean b/Std/Data/RBMap/Alter.lean
index 09f033801b..2a13a8c5d8 100644
--- a/Std/Data/RBMap/Alter.lean
+++ b/Std/Data/RBMap/Alter.lean
@@ -431,7 +431,7 @@ so it uses the element linearly if `t` is unshared.
 -/
 def modify (t : RBMap α β cmp) (k : α) (f : β → β) : RBMap α β cmp :=
   @RBSet.modifyP _ _ t (cmp k ·.1) (fun (a, b) => (a, f b))
-    (.of_eq fun _ => ⟨OrientedCmp.cmp_refl (cmp := byKey Prod.fst cmp)⟩)
+    (.of_eq fun _ => ⟨OrientedCmp.cmp_refl (cmp := Ordering.byKey Prod.fst cmp)⟩)
 
 /-- Auxiliary definition for `alter`. -/
 def alter.adapt (k : α) (f : Option β → Option β) : Option (α × β) → Option (α × β)
@@ -461,6 +461,6 @@ the ordering properties of the element, which would break the invariants.
   cases t' <;> simp [alter.adapt, RBNode.root?] <;> split <;> intro h <;> cases h
   · exact ⟨(t.2.out.1.zoom eq).2.2.2.toRootOrdered, ⟨⟩⟩
   · refine ⟨(?a).RootOrdered_congr.2 (t.2.out.1.zoom eq).2.2.1.1, ?a⟩
-    exact ⟨OrientedCmp.cmp_refl (cmp := byKey Prod.fst cmp)⟩
+    exact ⟨OrientedCmp.cmp_refl (cmp := Ordering.byKey Prod.fst cmp)⟩
 
 end RBMap
diff --git a/Std/Data/RBMap/Basic.lean b/Std/Data/RBMap/Basic.lean
index 748bdbfc2b..31c23df6c7 100644
--- a/Std/Data/RBMap/Basic.lean
+++ b/Std/Data/RBMap/Basic.lean
@@ -849,7 +849,7 @@ The `cmp` function is the comparator that will be used for performing searches;
 it should satisfy the requirements of `TransCmp` for it to have sensible behavior.
 -/
 def RBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Type (max u v) :=
-  RBSet (α × β) (byKey Prod.fst cmp)
+  RBSet (α × β) (Ordering.byKey Prod.fst cmp)
 
 /-- `O(1)`. Construct a new empty map. -/
 @[inline] def mkRBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : RBMap α β cmp :=
diff --git a/Std/Data/RBMap/WF.lean b/Std/Data/RBMap/WF.lean
index f42acce326..46ed5eda88 100644
--- a/Std/Data/RBMap/WF.lean
+++ b/Std/Data/RBMap/WF.lean
@@ -525,6 +525,8 @@ We extract this as a function so that `IsMonotone (mapSnd f)` can be an instance
 -/
 @[inline] def mapSnd (f : α → β → γ) := fun (a, b) => (a, f a b)
 
+open Ordering (byKey)
+
 instance (cmp : α → α → Ordering) (f : α → β → γ) :
     IsMonotone (byKey Prod.fst cmp) (byKey Prod.fst cmp) (mapSnd f) where
   lt_mono | ⟨h⟩ => ⟨@fun _ => @h {