diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean
index 5554d152fc..89c0fcb49e 100644
--- a/src/Init/Control/Basic.lean
+++ b/src/Init/Control/Basic.lean
@@ -48,7 +48,7 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
 /--
 Extracts the value from a `ForInStep`, ignoring whether it is `ForInStep.done` or `ForInStep.yield`.
 -/
-@[expose] def ForInStep.value (x : ForInStep α) : α :=
+def ForInStep.value (x : ForInStep α) : α :=
   match x with
   | ForInStep.done b => b
   | ForInStep.yield b => b
diff --git a/src/Init/Control/Do.lean b/src/Init/Control/Do.lean
index 68b0707360..7f5eeb41bb 100644
--- a/src/Init/Control/Do.lean
+++ b/src/Init/Control/Do.lean
@@ -19,29 +19,27 @@ non-algebraic higher-order effect combinators such as `tryCatch`.
 -/
 
 /-- A wrapper around `ExceptT` signifying early return. -/
-@[expose]
 abbrev EarlyReturnT (ρ m α) := ExceptT ρ m α
 
 /-- Exit a computation by returning a value `r : ρ` early. -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 abbrev EarlyReturnT.return {ρ m α} [Monad m] (r : ρ) : EarlyReturnT ρ m α :=
   throw r
 
 /-- A specialization of `Except.casesOn`. -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 abbrev EarlyReturn.runK {ρ α : Type u} {β : Type v} (x : Except ρ α) (ret : ρ → β) (pure : α → β) : β :=
   x.casesOn ret pure
 
 /-- A wrapper around `OptionT` signifying `break` in a loop. -/
-@[expose]
 abbrev BreakT := OptionT
 
 /-- Exit a loop body via `break`. -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 abbrev BreakT.break {m : Type w → Type x} [Monad m] : BreakT m α := failure
 
 /-- A specialization of `Option.casesOn`. -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 abbrev Break.runK {α : Type u} {β : Type v} (x : Option α) (breakK : Unit → β) (successK : α → β) : β :=
   -- Note: The matcher below is used in the elaborator targeting `forIn` loops.
   -- If you change the order of match arms here, you may need to adjust the elaborator.
@@ -50,14 +48,13 @@ abbrev Break.runK {α : Type u} {β : Type v} (x : Option α) (breakK : Unit →
   | none => breakK ()
 
 /-- A wrapper around `OptionT` signifying `continue` in a loop. -/
-@[expose]
 abbrev ContinueT := OptionT
 
 /-- Exit a loop body via `continue`. -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 abbrev ContinueT.continue {m : Type w → Type x} [Monad m] : ContinueT m α := failure
 
 /-- A specialization of `Option.casesOn`. -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 abbrev Continue.runK {α : Type u} {β : Type v} (x : Option α) (continueK : Unit → β) (successK : α → β) : β :=
   x.casesOn continueK (fun a _ => successK a) ()
diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index e1d048c49c..01fa752649 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -128,7 +128,7 @@ end Except
 /--
 Adds exceptions of type `ε` to a monad `m`.
 -/
-@[expose] def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
+def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
   m (Except ε α)
 
 /--
@@ -137,7 +137,7 @@ may throw the corresponding exception.
 
 This is the inverse of `ExceptT.run`.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def ExceptT.mk {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) : ExceptT ε m α := x
 
 /--
@@ -145,14 +145,14 @@ Use a monadic action that may throw an exception as an action that may return an
 
 This is the inverse of `ExceptT.mk`.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α) := x
 
 /--
 Use a monadic action that may throw an exception by providing explicit success and failure
 continuations.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def ExceptT.runK [Monad m] (x : ExceptT ε m α) (ok : α → m β) (error : ε → m β) : m β :=
   x.run >>= (·.casesOn error ok)
 
@@ -161,7 +161,7 @@ Returns the value of a computation, forgetting whether it was an exception or a
 
 This corresponds to early return.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def ExceptT.runCatch [Monad m] (x : ExceptT α m α) : m α :=
   x.runK pure pure
 
@@ -172,14 +172,14 @@ variable {ε : Type u} {m : Type u → Type v} [Monad m]
 /--
 Returns the value `a` without throwing exceptions or having any other effect.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 protected def pure {α : Type u} (a : α) : ExceptT ε m α :=
   ExceptT.mk <| pure (Except.ok a)
 
 /--
 Handles exceptions thrown by an action that can have no effects _other_ than throwing exceptions.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 protected def bindCont {α β : Type u} (f : α → ExceptT ε m β) : Except ε α → m (Except ε β)
   | Except.ok a    => f a
   | Except.error e => pure (Except.error e)
@@ -188,14 +188,14 @@ protected def bindCont {α β : Type u} (f : α → ExceptT ε m β) : Except ε
 Sequences two actions that may throw exceptions. Typically used via `do`-notation or the `>>=`
 operator.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 protected def bind {α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) : ExceptT ε m β :=
   ExceptT.mk <| ma >>= ExceptT.bindCont f
 
 /--
 Transforms a successful computation's value using `f`. Typically used via the `<$>` operator.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 protected def map {α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m β :=
   ExceptT.mk <| x >>= fun a => match a with
     | (Except.ok a)    => pure <| Except.ok (f a)
@@ -204,7 +204,7 @@ protected def map {α β : Type u} (f : α → β) (x : ExceptT ε m α) : Excep
 /--
 Runs a computation from an underlying monad in the transformed monad with exceptions.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 protected def lift {α : Type u} (t : m α) : ExceptT ε m α :=
   ExceptT.mk <| Except.ok <$> t
 
