diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean
index dbb2661962..b8323d0225 100644
--- a/src/Init/Data/Ord.lean
+++ b/src/Init/Data/Ord.lean
@@ -303,7 +303,7 @@ In particular, if `x < y` then the result is `Ordering.lt`. If `x = y` then the
 
 `compareOfLessAndBEq` uses `BEq` instead of `DecidableEq`.
 -/
-@[inline] def compareOfLessAndEq {α} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering :=
+@[inline, expose] def compareOfLessAndEq {α} (x y : α) [LT α] [Decidable (x < y)] [DecidableEq α] : Ordering :=
   if x < y then Ordering.lt
   else if x = y then Ordering.eq
   else Ordering.gt
@@ -329,7 +329,7 @@ by `cmp₂` to break the tie.
 
 To lexicographically combine two `Ordering`s, use `Ordering.then`.
 -/
-@[inline] def compareLex (cmp₁ cmp₂ : α → β → Ordering) (a : α) (b : β) : Ordering :=
+@[inline, expose] def compareLex (cmp₁ cmp₂ : α → β → Ordering) (a : α) (b : β) : Ordering :=
   (cmp₁ a b).then (cmp₂ a b)
 
 section Lemmas
@@ -457,7 +457,7 @@ Examples:
  * `compareOn (· % 3) 5 6 = .gt`
  * `compareOn (·.foldl max 0) [1, 2, 3] [3, 2, 1] = .eq`
 -/
-@[inline] def compareOn [ord : Ord β] (f : α → β) (x y : α) : Ordering :=
+@[inline, expose] def compareOn [ord : Ord β] (f : α → β) (x y : α) : Ordering :=
   compare (f x) (f y)
 
 instance : Ord Nat where
@@ -724,7 +724,7 @@ protected theorem compare_eq_compare_toList {α n} [Ord α] {a b : Vector α n}
 end Vector
 
 /-- The lexicographic order on pairs. -/
-def lexOrd [Ord α] [Ord β] : Ord (α × β) where
+@[expose] def lexOrd [Ord α] [Ord β] : Ord (α × β) where
   compare := compareLex (compareOn (·.1)) (compareOn (·.2))
 
 /--
@@ -781,7 +781,7 @@ Inverts the order of an `Ord` instance.
 The result is an `Ord α` instance that returns `Ordering.lt` when `ord` would return `Ordering.gt`
 and that returns `Ordering.gt` when `ord` would return `Ordering.lt`.
 -/
-protected def opposite (ord : Ord α) : Ord α where
+@[expose] protected def opposite (ord : Ord α) : Ord α where
   compare x y := ord.compare y x
 
 /--
@@ -792,13 +792,13 @@ In particular, `ord.on f` compares `x` and `y` by comparing `f x` and `f y` acco
 The function `compareOn` can be used to perform this comparison without constructing an intermediate
 `Ord` instance.
 -/
-protected def on (_ : Ord β) (f : α → β) : Ord α where
+@[expose] protected def on (_ : Ord β) (f : α → β) : Ord α where
   compare := compareOn f
 
 /--
 Constructs the lexicographic order on products `α × β` from orders for `α` and `β`.
 -/
-protected abbrev lex (_ : Ord α) (_ : Ord β) : Ord (α × β) :=
+@[expose] protected abbrev lex (_ : Ord α) (_ : Ord β) : Ord (α × β) :=
   lexOrd
 
 /--
@@ -811,7 +811,7 @@ The function `compareLex` can be used to perform this comparison without constru
 intermediate `Ord` instance. `Ordering.then` can be used to lexicographically combine the results of
 comparisons.
 -/
-protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
+@[expose] protected def lex' (ord₁ ord₂ : Ord α) : Ord α where
   compare := compareLex ord₁.compare ord₂.compare
 
 end Ord
