From 30d3092f31f2550f6a2d29e5640612ae46b79d4c Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Wed, 6 May 2026 16:50:50 -0600
Subject: [PATCH] no expose

---
 Mathlib/Order/SuccPred/LinearLocallyFinite.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Order/SuccPred/LinearLocallyFinite.lean b/Mathlib/Order/SuccPred/LinearLocallyFinite.lean
index eb6e8f5d04a91f..b531ef801dbeff 100644
--- a/Mathlib/Order/SuccPred/LinearLocallyFinite.lean
+++ b/Mathlib/Order/SuccPred/LinearLocallyFinite.lean
@@ -55,8 +55,7 @@ About `toZ`:
 
 -/
 
-@[expose] public section
-
+public section
 
 open Order