diff --git a/src/Lean/Meta/Tactic/LibrarySearch.lean b/src/Lean/Meta/Tactic/LibrarySearch.lean
index c94f715b57..888cba27dd 100644
--- a/src/Lean/Meta/Tactic/LibrarySearch.lean
+++ b/src/Lean/Meta/Tactic/LibrarySearch.lean
@@ -13,6 +13,7 @@ public import Lean.Util.Heartbeats
 import Init.Grind.Util
 import Init.Try
 import Lean.Elab.Tactic.Basic
+import Lean.Linter.Deprecated
 
 public section
 
@@ -138,7 +139,9 @@ to find candidate lemmas.
 open LazyDiscrTree (InitEntry findMatches)
 
 private def addImport (name : Name) (constInfo : ConstantInfo) :
-    MetaM (Array (InitEntry (Name × DeclMod))) :=
+    MetaM (Array (InitEntry (Name × DeclMod))) := do
+  -- Don't report deprecated lemmas.
+  if Linter.isDeprecated (← getEnv) name then return #[]
   -- Don't report lemmas from metaprogramming namespaces.
   if name.isMetaprogramming then return #[] else
   forallTelescope constInfo.type fun _ type => do
diff --git a/src/Lean/Meta/Tactic/Rewrites.lean b/src/Lean/Meta/Tactic/Rewrites.lean
index 27f10b38ec..7822facacb 100644
--- a/src/Lean/Meta/Tactic/Rewrites.lean
+++ b/src/Lean/Meta/Tactic/Rewrites.lean
@@ -13,6 +13,7 @@ public import Lean.Meta.Tactic.Refl
 public import Lean.Meta.Tactic.SolveByElim
 public import Lean.Meta.Tactic.TryThis
 public import Lean.Util.Heartbeats
+import Lean.Linter.Deprecated
 
 public section
 
@@ -47,6 +48,8 @@ private def addImport (name : Name) (constInfo : ConstantInfo) :
     MetaM (Array (InitEntry (Name × RwDirection))) := do
   if constInfo.isUnsafe then return #[]
   if !allowCompletion (←getEnv) name then return #[]
+  -- Don't report deprecated lemmas.
+  if Linter.isDeprecated (← getEnv) name then return #[]
   -- We now remove some injectivity lemmas which are not useful to rewrite by.
   match name with
   | .str _ n => if n = "injEq" ∨ n = "sizeOf_spec" ∨ n.endsWith "_inj" ∨ n.endsWith "_inj'" then return #[]
diff --git a/tests/lean/run/exact_rw_deprecated.lean b/tests/lean/run/exact_rw_deprecated.lean
new file mode 100644
index 0000000000..6b38c18cd7
--- /dev/null
+++ b/tests/lean/run/exact_rw_deprecated.lean
@@ -0,0 +1,38 @@
+/-!
+# Test that `exact?` and `rw?` do not suggest deprecated lemmas
+-/
+
+-- Create a deprecated lemma and its non-deprecated replacement
+@[deprecated "use myLemma2" (since := "2025-01-01")]
+theorem myLemma1 : True := trivial
+
+theorem myLemma2 : True := trivial
+
+-- Test that exact? suggests myLemma2, not the deprecated myLemma1
+/--
+info: Try this:
+  [apply] exact myLemma2
+-/
+#guard_msgs in
+example : True := by exact?
+
+-- Create a unique type so our lemmas are the only matches
+structure MyType where
+  val : Nat
+
+def myFn (x : MyType) : MyType := x
+
+-- Create deprecated and non-deprecated rewrite lemmas with unique signature
+@[deprecated "use myRwLemma2" (since := "2025-01-01")]
+theorem myRwLemma1 (x : MyType) : myFn (myFn x) = myFn x := rfl
+
+theorem myRwLemma2 (x : MyType) : myFn (myFn x) = myFn x := rfl
+
+-- Test that rw? suggests myRwLemma2, not the deprecated myRwLemma1
+/--
+info: Try this:
+  [apply] rw [myRwLemma2]
+  -- no goals
+-/
+#guard_msgs in
+example (x : MyType) : myFn (myFn x) = myFn x := by rw?