diff --git a/src/Std/Classes.lean b/src/Std/Classes.lean
index c37eb9344c..0c9321f28e 100644
--- a/src/Std/Classes.lean
+++ b/src/Std/Classes.lean
@@ -3,5 +3,9 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul Reichert
 -/
+module
+
 prelude
-import Std.Classes.Ord
+public import Std.Classes.Ord
+
+public section
diff --git a/src/Std/Classes/Ord.lean b/src/Std/Classes/Ord.lean
index cd2e2005e2..7b68dceb9e 100644
--- a/src/Std/Classes/Ord.lean
+++ b/src/Std/Classes/Ord.lean
@@ -3,10 +3,14 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+module
+
 prelude
-import Std.Classes.Ord.Basic
-import Std.Classes.Ord.SInt
-import Std.Classes.Ord.UInt
-import Std.Classes.Ord.String
-import Std.Classes.Ord.BitVec
-import Std.Classes.Ord.Vector
+public import Std.Classes.Ord.Basic
+public import Std.Classes.Ord.SInt
+public import Std.Classes.Ord.UInt
+public import Std.Classes.Ord.String
+public import Std.Classes.Ord.BitVec
+public import Std.Classes.Ord.Vector
+
+public section
diff --git a/src/Std/Classes/Ord/Basic.lean b/src/Std/Classes/Ord/Basic.lean
index bac57d0048..750b86e580 100644
--- a/src/Std/Classes/Ord/Basic.lean
+++ b/src/Std/Classes/Ord/Basic.lean
@@ -3,8 +3,12 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Paul Reichert, Robin Arnez
 -/
+module
+
 prelude
-import Init.Data.Ord
+public import Init.Data.Ord
+
+public section
 
 /-!
 # Type classes related to `Ord`
@@ -82,7 +86,7 @@ instance [OrientedCmp cmp] : ReflCmp cmp where
 instance OrientedCmp.opposite [OrientedCmp cmp] : OrientedCmp fun a b => cmp b a where
   eq_swap := OrientedCmp.eq_swap (cmp := cmp)
 
-instance OrientedOrd.opposite [Ord α] [OrientedOrd α] : letI := Ord.opposite ‹_›; OrientedOrd α :=
+instance OrientedOrd.opposite [Ord α] [OrientedOrd α] : letI := Ord.opposite (α := α) ‹_›; OrientedOrd α :=
   OrientedCmp.opposite (cmp := compare)
 
 theorem OrientedCmp.gt_iff_lt [OrientedCmp cmp] {a b : α} : cmp a b = .gt ↔ cmp b a = .lt := by
@@ -197,7 +201,7 @@ theorem TransOrd.isGE_trans [Ord α] [TransOrd α] {a b c : α} :
 instance TransCmp.opposite [TransCmp cmp] : TransCmp fun a b => cmp b a where
   isLE_trans := flip TransCmp.isLE_trans
 
-instance TransOrd.opposite [Ord α] [TransOrd α] : letI := Ord.opposite ‹_›; TransOrd α :=
+instance TransOrd.opposite [Ord α] [TransOrd α] : letI := Ord.opposite (α := α) ‹_›; TransOrd α :=
   TransCmp.opposite (cmp := compare)
 
 theorem TransCmp.lt_of_lt_of_eq [TransCmp cmp] {a b c : α} (hab : cmp a b = .lt)
@@ -330,7 +334,7 @@ instance LawfulEqCmp.opposite [OrientedCmp cmp] [LawfulEqCmp cmp] :
     exact LawfulEqCmp.eq_of_compare
 
 instance LawfulEqOrd.opposite [Ord α] [OrientedOrd α] [LawfulEqOrd α] :
-    letI := Ord.opposite ‹_›; LawfulEqOrd α :=
+    letI := Ord.opposite (α := α) ‹_›; LawfulEqOrd α :=
   LawfulEqCmp.opposite (cmp := compare)
 
 theorem LawfulEqCmp.compare_eq_iff_eq {a b : α} : cmp a b = .eq ↔ a = b :=
