diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean
index 860ae0aa7f21..bc2e912f15c2 100644
--- a/src/Init/Data/List/Sublist.lean
+++ b/src/Init/Data/List/Sublist.lean
@@ -192,10 +192,10 @@ theorem Sublist.getLast_mem (s : ys <+ xs) (h) : ys.getLast h ∈ xs :=
   s.mem (List.getLast_mem h)
 
 instance : Trans (@Sublist α) Subset Subset :=
-  ⟨fun h₁ h₂ => trans h₁.subset h₂⟩
+  ⟨fun h₁ h₂ => Trans.trans h₁.subset h₂⟩
 
 instance : Trans Subset (@Sublist α) Subset :=
-  ⟨fun h₁ h₂ => trans h₁ h₂.subset⟩
+  ⟨fun h₁ h₂ => Trans.trans h₁ h₂.subset⟩
 
 instance : Trans (fun l₁ l₂ => Sublist l₂ l₁) (Membership.mem : List α → α → Prop) Membership.mem :=
   ⟨fun h₁ h₂ => h₁.subset h₂⟩
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 77a3446fea09..13a2820d0075 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1173,8 +1173,6 @@ class Trans (r : α → β → Sort u) (s : β → γ → Sort v) (t : outParam
   /-- Compose two proofs by transitivity, generalized over the relations involved. -/
   trans : r a b → s b c → t a c
 
-export Trans (trans)
-
 instance (r : α → γ → Sort u) : Trans Eq r r where
   trans heq h' := heq ▸ h'
 
diff --git a/tests/lean/run/trans.lean b/tests/lean/run/trans.lean
index 417886186be7..7b57b7854eb3 100644
--- a/tests/lean/run/trans.lean
+++ b/tests/lean/run/trans.lean
@@ -5,7 +5,7 @@ instance : Trans (α := Int) (β := Int) (γ := Int) (.≤.) (.≤.) (.≤.) whe
   trans := sorry
 
 theorem ex1 {a b c d : Nat} (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) : a ≤ d :=
-  trans h1 <| trans h2 h3
+  Trans.trans h1 <| Trans.trans h2 h3
 
 theorem ex2 {a b c d : Int} (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) : a ≤ d :=
-  trans h1 <| trans h2 h3
+  Trans.trans h1 <| Trans.trans h2 h3