From d47b474e41e4b134239ef70fa3c15778cc771bcf Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Mon, 10 Nov 2025 15:24:06 +1100
Subject: [PATCH] feat: suggestions don't included deprecated theorems (#11125)

This PR adds a filter for premise selectors to ensure deprecated
theorems are not returned.
---
 src/Lean/LibrarySuggestions/Basic.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Lean/LibrarySuggestions/Basic.lean b/src/Lean/LibrarySuggestions/Basic.lean
index 5bb3f3ce1e..6080e520d5 100644
--- a/src/Lean/LibrarySuggestions/Basic.lean
+++ b/src/Lean/LibrarySuggestions/Basic.lean
@@ -9,6 +9,7 @@ prelude
 public import Lean.Elab.Command
 public import Lean.Meta.Eval
 public import Lean.Meta.CompletionName
+public import Lean.Linter.Deprecated
 public import Init.Data.Random
 
 /-!
@@ -299,6 +300,7 @@ def isDeniedPremise (env : Environment) (name : Name) : Bool := Id.run do
   if name == ``sorryAx then return true
   if name.isInternalDetail then return true
   if Lean.Meta.isInstanceCore env name then return true
+  if Lean.Linter.isDeprecated env name then return false
   if (nameDenyListExt.getState env).any (fun p => name.anyS (· == p)) then return true
   if let some moduleIdx := env.getModuleIdxFor? name then
     let moduleName := env.header.moduleNames[moduleIdx.toNat]!