From 6142fe435e77645bbc57f6f7df84499286bcc452 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 28 Jan 2025 13:00:39 +1100
Subject: [PATCH] chore: don't export Trans.trans

---
 src/Init/Data/List/Sublist.lean | 4 ++--
 src/Init/Prelude.lean           | 2 --
 2 files changed, 2 insertions(+), 4 deletions(-)

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'