@@ -215,7 +215,7 @@ instance : MonadLift m (ExceptT ε m) := ⟨ExceptT.lift⟩
 /--
 Handles exceptions produced in the `ExceptT ε` transformer.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 protected def tryCatch {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m α :=
   ExceptT.mk <| ma >>= fun res => match res with
    | Except.ok a    => pure (Except.ok a)
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 21c3f2d92f..4496fd76d7 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -54,7 +54,7 @@ eq_norm ctx p q (eagerReduce (Eq.refl true)) h
 to instruct the kernel to use eager reduction when establishing that `(p.norm == q) = true` is
 definitionally equal to `true = true`.
 -/
-@[expose] def eagerReduce {α : Sort u} (a : α) : α := a
+def eagerReduce {α : Sort u} (a : α) : α := a
 
 /--
 `flip f a b` is `f b a`. It is useful for "point-free" programming,
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 175d15d50c..07c71162a3 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -69,7 +69,7 @@ end subsingleton
 section zero_allOnes
 
 /-- Returns a bitvector of size `n` where all bits are `0`. -/
-@[expose] protected def zero (n : Nat) : BitVec n := .ofNatLT 0 (Nat.two_pow_pos n)
+protected def zero (n : Nat) : BitVec n := .ofNatLT 0 (Nat.two_pow_pos n)
 instance : Inhabited (BitVec n) where default := .zero n
 
 /-- Returns a bitvector of size `n` where all bits are `1`. -/
@@ -83,10 +83,10 @@ section getXsb
 /--
 Returns the `i`th least significant bit.
 -/
-@[inline, expose] def getLsb (x : BitVec w) (i : Fin w) : Bool := x.toNat.testBit i
+@[inline] def getLsb (x : BitVec w) (i : Fin w) : Bool := x.toNat.testBit i
 
 /-- Returns the `i`th least significant bit, or `none` if `i ≥ w`. -/
-@[inline, expose] def getLsb? (x : BitVec w) (i : Nat) : Option Bool :=
+@[inline] def getLsb? (x : BitVec w) (i : Nat) : Option Bool :=
   if h : i < w then some (getLsb x ⟨i, h⟩) else none
 
 /--
@@ -99,7 +99,7 @@ Returns the `i`th most significant bit.
   if h : i < w then some (getMsb x ⟨i, h⟩) else none
 
 /-- Returns the `i`th least significant bit or `false` if `i ≥ w`. -/
-@[inline, expose] def getLsbD (x : BitVec w) (i : Nat) : Bool :=
+@[inline] def getLsbD (x : BitVec w) (i : Nat) : Bool :=
   x.toNat.testBit i
 
 /-- Returns the `i`th most significant bit, or `false` if `i ≥ w`. -/
@@ -139,7 +139,6 @@ section Int
 /--
 Interprets the bitvector as an integer stored in two's complement form.
 -/
-@[expose]
 protected def toInt (x : BitVec n) : Int :=
   if 2 * x.toNat < 2^n then
     x.toNat
@@ -153,7 +152,6 @@ over- and underflowing as needed.
 The underlying `Nat` is `(2^n + (i mod 2^n)) mod 2^n`. Converting the bitvector back to an `Int`
 with `BitVec.toInt` results in the value `i.bmod (2^n)`.
 -/
-@[expose]
 protected def ofInt (n : Nat) (i : Int) : BitVec n := .ofNatLT (i % (Int.ofNat (2^n))).toNat (by
   apply (Int.toNat_lt _).mpr
   · apply Int.emod_lt_of_pos
@@ -228,14 +226,12 @@ Usually accessed via the `-` prefix operator.
 
 SMT-LIB name: `bvneg`.
 -/
-@[expose]
 protected def neg (x : BitVec n) : BitVec n := .ofNat n (2^n - x.toNat)
 instance : Neg (BitVec n) := ⟨.neg⟩
 
 /--
 Returns the absolute value of a signed bitvector.
 -/
-@[expose]
 protected def abs (x : BitVec n) : BitVec n := if x.msb then .neg x else x
 
 /--
@@ -244,7 +240,6 @@ modulo `2^n`. Usually accessed via the `*` operator.
 
 SMT-LIB name: `bvmul`.
 -/
-@[expose]
 protected def mul (x y : BitVec n) : BitVec n := BitVec.ofNat n (x.toNat * y.toNat)
 instance : Mul (BitVec n) := ⟨.mul⟩
 
@@ -255,7 +250,6 @@ Note that this is currently an inefficient implementation,
 and should be replaced via an `@[extern]` with a native implementation.
 See https://github.com/leanprover/lean4/issues/7887.
 -/
-@[expose]
 protected def pow (x : BitVec n) (y : Nat) : BitVec n :=
   match y with
   | 0 => 1
@@ -267,7 +261,6 @@ instance : Pow (BitVec n) Nat where
 Unsigned division of bitvectors using the Lean convention where division by zero returns zero.
 Usually accessed via the `/` operator.
 -/
-@[expose]
 def udiv (x y : BitVec n) : BitVec n :=
   (x.toNat / y.toNat)#'(by exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) x.isLt)
 instance : Div (BitVec n) := ⟨.udiv⟩
@@ -277,7 +270,6 @@ Unsigned modulo for bitvectors. Usually accessed via the `%` operator.
 
 SMT-LIB name: `bvurem`.
 -/
-@[expose]
 def umod (x y : BitVec n) : BitVec n :=
   (x.toNat % y.toNat)#'(by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt)
 instance : Mod (BitVec n) := ⟨.umod⟩
@@ -289,7 +281,6 @@ where division by zero returns `BitVector.allOnes n`.
 
 SMT-LIB name: `bvudiv`.
 -/
-@[expose]
 def smtUDiv (x y : BitVec n) : BitVec n := if y = 0 then allOnes n else udiv x y
 
 /--
@@ -359,7 +350,6 @@ end arithmetic
 section bool
 
 /-- Turns a `Bool` into a bitvector of length `1`. -/
-@[expose]
 def ofBool (b : Bool) : BitVec 1 := cond b 1 0
 
 @[simp, grind =] theorem ofBool_false : ofBool false = 0 := by trivial
@@ -377,7 +367,6 @@ Unsigned less-than for bitvectors.
 
 SMT-LIB name: `bvult`.
 -/
-@[expose]
 protected def ult (x y : BitVec n) : Bool := x.toNat < y.toNat
 
 /--
@@ -385,7 +374,6 @@ Unsigned less-than-or-equal-to for bitvectors.
 
 SMT-LIB name: `bvule`.
 -/
-@[expose]
 protected def ule (x y : BitVec n) : Bool := x.toNat ≤ y.toNat
 
 /--
@@ -397,7 +385,6 @@ Examples:
  * `BitVec.slt 6#4 7 = true`
  * `BitVec.slt 7#4 8 = false`
 -/
-@[expose]
 protected def slt (x y : BitVec n) : Bool := x.toInt < y.toInt
 
 /--
@@ -405,7 +392,6 @@ Signed less-than-or-equal-to for bitvectors.
 
 SMT-LIB name: `bvsle`.
 -/
-@[expose]
 protected def sle (x y : BitVec n) : Bool := x.toInt ≤ y.toInt
 
 end relations
@@ -419,7 +405,7 @@ width `m`.
 Using `x.cast eq` should be preferred over `eq ▸ x` because there are special-purpose `simp` lemmas
 that can more consistently simplify `BitVec.cast` away.
 -/
-@[inline, expose] protected def cast (eq : n = m) (x : BitVec n) : BitVec m := .ofNatLT x.toNat (eq ▸ x.isLt)
+@[inline] protected def cast (eq : n = m) (x : BitVec n) : BitVec m := .ofNatLT x.toNat (eq ▸ x.isLt)
 
 @[simp, grind =] theorem cast_ofNat {n m : Nat} (h : n = m) (x : Nat) :
     (BitVec.ofNat n x).cast h = BitVec.ofNat m x := by
@@ -435,7 +421,6 @@ that can more consistently simplify `BitVec.cast` away.
 Extracts the bits `start` to `start + len - 1` from a bitvector of size `n` to yield a
 new bitvector of size `len`. If `start + len > n`, then the bitvector is zero-extended.
 -/
-@[expose]
 def extractLsb' (start len : Nat) (x : BitVec n) : BitVec len := .ofNat _ (x.toNat >>> start)
 
 /--
@@ -446,7 +431,6 @@ The resulting bitvector has size `hi - lo + 1`.
 
 SMT-LIB name: `extract`.
 -/
-@[expose]
 def extractLsb (hi lo : Nat) (x : BitVec n) : BitVec (hi - lo + 1) := extractLsb' lo _ x
 
 /--
@@ -455,7 +439,6 @@ Increases the width of a bitvector to one that is at least as large by zero-exte
 This is a constant-time operation because the underlying `Nat` is unmodified; because the new width
 is at least as large as the old one, no overflow is possible.
 -/
-@[expose]
 def setWidth' {n w : Nat} (le : n ≤ w) (x : BitVec n) : BitVec w :=
   x.toNat#'(by
     apply Nat.lt_of_lt_of_le x.isLt
@@ -464,7 +447,6 @@ def setWidth' {n w : Nat} (le : n ≤ w) (x : BitVec n) : BitVec w :=
 /--
 Returns `zeroExtend (w+n) x <<< n` without needing to compute `x % 2^(2+n)`.
 -/
-@[expose]
 def shiftLeftZeroExtend (msbs : BitVec w) (m : Nat) : BitVec (w + m) :=
   let shiftLeftLt {x : Nat} (p : x < 2^w) (m : Nat) : x <<< m < 2^(w + m) := by
         simp [Nat.shiftLeft_eq, Nat.pow_add]
@@ -521,7 +503,6 @@ SMT-LIB name: `bvand`.
 Example:
  * `0b1010#4 &&& 0b0110#4 = 0b0010#4`
 -/
-@[expose]
 protected def and (x y : BitVec n) : BitVec n :=
   (x.toNat &&& y.toNat)#'(by exact Nat.and_lt_two_pow x.toNat y.isLt)
 instance : AndOp (BitVec w) := ⟨.and⟩
@@ -534,7 +515,6 @@ SMT-LIB name: `bvor`.
 Example:
  * `0b1010#4 ||| 0b0110#4 = 0b1110#4`
 -/
-@[expose]
 protected def or (x y : BitVec n) : BitVec n :=
   (x.toNat ||| y.toNat)#'(by exact Nat.or_lt_two_pow x.isLt y.isLt)
 instance : OrOp (BitVec w) := ⟨.or⟩
@@ -547,7 +527,6 @@ SMT-LIB name: `bvxor`.
 Example:
  * `0b1010#4 ^^^ 0b0110#4 = 0b1100#4`
 -/
-@[expose]
 protected def xor (x y : BitVec n) : BitVec n :=
   (x.toNat ^^^ y.toNat)#'(by exact Nat.xor_lt_two_pow x.isLt y.isLt)
 instance : XorOp (BitVec w) := ⟨.xor⟩
@@ -560,7 +539,6 @@ SMT-LIB name: `bvnot`.
 Example:
  * `~~~(0b0101#4) == 0b1010`
 -/
-@[expose]
 protected def not (x : BitVec n) : BitVec n := allOnes n ^^^ x
 instance : Complement (BitVec w) := ⟨.not⟩
 
@@ -570,7 +548,6 @@ equivalent to `x * 2^s`, modulo `2^n`.
 
 SMT-LIB name: `bvshl` except this operator uses a `Nat` shift value.
 -/
-@[expose]
 protected def shiftLeft (x : BitVec n) (s : Nat) : BitVec n := BitVec.ofNat n (x.toNat <<< s)
 instance : HShiftLeft (BitVec w) Nat (BitVec w) := ⟨.shiftLeft⟩
 
@@ -582,7 +559,6 @@ As a numeric operation, this is equivalent to `x / 2^s`, rounding down.
 
 SMT-LIB name: `bvlshr` except this operator uses a `Nat` shift value.
 -/
-@[expose]
 def ushiftRight (x : BitVec n) (s : Nat) : BitVec n :=
   (x.toNat >>> s)#'(by
   let ⟨x, lt⟩ := x
@@ -600,7 +576,6 @@ As a numeric operation, this is equivalent to `x.toInt >>> s`.
 
 SMT-LIB name: `bvashr` except this operator uses a `Nat` shift value.
 -/
-@[expose]
 def sshiftRight (x : BitVec n) (s : Nat) : BitVec n := .ofInt n (x.toInt >>> s)
 
 instance {n} : HShiftLeft  (BitVec m) (BitVec n) (BitVec m) := ⟨fun x y => x <<< y.toNat⟩
@@ -614,12 +589,10 @@ As a numeric operation, this is equivalent to `a.toInt >>> s.toNat`.
 
 SMT-LIB name: `bvashr`.
 -/
-@[expose]
 def sshiftRight' (a : BitVec n) (s : BitVec m) : BitVec n := a.sshiftRight s.toNat
 
 /-- Auxiliary function for `rotateLeft`, which does not take into account the case where
 the rotation amount is greater than the bitvector width. -/
-@[expose]
 def rotateLeftAux (x : BitVec w) (n : Nat) : BitVec w :=
   x <<< n ||| x >>> (w - n)
 
@@ -634,7 +607,6 @@ SMT-LIB name: `rotate_left`, except this operator uses a `Nat` shift amount.
 Example:
  * `(0b0011#4).rotateLeft 3 = 0b1001`
 -/
-@[expose]
 def rotateLeft (x : BitVec w) (n : Nat) : BitVec w := rotateLeftAux x (n % w)
 
 
@@ -642,7 +614,6 @@ def rotateLeft (x : BitVec w) (n : Nat) : BitVec w := rotateLeftAux x (n % w)
 Auxiliary function for `rotateRight`, which does not take into account the case where
 the rotation amount is greater than the bitvector width.
 -/
-@[expose]
 def rotateRightAux (x : BitVec w) (n : Nat) : BitVec w :=
   x >>> n ||| x <<< (w - n)
 
@@ -657,7 +628,6 @@ SMT-LIB name: `rotate_right`, except this operator uses a `Nat` shift amount.
 Example:
  * `rotateRight 0b01001#5 1 = 0b10100`
 -/
-@[expose]
 def rotateRight (x : BitVec w) (n : Nat) : BitVec w := rotateRightAux x (n % w)
 
 /--
@@ -669,7 +639,6 @@ SMT-LIB name: `concat`.
 Example:
  * `0xAB#8 ++ 0xCD#8 = 0xABCD#16`.
 -/
-@[expose]
 def append (msbs : BitVec n) (lsbs : BitVec m) : BitVec (n+m) :=
   shiftLeftZeroExtend msbs m ||| setWidth' (Nat.le_add_left m n) lsbs
 
@@ -692,7 +661,6 @@ result of appending a single bit to the front in the naive implementation).
 
 /-- Append a single bit to the end of a bitvector, using big endian order (see `append`).
     That is, the new bit is the least significant bit. -/
-@[expose]
 def concat {n} (msbs : BitVec n) (lsb : Bool) : BitVec (n+1) := msbs ++ (ofBool lsb)
 
 /--
@@ -700,7 +668,6 @@ Shifts all bits of `x` to the left by `1` and sets the least significant bit to
 
 This is a non-dependent version of `BitVec.concat` that does not change the total bitwidth.
 -/
-@[expose]
 def shiftConcat (x : BitVec n) (b : Bool) : BitVec n :=
   (x.concat b).truncate n
 
@@ -709,7 +676,6 @@ Prepends a single bit to the front of a bitvector, using big-endian order (see `
 
 The new bit is the most significant bit.
 -/
-@[expose]
 def cons {n} (msb : Bool) (lsbs : BitVec n) : BitVec (n+1) :=
   ((ofBool msb) ++ lsbs).cast (Nat.add_comm ..)
 
@@ -734,10 +700,10 @@ def twoPow (w : Nat) (i : Nat) : BitVec w := 1#w <<< i
 end bitwise
 
 /-- The bitvector of width `w` that has the smallest value when interpreted as an integer. -/
-@[expose] def intMin (w : Nat) := twoPow w (w - 1)
+def intMin (w : Nat) := twoPow w (w - 1)
 
 /-- The bitvector of width `w` that has the largest value when interpreted as an integer. -/
-@[expose] def intMax (w : Nat) := (twoPow w (w - 1)) - 1
+def intMax (w : Nat) := (twoPow w (w - 1)) - 1
 
 /--
 Computes a hash of a bitvector, combining 64-bit words using `mixHash`.
@@ -802,7 +768,6 @@ Checks whether subtraction of `x` and `y` results in *unsigned* overflow.
 
 SMT-Lib name: `bvusubo`.
 -/
-@[expose]
 def usubOverflow {w : Nat} (x y : BitVec w) : Bool := x.toNat < y.toNat
 
 /--
@@ -811,7 +776,6 @@ Checks whether the subtraction of `x` and `y` results in *signed* overflow, trea
 
 SMT-Lib name: `bvssubo`.
 -/
-@[expose]
 def ssubOverflow {w : Nat} (x y : BitVec w) : Bool :=
   (x.toInt - y.toInt ≥ 2 ^ (w - 1)) || (x.toInt - y.toInt < - 2 ^ (w - 1))
 
@@ -822,7 +786,6 @@ For a bitvector `x` with nonzero width, this only happens if `x = intMin`.
 
 SMT-Lib name: `bvnego`.
 -/
-@[expose]
 def negOverflow {w : Nat} (x : BitVec w) : Bool :=
   x.toInt == - 2 ^ (w - 1)
 
@@ -832,7 +795,6 @@ For BitVecs `x` and `y` with nonzero width, this only happens if `x = intMin` an
 
 SMT-LIB name: `bvsdivo`.
 -/
-@[expose]
 def sdivOverflow {w : Nat} (x y : BitVec w) : Bool :=
   (2 ^ (w - 1) ≤ x.toInt / y.toInt) || (x.toInt / y.toInt <  - 2 ^ (w - 1))
 
diff --git a/src/Init/Data/Char/Basic.lean b/src/Init/Data/Char/Basic.lean
index 2d52b6788e..60b5554fa5 100644
--- a/src/Init/Data/Char/Basic.lean
+++ b/src/Init/Data/Char/Basic.lean
@@ -23,13 +23,13 @@ namespace Char
 /--
 One character is less than another if its code point is strictly less than the other's.
 -/
-@[expose] protected def lt (a b : Char) : Prop := a.val < b.val
+protected def lt (a b : Char) : Prop := a.val < b.val
 
 /--
 One character is less than or equal to another if its code point is less than or equal to the
 other's.
 -/
-@[expose] protected def le (a b : Char) : Prop := a.val ≤ b.val
+protected def le (a b : Char) : Prop := a.val ≤ b.val
 
 instance : LT Char := ⟨Char.lt⟩
 instance : LE Char := ⟨Char.le⟩
diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index 4ed9b2c3e8..e4f0208e41 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -50,7 +50,7 @@ Returns `a` modulo `n` as a `Fin n`.
 
 The assumption `NeZero n` ensures that `Fin n` is nonempty.
 -/
-@[expose] protected def ofNat (n : Nat) [NeZero n] (a : Nat) : Fin n :=
+protected def ofNat (n : Nat) [NeZero n] (a : Nat) : Fin n :=
   ⟨a % n, Nat.mod_lt _ (pos_of_neZero n)⟩
 
 @[simp]
diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index e32609ee86..48f4a7fb86 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -123,7 +123,7 @@ For example, for `x : Fin k` and `n : Nat`,
 it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
 silently introducing wraparound arithmetic.
 -/
-@[expose, implicit_reducible]
+@[implicit_reducible]
 def instNatCast (n : Nat) [NeZero n] : NatCast (Fin n) where
   natCast a := Fin.ofNat n a
 
@@ -131,7 +131,6 @@ attribute [scoped instance] instNatCast
 
 end NatCast
 
-@[expose]
 def intCast [NeZero n] (a : Int) : Fin n :=
   if 0 ≤ a then
     Fin.ofNat n a.natAbs
@@ -145,7 +144,7 @@ This is not a global instance, but may be activated locally via `open Fin.IntCas
 
 See the doc-string for `Fin.NatCast.instNatCast` for more details.
 -/
-@[expose, implicit_reducible]
+@[implicit_reducible]
 def instIntCast (n : Nat) [NeZero n] : IntCast (Fin n) where
   intCast := Fin.intCast
 
@@ -909,7 +908,7 @@ parameter, `Fin.cases` is the corresponding case analysis operator, and `Fin.rev
 version that starts at the greatest value instead of `0`.
 -/
 -- FIXME: Performance review
-@[elab_as_elim, expose] def induction {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+@[elab_as_elim] def induction {motive : Fin (n + 1) → Sort _} (zero : motive 0)
     (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
     ∀ i : Fin (n + 1), motive i
   | ⟨i, hi⟩ => go i hi
@@ -951,7 +950,7 @@ The two cases are:
 
 The corresponding induction principle is `Fin.induction`.
 -/
-@[elab_as_elim, expose] def cases {motive : Fin (n + 1) → Sort _}
+@[elab_as_elim] def cases {motive : Fin (n + 1) → Sort _}
     (zero : motive 0) (succ : ∀ i : Fin n, motive i.succ) :
     ∀ i : Fin (n + 1), motive i := induction zero fun i _ => succ i
 
diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index d65040544f..7098c0dad8 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -323,7 +323,7 @@ Examples:
  * `(0 : Int).natAbs = 0`
  * `(-11 : Int).natAbs = 11`
 -/
-@[extern "lean_nat_abs", expose]
+@[extern "lean_nat_abs"]
 def natAbs (m : @& Int) : Nat :=
   match m with
   | ofNat m => m
@@ -413,20 +413,20 @@ instance : Min Int := minOfLe
 instance : Max Int := maxOfLe
 
 /-- Equality predicate for kernel reduction. -/
-@[expose] protected noncomputable def beq' (a b : Int) : Bool :=
+protected noncomputable def beq' (a b : Int) : Bool :=
   Int.rec
     (fun a => Int.rec (fun b => Nat.beq a b) (fun _ => false) b)
     (fun a => Int.rec (fun _ => false) (fun b => Nat.beq a b) b) a
 
 /-- `x ≤ y` for kernel reduction. -/
-@[expose] protected noncomputable def ble' (a b : Int) : Bool :=
+protected noncomputable def ble' (a b : Int) : Bool :=
   Int.rec
     (fun a => Int.rec (fun b => Nat.ble a b) (fun _ => false) b)
     (fun a => Int.rec (fun _ => true) (fun b => Nat.ble b a) b)
     a
 
 /-- `x < y` for kernel reduction. -/
-@[expose] protected noncomputable def blt' (a b : Int) : Bool :=
+protected noncomputable def blt' (a b : Int) : Bool :=
   Int.rec
     (fun a => Int.rec (fun b => Nat.blt a b) (fun _ => false) b)
     (fun a => Int.rec (fun _ => true) (fun b => Nat.blt b a) b)
diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean
index 6c07229912..36244abcf2 100644
--- a/src/Init/Data/Int/Linear.lean
+++ b/src/Init/Data/Int/Linear.lean
@@ -191,7 +191,7 @@ def Poly.combine' (fuel : Nat) (p₁ p₂ : Poly) : Poly :=
     else
       .add a₂ x₂ (combine' fuel (.add a₁ x₁ p₁) p₂)
 
-@[expose] abbrev hugeFuel := 100000000
+abbrev hugeFuel := 100000000
 
 @[expose]
 def Poly.combine (p₁ p₂ : Poly) : Poly :=
diff --git a/src/Init/Data/Iterators/Basic.lean b/src/Init/Data/Iterators/Basic.lean
index 1cfad1a296..297d757614 100644
--- a/src/Init/Data/Iterators/Basic.lean
+++ b/src/Init/Data/Iterators/Basic.lean
@@ -314,7 +314,6 @@ of another state. Having this proof bundled up with the step is important for te
 
 See `IterM.Step` and `Iter.Step` for the concrete choice of the plausibility predicate.
 -/
-@[expose]
 abbrev PlausibleIterStep (IsPlausibleStep : IterStep α β → Prop) := Subtype IsPlausibleStep
 
 /--
@@ -384,7 +383,7 @@ attribute [reducible] Iterator.IsPlausibleStep
 section Monadic
 
 /-- The constructor has been renamed. -/
-@[deprecated IterM.mk (since := "2025-01-19"), inline, expose]
+@[deprecated IterM.mk (since := "2025-01-19"), inline]
 abbrev IterM.mk' {α : Type w} {m : Type w → Type w'} {β : Type w} (it : α) : IterM (α := α) m β :=
   ⟨it⟩
 
@@ -434,7 +433,6 @@ abbrev IterM.IsPlausibleStep {α : Type w} {m : Type w → Type w'} {β : Type w
 The type of the step object returned by `IterM.step`, containing an `IterStep`
 and a proof that this is a plausible step for the given iterator.
 -/
-@[expose]
 abbrev IterM.Step {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
     (it : IterM (α := α) m β) :=
   PlausibleIterStep it.IsPlausibleStep
@@ -493,7 +491,6 @@ section Pure
 Asserts that certain step is plausibly the successor of a given iterator. What "plausible" means
 is up to the `Iterator` instance but it should be strong enough to allow termination proofs.
 -/
-@[expose]
 abbrev Iter.IsPlausibleStep {α : Type w} {β : Type w} [Iterator α Id β]
     (it : Iter (α := α) β) (step : IterStep (Iter (α := α) β) β) : Prop :=
   it.toIterM.IsPlausibleStep (step.mapIterator Iter.toIterM)
@@ -549,7 +546,6 @@ theorem IterM.IsPlausibleIndirectOutput.trans {α β : Type w} {m : Type w → T
 The type of the step object returned by `Iter.step`, containing an `IterStep`
 and a proof that this is a plausible step for the given iterator.
 -/
-@[expose]
 abbrev Iter.Step {α : Type w} {β : Type w} [Iterator α Id β] (it : Iter (α := α) β) :=
   PlausibleIterStep (Iter.IsPlausibleStep it)
 
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/Append.lean b/src/Init/Data/Iterators/Combinators/Monadic/Append.lean
index 2d9855f186..75a51b7f70 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/Append.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/Append.lean
@@ -189,7 +189,6 @@ def Append.instFinitenessRelation [Monad m] [Iterator α₁ m β] [Iterator α
       apply Append.rel_of_snd
       exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
 
-@[no_expose]
 instance Append.instFinite [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
     [Finite α₁ m] [Finite α₂ m] : Finite (Append α₁ α₂ m β) m :=
   .of_finitenessRelation instFinitenessRelation
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
index f35b21b00f..8aac50835f 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
@@ -196,13 +196,11 @@ private def FilterMap.instFinitenessRelation {α β γ : Type w} {m : Type w →
     case done h' =>
       cases h
 
-@[no_expose]
 instance FilterMap.instFinite {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n (Option γ)} [Finite α m] : Finite (FilterMap α m n lift f) n :=
   Finite.of_finitenessRelation FilterMap.instFinitenessRelation
 
-@[no_expose]
 instance Map.instFinite {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [Monad n]
     [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} [Finite α m] :
     Finite (Map α m n lift f) n :=
@@ -221,7 +219,6 @@ private def Map.instProductivenessRelation {α β γ : Type w} {m : Type w → T
     case skip it' h =>
       exact h
 
-@[no_expose]
 instance Map.instProductive {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n γ} [Productive α m] :
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean
index a1ce3074bf..bb8dd3798c 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/FlatMap.lean
@@ -301,7 +301,6 @@ def Flatten.instFinitenessRelation [Monad m] [Iterator α m (IterM (α := α₂)
     case innerDone =>
       apply Flatten.rel_of_right₂
 
-@[no_expose]
 public instance Flatten.instFinite [Monad m] [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
     [Finite α m] [Finite α₂ m] : Finite (Flatten α α₂ β m) m :=
   .of_finitenessRelation instFinitenessRelation
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean
index b91d54e5be..290f4c754c 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/ULift.lean
@@ -31,7 +31,6 @@ instance {n : Type max u v → Type v'} [Monad n] : Monad.{u} (ULiftT n) where
   pure a := pure (f := n) (ULift.up a)
   bind x f := bind (m := n) (x : n _) fun a => f a.down
 
-@[no_expose]
 instance {n : Type max u v → Type v'} [Monad n] [LawfulMonad n] : LawfulMonad.{u} (ULiftT n) where
   map_const := by simp [Functor.mapConst, Functor.map]
   id_map := by simp [Functor.map]
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index ea55cda038..354a7cfb21 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -572,7 +572,7 @@ Examples:
 * `[1, 2, 3, 4].reverse = [4, 3, 2, 1]`
 * `[].reverse = []`
 -/
-@[expose] def reverse (as : List α) : List α :=
+def reverse (as : List α) : List α :=
   reverseAux as []
 
 @[simp, grind =] theorem reverse_nil : reverse ([] : List α) = [] := rfl
@@ -681,7 +681,7 @@ Examples:
  * `List.singleton "green" = ["green"]`.
  * `List.singleton [1, 2, 3] = [[1, 2, 3]]`
 -/
-@[inline, expose] protected def singleton {α : Type u} (a : α) : List α := [a]
+@[inline] protected def singleton {α : Type u} (a : α) : List α := [a]
 
 /-! ### flatMap -/
 
diff --git a/src/Init/Data/List/Lex.lean b/src/Init/Data/List/Lex.lean
index 5b27bfa374..ea3b93b183 100644
--- a/src/Init/Data/List/Lex.lean
+++ b/src/Init/Data/List/Lex.lean
@@ -293,7 +293,6 @@ instance [LT α] [Std.Asymm (· < · : α → α → Prop)] :
     Std.Total (· ≤ · : List α → List α → Prop) where
   total := List.le_total
 
-@[no_expose]
 instance instIsLinearOrder [LT α] [LE α] [IsLinearOrder α] [LawfulOrderLT α] :
     IsLinearOrder (List α) := IsLinearOrder.of_le
 
diff --git a/src/Init/Data/Ord/Basic.lean b/src/Init/Data/Ord/Basic.lean
index dea4c6a5cb..2eda2fa5eb 100644
--- a/src/Init/Data/Ord/Basic.lean
+++ b/src/Init/Data/Ord/Basic.lean
@@ -656,19 +656,19 @@ namespace Ord
 /--
 Constructs a `BEq` instance from an `Ord` instance.
 -/
-@[expose] protected abbrev toBEq (ord : Ord α) : BEq α :=
+protected abbrev toBEq (ord : Ord α) : BEq α :=
   beqOfOrd
 
 /--
 Constructs an `LT` instance from an `Ord` instance.
 -/
-@[expose] protected abbrev toLT (ord : Ord α) : LT α :=
+protected abbrev toLT (ord : Ord α) : LT α :=
   ltOfOrd
 
 /--
 Constructs an `LE` instance from an `Ord` instance.
 -/
-@[expose] protected abbrev toLE (ord : Ord α) : LE α :=
+protected abbrev toLE (ord : Ord α) : LE α :=
   leOfOrd
 
 /--
@@ -694,7 +694,7 @@ The function `compareOn` can be used to perform this comparison without construc
 /--
 Constructs the lexicographic order on products `α × β` from orders for `α` and `β`.
 -/
-@[expose] protected abbrev lex (_ : Ord α) (_ : Ord β) : Ord (α × β) :=
+protected abbrev lex (_ : Ord α) (_ : Ord β) : Ord (α × β) :=
   lexOrd
 
 /--
diff --git a/src/Init/Data/Range/Polymorphic/Iterators.lean b/src/Init/Data/Range/Polymorphic/Iterators.lean
index e9a1c2b063..160bb89fe0 100644
--- a/src/Init/Data/Range/Polymorphic/Iterators.lean
+++ b/src/Init/Data/Range/Polymorphic/Iterators.lean
@@ -38,7 +38,7 @@ def Internal.iter [UpwardEnumerable α] (r : Rcc α) : Iter (α := Rxc.Iterator
 /--
 Returns the elements of the given closed range as a list in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toList [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [Rxc.IsAlwaysFinite α] (r : Rcc α) : List α :=
   Internal.iter r |>.toList
@@ -46,7 +46,7 @@ def toList [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerabl
 /--
 Returns the elements of the given closed range as an array in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toArray [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [Rxc.IsAlwaysFinite α] (r : Rcc α) : Array α :=
   Internal.iter r |>.toArray
@@ -124,7 +124,7 @@ def Internal.iter [UpwardEnumerable α] (r : Rco α) : Iter (α := Rxo.Iterator
 /--
 Returns the elements of the given left-closed right-open range as a list in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toList [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [Rxo.IsAlwaysFinite α] (r : Rco α) : List α :=
   Internal.iter r |>.toList
@@ -132,7 +132,7 @@ def toList [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerabl
 /--
 Returns the elements of the given left-closed right-open range as an array in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toArray [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [Rxo.IsAlwaysFinite α] (r : Rco α) : Array α :=
   Internal.iter r |>.toArray
@@ -210,7 +210,7 @@ def Internal.iter [UpwardEnumerable α] (r : Rci α) : Iter (α := Rxi.Iterator
 /--
 Returns the elements of the given left-closed right-unbounded range as a list in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toList [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] (r : Rci α) :
     List α :=
   Internal.iter r |>.toList
@@ -218,7 +218,7 @@ def toList [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite
 /--
 Returns the elements of the given left-closed right-unbounded range as an array in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toArray [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] (r : Rci α) :
     Array α :=
   Internal.iter r |>.toArray
@@ -295,7 +295,7 @@ def Internal.iter [UpwardEnumerable α] (r : Roc α) : Iter (α := Rxc.Iterator
 /--
 Returns the elements of the given left-open right-closed range as a list in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toList [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [Rxc.IsAlwaysFinite α] (r : Roc α) : List α :=
   Internal.iter r |>.toList
@@ -303,7 +303,7 @@ def toList [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerabl
 /--
 Returns the elements of the given left-open right-closed range as an array in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toArray [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [Rxc.IsAlwaysFinite α] (r : Roc α) : Array α :=
   Internal.iter r |>.toArray
@@ -376,7 +376,7 @@ def Internal.iter [UpwardEnumerable α] (r : Roo α) : Iter (α := Rxo.Iterator
 /--
 Returns the elements of the given open range as a list in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toList [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [Rxo.IsAlwaysFinite α] (r : Roo α) : List α :=
   Internal.iter r |>.toList
@@ -384,7 +384,7 @@ def toList [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerabl
 /--
 Returns the elements of the given open range as an array in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toArray [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [Rxo.IsAlwaysFinite α] (r : Roo α) : Array α :=
   Internal.iter r |>.toArray
@@ -456,7 +456,7 @@ def Internal.iter [UpwardEnumerable α] (r : Roi α) : Iter (α := Rxi.Iterator
 /--
 Returns the elements of the given left-open right-unbounded range as a list in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toList[UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α]
     (r : Roi α) : List α :=
   Internal.iter r |>.toList
@@ -464,7 +464,7 @@ def toList[UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite
 /--
 Returns the elements of the given left-open right-unbounded range as an array in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toArray [UpwardEnumerable α] [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α]
     (r : Roi α) : Array α :=
   Internal.iter r |>.toArray
@@ -532,7 +532,7 @@ def Internal.iter [Least? α] (r : Ric α) : Iter (α := Rxc.Iterator α) α :=
 /--
 Returns the elements of the given closed range as a list in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toList [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [Rxc.IsAlwaysFinite α] (r : Ric α) : List α :=
   Internal.iter r |>.toList
@@ -540,7 +540,7 @@ def toList [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpw
 /--
 Returns the elements of the given closed range as an array in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toArray [Least? α] [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [Rxc.IsAlwaysFinite α] (r : Ric α) : Array α :=
   Internal.iter r |>.toArray
@@ -607,7 +607,7 @@ def Internal.iter [UpwardEnumerable α] [Least? α] (r : Rio α) : Iter (α := R
 /--
 Returns the elements of the given closed range as a list in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toList [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [Rxo.IsAlwaysFinite α] (r : Rio α) : List α :=
   Internal.iter r |>.toList
@@ -615,7 +615,7 @@ def toList [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpw
 /--
 Returns the elements of the given closed range as an array in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toArray [Least? α] [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [Rxo.IsAlwaysFinite α] (r : Rio α) : Array α :=
   Internal.iter r |>.toArray
@@ -681,7 +681,7 @@ def Internal.iter [UpwardEnumerable α] [Least? α] (_ : Rii α) : Iter (α := R
 /--
 Returns the elements of the given full range as a list in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toList [UpwardEnumerable α] [Least? α] (r : Rii α)
     [Iterator (Rxi.Iterator α) Id α] [Finite (Rxi.Iterator α) Id] : List α :=
   Internal.iter r |>.toList
@@ -689,7 +689,7 @@ def toList [UpwardEnumerable α] [Least? α] (r : Rii α)
 /--
 Returns the elements of the given full range as an array in ascending order.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def toArray {α} [UpwardEnumerable α] [Least? α] (r : Rii α)
     [Iterator (Rxi.Iterator α) Id α] [Finite (Rxi.Iterator α) Id] : Array α :=
   Internal.iter r |>.toArray
diff --git a/src/Init/Data/Range/Polymorphic/RangeIterator.lean b/src/Init/Data/Range/Polymorphic/RangeIterator.lean
index 765bc11447..94f4c951d5 100644
--- a/src/Init/Data/Range/Polymorphic/RangeIterator.lean
+++ b/src/Init/Data/Range/Polymorphic/RangeIterator.lean
@@ -279,7 +279,6 @@ private def Iterator.instFinitenessRelation [UpwardEnumerable α] [LE α] [Decid
           · cases h
   subrelation := id
 
-@[no_expose]
 instance Iterator.instFinite [UpwardEnumerable α] [LE α] [DecidableLE α]
     [LawfulUpwardEnumerable α] [Rxc.IsAlwaysFinite α] :
     Finite (Rxc.Iterator α) Id :=
@@ -300,7 +299,6 @@ private def Iterator.instProductivenessRelation [UpwardEnumerable α] [LE α] [D
       · cases h
       · cases h
 
-@[no_expose]
 instance Iterator.instProductive [UpwardEnumerable α] [LE α] [DecidableLE α]
     [LawfulUpwardEnumerable α] :
     Productive (Rxc.Iterator α) Id :=
@@ -861,7 +859,6 @@ private def Iterator.instFinitenessRelation [UpwardEnumerable α] [LT α] [Decid
           · cases h
   subrelation := id
 
-@[no_expose]
 instance Iterator.instFinite [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] :
     Finite (Rxo.Iterator α) Id :=
@@ -882,7 +879,6 @@ private def Iterator.instProductivenessRelation [UpwardEnumerable α] [LT α] [D
       · cases h
       · cases h
 
-@[no_expose]
 instance Iterator.instProductive [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] :
     Productive (Rxo.Iterator α) Id :=
@@ -1374,7 +1370,6 @@ private def Iterator.instFinitenessRelation [UpwardEnumerable α]
           exact ih
   subrelation := id
 
-@[no_expose]
 instance Iterator.instFinite [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [Rxi.IsAlwaysFinite α] :
     Finite (Rxi.Iterator α) Id :=
@@ -1391,7 +1386,6 @@ private def Iterator.instProductivenessRelation [UpwardEnumerable α]
       Iterator.IsPlausibleStep, Monadic.step, instIteratorIteratorIdOfUpwardEnumerable] at h -- TODO
     split at h <;> cases h
 
-@[no_expose]
 instance Iterator.instProductive [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] :
     Productive (Rxi.Iterator α) Id :=
diff --git a/src/Init/Data/String/Iterate.lean b/src/Init/Data/String/Iterate.lean
index 9d0a7f6df5..408258e8ae 100644
--- a/src/Init/Data/String/Iterate.lean
+++ b/src/Init/Data/String/Iterate.lean
@@ -82,7 +82,6 @@ private def finitenessRelation [Pure m] :
     · cases h'
     · cases h
 
-@[no_expose]
 instance [Pure m] : Std.Iterators.Finite (PosIterator s) m :=
   .of_finitenessRelation finitenessRelation
 
@@ -170,7 +169,6 @@ private def finitenessRelation [Pure m] :
     · cases h'
     · cases h
 
-@[no_expose]
 instance [Pure m] : Std.Iterators.Finite (RevPosIterator s) m :=
   .of_finitenessRelation finitenessRelation
 
@@ -247,7 +245,6 @@ private def finitenessRelation [Pure m] :
     · cases h'
     · cases h
 
-@[no_expose]
 instance [Pure m] : Std.Iterators.Finite ByteIterator m :=
   .of_finitenessRelation finitenessRelation
 
@@ -325,7 +322,6 @@ private def finitenessRelation [Pure m] :
     · cases h'
     · cases h
 
-@[no_expose]
 instance [Pure m] : Std.Iterators.Finite RevByteIterator m :=
   .of_finitenessRelation finitenessRelation
 
diff --git a/src/Init/Data/String/Pattern/String.lean b/src/Init/Data/String/Pattern/String.lean
index 49e2541d21..b3210bc02d 100644
--- a/src/Init/Data/String/Pattern/String.lean
+++ b/src/Init/Data/String/Pattern/String.lean
@@ -258,7 +258,6 @@ private def finitenessRelation :
       | .atEnd .. => simp
     · cases h
 
-@[no_expose]
 instance : Std.Iterators.Finite (ForwardSliceSearcher s) Id :=
   .of_finitenessRelation finitenessRelation
 
diff --git a/src/Init/Data/String/PosRaw.lean b/src/Init/Data/String/PosRaw.lean
index 505515150d..9f808632b9 100644
--- a/src/Init/Data/String/PosRaw.lean
+++ b/src/Init/Data/String/PosRaw.lean
@@ -108,7 +108,7 @@ At runtime, this function is implemented by efficient, constant-time code.
 def getUTF8Byte (s : @& String) (p : Pos.Raw) (h : p < s.rawEndPos) : UInt8 :=
   s.toByteArray[p.byteIdx]
 
-@[deprecated getUTF8Byte (since := "2025-10-01"), extern "lean_string_get_byte_fast", expose]
+@[deprecated getUTF8Byte (since := "2025-10-01"), extern "lean_string_get_byte_fast"]
 abbrev getUtf8Byte (s : String) (p : Pos.Raw) (h : p < s.rawEndPos) : UInt8 :=
   s.getUTF8Byte p h
 
diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean
index c12feb1ca3..b5a5315645 100644
--- a/src/Init/Data/String/Slice.lean
+++ b/src/Init/Data/String/Slice.lean
@@ -190,7 +190,6 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
       | ⟨.operating _ searcher⟩, ⟨.atEnd⟩ => simp [SplitIterator.toOption, Option.lt]
       | ⟨.atEnd⟩, _ => simp
 
-@[no_expose]
 instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (SplitIterator pat s) Id :=
   .of_finitenessRelation finitenessRelation
 
@@ -301,7 +300,6 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
       | ⟨.operating _ searcher⟩, ⟨.atEnd⟩ => simp [SplitInclusiveIterator.toOption, Option.lt]
       | ⟨.atEnd⟩, _ => simp
 
-@[no_expose]
 instance [Std.Iterators.Finite (σ s) Id] :
     Std.Iterators.Finite (SplitInclusiveIterator pat s) Id :=
   .of_finitenessRelation finitenessRelation
@@ -661,7 +659,6 @@ private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
       | ⟨.operating _ searcher⟩, ⟨.atEnd⟩ => simp [RevSplitIterator.toOption, Option.lt]
       | ⟨.atEnd⟩, _ => simp
 
-@[no_expose]
 instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (RevSplitIterator ρ s) Id :=
   .of_finitenessRelation finitenessRelation
 
diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean
index 8845b1db4f..2814e6b6cc 100644
--- a/src/Init/Data/UInt/Basic.lean
+++ b/src/Init/Data/UInt/Basic.lean
@@ -502,12 +502,12 @@ natural numbers. Usually accessed via the `<` operator.
 -/
 -- These need to be exposed as `Init.Prelude` already has an instance for bootstrapping purposes and
 -- they should be defeq
-@[expose] protected def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
+protected def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
 /--
 Non-strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
 natural numbers. Usually accessed via the `≤` operator.
 -/
-@[expose] protected def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec
+protected def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec
 
 instance : Mul UInt32       := ⟨UInt32.mul⟩
 instance : Pow UInt32 Nat   := ⟨UInt32.pow⟩
diff --git a/src/Init/Grind/ToInt.lean b/src/Init/Grind/ToInt.lean
index 1e131ac7ed..10a343a146 100644
--- a/src/Init/Grind/ToInt.lean
+++ b/src/Init/Grind/ToInt.lean
@@ -47,9 +47,9 @@ inductive IntInterval : Type where
 namespace IntInterval
 
 /-- The interval `[0, 2^n)`. -/
-@[expose] abbrev uint (n : Nat) := IntInterval.co 0 (2 ^ n)
+abbrev uint (n : Nat) := IntInterval.co 0 (2 ^ n)
 /-- The interval `[-2^(n-1), 2^(n-1))`. -/
-@[expose] abbrev sint (n : Nat) := IntInterval.co (-(2 ^ (n - 1))) (2 ^ (n - 1))
+abbrev sint (n : Nat) := IntInterval.co (-(2 ^ (n - 1))) (2 ^ (n - 1))
 
 /-- The lower bound of the interval, if finite. -/
 @[expose] def lo? (i : IntInterval) : Option Int :=
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 06361a426c..9ed192846b 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2346,7 +2346,7 @@ Returns `a` modulo `n` as a `Fin n`.
 
 This function exists for bootstrapping purposes. Use `Fin.ofNat` instead.
 -/
-@[expose] protected def Fin.Internal.ofNat (n : Nat) (hn : LT.lt 0 n) (a : Nat) : Fin n :=
+protected def Fin.Internal.ofNat (n : Nat) (hn : LT.lt 0 n) (a : Nat) : Fin n :=
   ⟨HMod.hMod a n, Nat.mod_lt _ hn⟩
 
 /--
@@ -2388,7 +2388,7 @@ protected def BitVec.ofNatLT {w : Nat} (i : Nat) (p : LT.lt i (hPow 2 w)) : BitV
 /--
 The bitvector with value `i mod 2^n`.
 -/
-@[expose, match_pattern]
+@[match_pattern]
 protected def BitVec.ofNat (n : Nat) (i : Nat) : BitVec n where
   toFin := Fin.Internal.ofNat (HPow.hPow 2 n) (Nat.pow_pos (Nat.zero_lt_succ _)) i
 
@@ -2397,7 +2397,6 @@ Return the underlying `Nat` that represents a bitvector.
 
 This is O(1) because `BitVec` is a (zero-cost) wrapper around a `Nat`.
 -/
-@[expose]
 protected def BitVec.toNat (x : BitVec w) : Nat := x.toFin.val
 
 instance : LT (BitVec w) where lt := (LT.lt ·.toNat ·.toNat)
@@ -2924,7 +2923,7 @@ Examples:
  * `(some "hello").getD "goodbye" = "hello"`
  * `none.getD "goodbye" = "goodbye"`
 -/
-@[macro_inline, expose] def Option.getD (opt : Option α) (dflt : α) : α :=
+@[macro_inline] def Option.getD (opt : Option α) (dflt : α) : α :=
   match opt with
   | some x => x
   | none => dflt
@@ -3215,7 +3214,7 @@ def Array.mkEmpty {α : Type u} (c : @& Nat) : Array α where
 /--
 Constructs a new empty array with initial capacity `c`.
 -/
-@[extern "lean_mk_empty_array_with_capacity", expose]
+@[extern "lean_mk_empty_array_with_capacity"]
 def Array.emptyWithCapacity {α : Type u} (c : @& Nat) : Array α where
   toList := List.nil
 
@@ -3224,7 +3223,7 @@ Constructs a new empty array with initial capacity `0`.
 
 Use `Array.emptyWithCapacity` to create an array with a greater initial capacity.
 -/
-@[expose, inline]
+@[inline]
 def Array.empty {α : Type u} : Array α := emptyWithCapacity 0
 
 /--
@@ -3303,7 +3302,7 @@ Examples:
 * `#[].push "apple" = #["apple"]`
 * `#["apple"].push "orange" = #["apple", "orange"]`
 -/
-@[extern "lean_array_push", expose]
+@[extern "lean_array_push"]
 def Array.push {α : Type u} (a : Array α) (v : α) : Array α where
   toList := List.concat a.toList v
 
@@ -3593,7 +3592,7 @@ instance : Inhabited Substring.Raw where
 /--
 The number of bytes used by the string's UTF-8 encoding.
 -/
-@[inline, expose] def Substring.Raw.bsize : Substring.Raw → Nat
+@[inline] def Substring.Raw.bsize : Substring.Raw → Nat
   | ⟨_, b, e⟩ => e.byteIdx.sub b.byteIdx
 
 /--
diff --git a/src/Lean/Elab/DocString.lean b/src/Lean/Elab/DocString.lean
index 04c4002917..3058b484f5 100644
--- a/src/Lean/Elab/DocString.lean
+++ b/src/Lean/Elab/DocString.lean
@@ -295,7 +295,6 @@ abbrev flag (default : Bool) : Type := Bool
 Gadget that indicates that a function's parameter should be treated as a repeated (and thus
 optional) named argument when used in a docstring extension.
 -/
-@[expose]
 abbrev many (α : Type u) : Type u := Array α
 
 
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 3f6e147999..328d22c799 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -1184,6 +1184,11 @@ register_builtin_option warn.exposeOnPrivate : Bool := {
   descr    := "warn about uses of `@[expose]` on private declarations"
 }
 
+register_builtin_option warn.redundantExpose : Bool := {
+  defValue := true
+  descr    := "warn about redundant `@[expose]`/`@[no_expose]` attributes"
+}
+
 def elabMutualDef (vars : Array Expr) (sc : Command.Scope) (views : Array DefView) : TermElabM Unit :=
   if isExample views then
     withoutModifyingEnv do
@@ -1328,35 +1333,49 @@ where
     applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation
   finishElab headers := withFunLocalDecls headers fun funFVars => do
     let env ← getEnv
-    if warn.exposeOnPrivate.get (← getOptions) then
-      if env.header.isModule && !env.isExporting then
-        for header in headers do
-          for attr in header.modifiers.attrs do
-            if attr.name == `expose then
-              logWarningAt attr.stx m!"Redundant `[expose]` attribute, it is meaningful on public \
-                definitions only"
+    let inExposeSection := sc.attrs.any (· matches `(attrInstance| expose))
+    -- Determine whether each header would be exposed without any explicit `@[expose]`/`@[no_expose]`
+    let wouldBeExposed ← headers.mapM fun header => do
+      if header.kind == .abbrev then return true
+      if header.kind == .instance then
+        if !(← isProp header.type) then return true
+      if header.kind == .def && (!header.modifiers.isMeta || sc.isMeta) && inExposeSection then return true
+      return false
+    let hasExpose (header : DefViewElabHeader) := header.modifiers.attrs.any (·.name == `expose)
+    let hasNoExpose (header : DefViewElabHeader) := header.modifiers.attrs.any (·.name == `no_expose)
+
+    let opts ← getOptions
+    let warnExposeOnPrivate := warn.exposeOnPrivate.get opts
+    let warnRedundantExpose := warn.redundantExpose.get opts
+    for header in headers, exposed in wouldBeExposed do
+      for attr in header.modifiers.attrs do
+        -- skip macro-generated attributes
+        unless attr.stx.getHeadInfo matches .original .. do continue
+        match attr.name with
+        | `expose =>
+          if warnExposeOnPrivate && env.header.isModule && !env.isExporting then
+            logWarningAt attr.stx m!"Redundant `[expose]` attribute, it is meaningful on public \
+              definitions only"
+          if warnRedundantExpose then
+            if !env.header.isModule then
+              logWarningAt attr.stx m!"`@[expose]` has no effect outside a `module` file"
+            else if env.isExporting && exposed then
+              logWarningAt attr.stx m!"`@[expose]` has no effect; this declaration would be exposed by default"
+        | `no_expose =>
+          if warnRedundantExpose then
+            if !env.header.isModule then
+              logWarningAt attr.stx m!"`@[no_expose]` has no effect outside a `module` file"
+            else if env.isExporting && !exposed && !hasExpose header then
+              logWarningAt attr.stx m!"`@[no_expose]` has no effect; this declaration would not \
+                be exposed by default"
+        | _ => pure ()
 