@@ -449,7 +453,7 @@ instance LawfulBEqCmp.opposite [OrientedCmp cmp] [LawfulBEqCmp cmp] :
     simp [OrientedCmp.eq_comm (cmp := cmp), LawfulBEqCmp.compare_eq_iff_beq]
 
 instance LawfulBEqOrd.opposite [Ord α] [OrientedOrd α] [LawfulBEqOrd α] :
-    letI := Ord.opposite ‹_›; LawfulBEqOrd α :=
+    letI := Ord.opposite (α := α) ‹_›; LawfulBEqOrd α :=
   LawfulBEqCmp.opposite (cmp := compare)
 
 end LawfulBEq
diff --git a/src/Std/Classes/Ord/BitVec.lean b/src/Std/Classes/Ord/BitVec.lean
index 1ec159aa94..9a102f4c69 100644
--- a/src/Std/Classes/Ord/BitVec.lean
+++ b/src/Std/Classes/Ord/BitVec.lean
@@ -3,9 +3,13 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Paul Reichert, Robin Arnez
 -/
+module
+
 prelude
-import Std.Classes.Ord.Basic
-import Init.Data.BitVec.Lemmas
+public import Std.Classes.Ord.Basic
+public import Init.Data.BitVec.Lemmas
+
+public section
 
 /-!
 # Instances for strings.
diff --git a/src/Std/Classes/Ord/SInt.lean b/src/Std/Classes/Ord/SInt.lean
index 732da75f78..3a628521e3 100644
--- a/src/Std/Classes/Ord/SInt.lean
+++ b/src/Std/Classes/Ord/SInt.lean
@@ -3,9 +3,13 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Paul Reichert, Robin Arnez
 -/
+module
+
 prelude
-import Std.Classes.Ord.Basic
-import Init.Data.SInt.Lemmas
+public import Std.Classes.Ord.Basic
+public import Init.Data.SInt.Lemmas
+
+public section
 
 /-!
 # Instances for fixed width signed integer types.
diff --git a/src/Std/Classes/Ord/String.lean b/src/Std/Classes/Ord/String.lean
index 145779f73b..018a4e09a8 100644
--- a/src/Std/Classes/Ord/String.lean
+++ b/src/Std/Classes/Ord/String.lean
@@ -3,9 +3,13 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Paul Reichert, Robin Arnez
 -/
+module
+
 prelude
-import Std.Classes.Ord.Basic
-import Init.Data.String.Lemmas
+public import Std.Classes.Ord.Basic
+public import Init.Data.String.Lemmas
+
+public section
 
 /-!
 # Instances for strings.
diff --git a/src/Std/Classes/Ord/UInt.lean b/src/Std/Classes/Ord/UInt.lean
index 1dfb74cd65..7e212a9419 100644
--- a/src/Std/Classes/Ord/UInt.lean
+++ b/src/Std/Classes/Ord/UInt.lean
@@ -3,9 +3,13 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Paul Reichert, Robin Arnez
 -/
+module
+
 prelude
-import Std.Classes.Ord.Basic
-import Init.Data.UInt.Lemmas
+public import Std.Classes.Ord.Basic
+public import Init.Data.UInt.Lemmas
+
+public section
 
 /-!
 # Instances for fixed width unsigned integer types.
diff --git a/src/Std/Classes/Ord/Vector.lean b/src/Std/Classes/Ord/Vector.lean
index 7d2a5c5c1b..48d6179e89 100644
--- a/src/Std/Classes/Ord/Vector.lean
+++ b/src/Std/Classes/Ord/Vector.lean
@@ -3,9 +3,13 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Paul Reichert, Robin Arnez
 -/
+module
+
 prelude
-import Std.Classes.Ord.Basic
-import Init.Data.Vector.Lemmas
+public import Std.Classes.Ord.Basic
+public import Init.Data.Vector.Lemmas
+
+public section
 
 /-!
 # Instances for `Vector`