From 975a81cdb80e9fdc4ff33f4b7e1bae459e45b5a0 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Thu, 8 Jan 2026 10:45:04 +1100
Subject: [PATCH] feat: filter out deprecated lemmas from suggestions in
 `exact?`/`rw?` (#11918)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR filters deprecated lemmas from `exact?` and `rw?` suggestions.

Previously, both tactics would suggest deprecated lemmas, which could be
confusing for users since using the suggestion would trigger a
deprecation warning.

Now, lemmas marked with `@[deprecated]` are filtered out in the
`addImport` functions that populate the discrimination trees used by
these tactics.

**Example (before this PR):**
```lean
import Mathlib.Logic.Basic

example (h : ∃ n : Nat, n > 0) : True := by
  choose (n : Nat) (hn : n > 0 + 0) using h
  guard_hyp hn : n > 0  -- `rw?` would suggest `Eq.rec_eq_cast` which is deprecated
```

Zulip discussion:
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/deprecated.20lemma.20from.20rw.3F/near/554106870

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
---
 src/Lean/Meta/Tactic/LibrarySearch.lean |  5 +++-
 src/Lean/Meta/Tactic/Rewrites.lean      |  3 ++
 tests/lean/run/exact_rw_deprecated.lean | 38 +++++++++++++++++++++++++
 3 files changed, 45 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/exact_rw_deprecated.lean

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?