-    -- Switch to private scope if...
     withoutExporting (when :=
-      (← headers.allM (fun header => do
-        -- ... there is a `@[no_expose]` attribute
-        if header.modifiers.attrs.any (·.name == `no_expose) then
-          return true
-        -- ... or NONE of the following:
-        -- ... this is a non-`meta` `def` inside a `@[expose] section`
-        if header.kind == .def && (!header.modifiers.isMeta || sc.isMeta) && sc.attrs.any (· matches `(attrInstance| expose)) then
-          return false
-        -- ... there is an `@[expose]` attribute directly on the def (of any kind or phase)
-        if header.modifiers.attrs.any (·.name == `expose) then
-          return false
-        -- ... this is an `abbrev`
-        if header.kind == .abbrev then
-          return false
-        -- ... this is a data instance
-        if header.kind == .instance then
-          if !(← isProp header.type) then
-            return false
+      (← (headers.zip wouldBeExposed).allM (fun (header, exposed) => do
+        if hasNoExpose header then return true
+        if exposed || hasExpose header then return false
         return true))) do
+
     -- Never export private decls from theorem bodies to make sure they stay irrelevant for rebuilds
     withOptions (fun opts =>
       if headers.any (·.kind.isTheorem) then ResolveName.backward.privateInPublic.set opts false else opts) do
diff --git a/src/Std/Data/DTreeMap/Internal/Zipper.lean b/src/Std/Data/DTreeMap/Internal/Zipper.lean
index dc54fc1adc..6d8471cd1e 100644
--- a/src/Std/Data/DTreeMap/Internal/Zipper.lean
+++ b/src/Std/Data/DTreeMap/Internal/Zipper.lean
@@ -364,7 +364,6 @@ def Zipper.FinitenessRelation : FinitenessRelation (Zipper α β) Id where
           simp only [h2, ← h'.1, Zipper.size_prependMap, Zipper.size, Nat.add_lt_add_iff_right,
             Nat.lt_add_left_iff_pos, Nat.lt_add_one]
 
-@[no_expose]
 public instance Zipper.instFinite : Finite (Zipper α β) Id :=
   .of_finitenessRelation Zipper.FinitenessRelation
 
@@ -477,7 +476,6 @@ def RxcIterator.FinitenessRelation [Ord α] : FinitenessRelation (RxcIterator α
           simp only [h2, ← h'.1, Zipper.size_prependMap, Zipper.size, Nat.add_lt_add_iff_right,
             Nat.lt_add_left_iff_pos, Nat.lt_add_one]
 
-@[no_expose]
 public instance instFinite [Ord α] : Finite (RxcIterator α β) Id :=
   .of_finitenessRelation RxcIterator.FinitenessRelation
 
@@ -606,7 +604,6 @@ def RxoIterator.instFinitenessRelation [Ord α] : FinitenessRelation (RxoIterato
           simp only [h2, ← h'.1, Zipper.size_prependMap, Zipper.size, Nat.add_lt_add_iff_right,
             Nat.lt_add_left_iff_pos, Nat.lt_add_one]
 
-@[no_expose]
 public instance Rxo.instFinite [Ord α] : Finite (RxoIterator α β) Id :=
   .of_finitenessRelation RxoIterator.instFinitenessRelation
 
diff --git a/src/Std/Data/Iterators/Lemmas/Equivalence/HetT.lean b/src/Std/Data/Iterators/Lemmas/Equivalence/HetT.lean
index de2ba5a6b2..5a1d3208dd 100644
--- a/src/Std/Data/Iterators/Lemmas/Equivalence/HetT.lean
+++ b/src/Std/Data/Iterators/Lemmas/Equivalence/HetT.lean
@@ -187,7 +187,7 @@ attribute [-simp] HetT.mk.injEq
 /--
 Converts `PostconditionT m α` to `HetT m α`, preserving the postcondition property.
 -/
-@[expose] noncomputable def HetT.ofPostconditionT [Monad m] (x : PostconditionT m α) : HetT m α :=
+noncomputable def HetT.ofPostconditionT [Monad m] (x : PostconditionT m α) : HetT m α :=
   ⟨x.Property, inferInstance, USquash.deflate <$> x.operation⟩
 
 noncomputable instance (m : Type w → Type w') [Monad m] : MonadLift m (HetT m) where
@@ -198,7 +198,7 @@ Lifts `x : m α` into `HetT m α` with the trivial postcondition.
 
 Caution: This is not a lawful monad lifting function
 -/
-@[expose] noncomputable def HetT.lift {α : Type w} {m : Type w → Type w'} [Monad m] (x : m α) :
+noncomputable def HetT.lift {α : Type w} {m : Type w → Type w'} [Monad m] (x : m α) :
     HetT m α :=
   x
 
@@ -229,7 +229,7 @@ protected noncomputable def HetT.map {m : Type w → Type w'} [Functor m] {α :
 /--
 A generalization of `HetT.bind` that provides the postcondition property to the mapping function.
 -/
-@[expose] protected noncomputable def HetT.pbind {m : Type w → Type w'} [Monad m] {α : Type u} {β : Type v}
+protected noncomputable def HetT.pbind {m : Type w → Type w'} [Monad m] {α : Type u} {β : Type v}
     (x : HetT m α) (f : (a : α) → x.Property a → HetT m β) : HetT m β :=
   have := x.small
   have := fun a h => (f a h).small
@@ -290,7 +290,7 @@ theorem HetT.prun_ofPostconditionT [Monad m] [LawfulMonad m] {x : PostconditionT
 /--
 If the monad `m` is liftable to `n`, lifts `HetT m α` to `HetT n α`.
 -/
-@[expose] noncomputable def HetT.liftInner {m : Type w → Type w'} (n : Type w → Type w'') [MonadLiftT m n]
+noncomputable def HetT.liftInner {m : Type w → Type w'} (n : Type w → Type w'') [MonadLiftT m n]
     (x : HetT m α) : HetT n α :=
   ⟨x.Property, x.small, x.operation⟩
 
diff --git a/src/Std/Http/Internal/Char.lean b/src/Std/Http/Internal/Char.lean
index be48bb1064..c2c9c4dce8 100644
--- a/src/Std/Http/Internal/Char.lean
+++ b/src/Std/Http/Internal/Char.lean
@@ -29,28 +29,28 @@ set_option linter.all true
 /--
 Checks if a character is ASCII (Unicode code point < 128).
 -/
-@[inline, expose]
+@[inline]
 def isAscii (c : Char) : Bool :=
   c.toNat < 128
 
 /--
 Checks if a byte represents an ASCII character (value < 128).
 -/
-@[inline, expose]
+@[inline]
 def isAsciiByte (c : UInt8) : Bool :=
   c < 128
 
 /--
 Checks if a byte is a decimal digit (0-9).
 -/
-@[inline, expose]
+@[inline]
 def isDigitByte (c : UInt8) : Bool :=
   c >= '0'.toUInt8 && c <= '9'.toUInt8
 
 /--
 Checks if a byte is an alphabetic character (a-z or A-Z).
 -/
-@[inline, expose]
+@[inline]
 def isAlphaByte (c : UInt8) : Bool :=
   (c >= 'A'.toUInt8 && c <= 'Z'.toUInt8) || (c >= 'a'.toUInt8 && c <= 'z'.toUInt8)
 
@@ -196,7 +196,7 @@ def reasonPhraseChar (c : Char) : Bool :=
 /--
 Checks if a character is a hexadecimal digit (0-9, a-f, or A-F).
 -/
-@[inline, expose]
+@[inline]
 def isHexDigit (c : Char) : Bool :=
   (c matches 'a' | 'b' | 'c' | 'd' | 'e' | 'f' | 'A' | 'B' | 'C' | 'D' | 'E' | 'F') ||
   Char.isDigit c
@@ -204,7 +204,7 @@ def isHexDigit (c : Char) : Bool :=
 /--
 Checks if a byte is a hexadecimal digit (0-9, a-f, or A-F).
 -/
-@[inline, expose]
+@[inline]
 def isHexDigitByte (c : UInt8) : Bool :=
   (c ≥ '0'.toUInt8 && c ≤ '9'.toUInt8) ||
   (c ≥ 'a'.toUInt8 && c ≤ 'f'.toUInt8) ||
@@ -213,7 +213,7 @@ def isHexDigitByte (c : UInt8) : Bool :=
 /--
 Checks if a byte is an alphanumeric digit (0-9, a-z, or A-Z).
 -/
-@[inline, expose]
+@[inline]
 def isAlphaNum (c : UInt8) : Bool :=
   (c ≥ '0'.toUInt8 && c ≤ '9'.toUInt8) ||
   (c ≥ 'a'.toUInt8 && c ≤ 'z'.toUInt8) ||
@@ -222,7 +222,7 @@ def isAlphaNum (c : UInt8) : Bool :=
 /--
 Checks whether `c` is an ASCII alphanumeric character.
 -/
-@[inline, expose]
+@[inline]
 def isAsciiAlphaNumChar (c : Char) : Bool :=
   isAscii c && (Char.isDigit c || Char.isAlpha c)
 
@@ -230,7 +230,7 @@ def isAsciiAlphaNumChar (c : Char) : Bool :=
 Checks if a character is valid after the first character of a URI scheme.
 Valid characters are ASCII alphanumeric, `+`, `-`, and `.`.
 -/
-@[inline, expose]
+@[inline]
 def isValidSchemeChar (c : Char) : Bool :=
   isAsciiAlphaNumChar c || (c matches '+' | '-' | '.')
 
@@ -238,7 +238,7 @@ def isValidSchemeChar (c : Char) : Bool :=
 Checks if a character is valid for use in a domain name.
 Valid characters are ASCII alphanumeric, hyphens, and dots.
 -/
-@[inline, expose]
+@[inline]
 def isValidDomainNameChar (c : Char) : Bool :=
   isAsciiAlphaNumChar c || (c matches '-' | '.')
 
@@ -246,7 +246,7 @@ def isValidDomainNameChar (c : Char) : Bool :=
 Checks if a byte is an unreserved character according to RFC 3986. Unreserved characters are:
 alphanumeric, hyphen, period, underscore, and tilde.
 -/
-@[inline, expose]
+@[inline]
 def isUnreserved (c : UInt8) : Bool :=
   isAlphaNum c ||
   (c = '-'.toUInt8 || c = '.'.toUInt8 || c = '_'.toUInt8 || c = '~'.toUInt8)
@@ -255,7 +255,7 @@ def isUnreserved (c : UInt8) : Bool :=
 Checks if a byte is a sub-delimiter character according to RFC 3986.
 Sub-delimiters are: `!`, `$`, `&`, `'`, `(`, `)`, `*`, `+`, `,`, `;`, `=`.
 -/
-@[inline, expose]
+@[inline]
 def isSubDelims (c : UInt8) : Bool :=
   c = '!'.toUInt8 || c = '$'.toUInt8 || c = '&'.toUInt8 || c = ('\'' : Char).toUInt8 ||
   c = '('.toUInt8 || c = ')'.toUInt8 || c = '*'.toUInt8 || c = '+'.toUInt8 ||
@@ -268,7 +268,7 @@ Checks if a byte is a valid path character (`pchar`) according to RFC 3986.
 Note: The percent-encoding (`pct-encoded`) is handled separately by `isEncodedChar`,
 so this predicate only covers the non-percent characters.
 -/
-@[inline, expose]
+@[inline]
 def isPChar (c : UInt8) : Bool :=
   isUnreserved c || isSubDelims c || c = ':'.toUInt8 || c = '@'.toUInt8
 
@@ -276,7 +276,7 @@ def isPChar (c : UInt8) : Bool :=
 Checks if a byte is a valid character in a URI query component according to RFC 3986.
 `query = *( pchar / "/" / "?" )`
 -/
-@[inline, expose]
+@[inline]
 def isQueryChar (c : UInt8) : Bool :=
   isPChar c || c = '/'.toUInt8 || c = '?'.toUInt8
 
@@ -284,7 +284,7 @@ def isQueryChar (c : UInt8) : Bool :=
 Checks if a byte is a valid character in a URI fragment component according to RFC 3986.
 `fragment = *( pchar / "/" / "?" )`
 -/
-@[inline, expose]
+@[inline]
 def isFragmentChar (c : UInt8) : Bool :=
   isPChar c || c = '/'.toUInt8 || c = '?'.toUInt8
 
@@ -295,7 +295,7 @@ Checks if a byte is a valid character in a URI userinfo component according to R
 Note: It avoids the pct-encoded of the original grammar because it is used with `Encoding.lean`
 that provides it.
 -/
-@[inline, expose]
+@[inline]
 def isUserInfoChar (c : UInt8) : Bool :=
   isUnreserved c || isSubDelims c || c = ':'.toUInt8
 
@@ -306,7 +306,7 @@ excluding the typical key/value separators `&` and `=`.
 Inspired by `query = *( pchar / "/" / "?" )` from RFC 3986,
 but disallows `&` and `=` so they can be treated as structural separators.
 -/
-@[inline, expose]
+@[inline]
 def isQueryDataChar (c : UInt8) : Bool :=
   isQueryChar c && c ≠ '&'.toUInt8 && c ≠ '='.toUInt8
 
diff --git a/src/Std/Http/Internal/LowerCase.lean b/src/Std/Http/Internal/LowerCase.lean
index c4f89ae258..1a02239148 100644
--- a/src/Std/Http/Internal/LowerCase.lean
+++ b/src/Std/Http/Internal/LowerCase.lean
@@ -30,7 +30,7 @@ set_option linter.all true
 /--
 Predicate asserting that a string is in lowercase form.
 -/
-@[expose] def IsLowerCase (s : String) : Prop :=
+def IsLowerCase (s : String) : Prop :=
   s.toLower = s
 
 private theorem Char.toLower_eq_self_iff {c : Char} : c.toLower = c ↔ c.isUpper = false := by
diff --git a/src/Std/Http/Protocol/H1/Message.lean b/src/Std/Http/Protocol/H1/Message.lean
index a4ea755b21..cbb073c058 100644
--- a/src/Std/Http/Protocol/H1/Message.lean
+++ b/src/Std/Http/Protocol/H1/Message.lean
@@ -44,7 +44,6 @@ deriving BEq
 /--
 Inverts the message direction.
 -/
-@[expose]
 abbrev Direction.swap : Direction → Direction
   | .receiving => .sending
   | .sending => .receiving
diff --git a/src/Std/Time/Internal/Bounded.lean b/src/Std/Time/Internal/Bounded.lean
index 0b7c18a75a..051ad93417 100644
--- a/src/Std/Time/Internal/Bounded.lean
+++ b/src/Std/Time/Internal/Bounded.lean
@@ -24,7 +24,7 @@ set_option linter.all true in
 A `Bounded` is represented by an `Int` that is constrained by a lower and higher bounded using some
 relation `rel`. It includes all the integers that `rel lo val ∧ rel val hi`.
 -/
-@[expose] def Bounded (rel : Int → Int → Prop) (lo : Int) (hi : Int) := { val : Int // rel lo val ∧ rel val hi }
+def Bounded (rel : Int → Int → Prop) (lo : Int) (hi : Int) := { val : Int // rel lo val ∧ rel val hi }
 
 namespace Bounded
 
@@ -103,7 +103,7 @@ namespace LE
 /--
 Convert a `Nat` to a `Bounded.LE` by wrapping it.
 -/
-@[inline, expose]
+@[inline]
 def ofNatWrapping { lo hi : Int } (val : Int) (h : lo ≤ hi) : Bounded.LE lo hi := by
   let range := hi - lo + 1
   have range_pos := Int.add_pos_of_nonneg_of_pos (b := 1) (Int.sub_nonneg_of_le h) (by decide)
@@ -214,7 +214,7 @@ def toInt (n : Bounded.LE lo hi) : Int :=
 /--
 Convert a `Bounded.LE` to a `Fin`.
 -/
-@[inline, simp, expose]
+@[inline, simp]
 def toFin (n : Bounded.LE lo hi) (h₀ : 0 ≤ lo) : Fin (hi + 1).toNat := by
   let h := n.property.right
   let h₁ := Int.le_trans h₀ n.property.left
@@ -284,7 +284,7 @@ def truncate (bounded : Bounded.LE n m) : Bounded.LE 0 (m - n) := by
 Adjust the bounds of a `Bounded` by changing the higher bound if another value `j` satisfies the same
 constraint.
 -/
-@[inline, simp, expose]
+@[inline, simp]
 def truncateTop (bounded : Bounded.LE n m) (h : bounded.val ≤ j) : Bounded.LE n j := by
   refine ⟨bounded.val, And.intro ?_ ?_⟩
   · exact bounded.property.left
@@ -312,7 +312,7 @@ def neg (bounded : Bounded.LE n m) : Bounded.LE (-m) (-n) := by
 /--
 Adjust the bounds of a `Bounded` by adding a constant value to both the lower and upper bounds.
 -/
-@[inline, simp, expose]
+@[inline, simp]
 def add (bounded : Bounded.LE n m) (num : Int) : Bounded.LE (n + num) (m + num) := by
   refine ⟨bounded.val + num, And.intro ?_ ?_⟩
   all_goals apply (Int.add_le_add · (Int.le_refl num))
@@ -331,7 +331,7 @@ def addProven (bounded : Bounded.LE n m) (h₀ : bounded.val + num ≤ m) (h₁
 /--
 Adjust the bounds of a `Bounded` by adding a constant value to the upper bounds.
 -/
-@[inline, expose]
+@[inline]
 def addTop (bounded : Bounded.LE n m) (num : Int) (h : num ≥ 0) : Bounded.LE n (m + num) := by
   refine ⟨bounded.val + num, And.intro ?_ ?_⟩
   · let h := Int.add_le_add bounded.property.left h
@@ -362,7 +362,7 @@ def addBounds (bounded : Bounded.LE n m) (bounded₂ : Bounded.LE i j) : Bounded
 /--
 Adjust the bounds of a `Bounded` by subtracting a constant value to both the lower and upper bounds.
 -/
-@[inline, simp, expose]
+@[inline, simp]
 def sub (bounded : Bounded.LE n m) (num : Int) : Bounded.LE (n - num) (m - num) :=
   add bounded (-num)
 
diff --git a/src/Std/Time/Time/Unit/Second.lean b/src/Std/Time/Time/Unit/Second.lean
index 3ad571d5fb..6f81a7d7a8 100644
--- a/src/Std/Time/Time/Unit/Second.lean
+++ b/src/Std/Time/Time/Unit/Second.lean
@@ -21,7 +21,7 @@ set_option linter.all true
 `Ordinal` represents a bounded value for second, which ranges between 0 and 59 or 60. This accounts
 for potential leap second.
 -/
-@[expose] def Ordinal (leap : Bool) := Bounded.LE 0 (.ofNat (if leap then 60 else 59))
+def Ordinal (leap : Bool) := Bounded.LE 0 (.ofNat (if leap then 60 else 59))
 
 instance : LE (Ordinal leap) where
   le x y := LE.le x.val y.val
@@ -58,7 +58,7 @@ instance : LawfulEqOrd (Ordinal leap) := inferInstanceAs <| LawfulEqOrd (Bounded
 /--
 `Offset` represents an offset in seconds. It is defined as an `Int`.
 -/
-@[expose] def Offset : Type := UnitVal 1
+def Offset : Type := UnitVal 1
 deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
 instance {x y : Offset} : Decidable (x ≤ y) :=
diff --git a/src/lake/Lake/Build/Fetch.lean b/src/lake/Lake/Build/Fetch.lean
index 67b43f10fb..bdd8a40231 100644
--- a/src/lake/Lake/Build/Fetch.lean
+++ b/src/lake/Lake/Build/Fetch.lean
@@ -25,7 +25,7 @@ using the `fetch` function defined in this module.
 namespace Lake
 
 /-- A type alias for `Option Package` that assists monad type class synthesis. -/
-@[expose] public abbrev CurrPackage := Option Package
+public abbrev CurrPackage := Option Package
 
 /-- Run the action `x` with `pkg?` as the current package or no package if `none`. -/
 @[inline] public def withCurrPackage? [MonadWithReader CurrPackage m] (pkg? : Option Package) (x : m α): m α :=
diff --git a/src/lake/Lake/Util/JsonObject.lean b/src/lake/Lake/Util/JsonObject.lean
index 691a010df0..df4ac63fb7 100644
--- a/src/lake/Lake/Util/JsonObject.lean
+++ b/src/lake/Lake/Util/JsonObject.lean
@@ -18,7 +18,7 @@ indexing fields more convenient.
 namespace Lake
 
 /-- A JSON object (`Json.obj` data). -/
-@[expose] public abbrev JsonObject :=
+public abbrev JsonObject :=
   Std.TreeMap.Raw String Json
 
 namespace JsonObject
diff --git a/tests/elab/do_for_loop_compiler_test.lean b/tests/elab/do_for_loop_compiler_test.lean
index 08d4080e54..9f3afa96c7 100644
--- a/tests/elab/do_for_loop_compiler_test.lean
+++ b/tests/elab/do_for_loop_compiler_test.lean
@@ -1,6 +1,6 @@
 import Std.Do.Triple.SpecLemmas
 
-@[specialize, expose]
+@[specialize]
 def List.newForIn (l : List α) (b : β) (kcons : α → (β → γ) → β → γ) (knil : β → γ) : γ :=
   match l with
   | []     => knil b
diff --git a/tests/elab/linterRedundantExpose.lean b/tests/elab/linterRedundantExpose.lean
new file mode 100644
index 0000000000..087cfdd186
--- /dev/null
+++ b/tests/elab/linterRedundantExpose.lean
@@ -0,0 +1,50 @@
+module
+
+/-! `warn.redundantExpose` tests -/
+
+public section
+
+-- `@[expose]` on abbrev should warn
+/-- warning: `@[expose]` has no effect; this declaration would be exposed by default -/
+#guard_msgs in
+@[expose] abbrev myAbbrev := 1
+
+-- `@[expose]` on a regular public def should not warn
+@[expose] def myDef := 1
+
+-- `@[no_expose]` on a regular def outside expose section should warn
+/-- warning: `@[no_expose]` has no effect; this declaration would not be exposed by default -/
+#guard_msgs in
+@[no_expose] def myDef3 := 3
+
+-- `@[expose]` on a data instance should warn
+/-- warning: `@[expose]` has no effect; this declaration would be exposed by default -/
+#guard_msgs in
+@[expose] instance : Inhabited Nat := ⟨0⟩
+
+-- `@[expose]` on a Prop instance should not warn
+@[expose] instance : Nonempty Nat := ⟨0⟩
+
+-- `@[no_expose]` on abbrev should not warn (it overrides auto-expose)
+@[no_expose] abbrev myAbbrev2 := 5
+
+-- `@[no_expose]` on a data instance should not warn (it overrides auto-expose)
+@[no_expose] instance : Inhabited Bool := ⟨false⟩
+
+end
+
+-- `@[expose]` inside `@[expose] section` on a def should warn
+@[expose] public section
+/-- warning: `@[expose]` has no effect; this declaration would be exposed by default -/
+#guard_msgs in
+@[expose] def myDef2 := 2
+
+-- `@[no_expose]` inside `@[expose] section` should not warn (it's meaningful)
+@[no_expose] def myDef4 := 4
+end
+
+-- disabling the linter should suppress warnings
+public section
+set_option warn.redundantExpose false in
+@[expose] abbrev myAbbrev3 := 6
+end