fix: don't suggest deprecated theorems (#11146)

This PR fixes a bug in #11125. Added a test this time ...

<!-- CURSOR_SUMMARY -->
---

> [!NOTE]
> Exclude deprecated declarations from library suggestions and add a
test verifying they are filtered out.
> 
> - **Library Suggestions**:
> - Update `isDeniedPremise` in `src/Lean/LibrarySuggestions/Basic.lean`
to treat `Lean.Linter.isDeprecated` as denied (`true`), filtering
deprecated constants from suggestions.
> - **Tests**:
> - Add `tests/lean/run/library_suggestions_deprecated.lean` to verify
deprecated theorems (e.g., `deprecatedTheorem`) are not suggested by
`currentFile`, while non-deprecated ones are.
> 
> <sup>Written by [Cursor
Bugbot](https://cursor.com/dashboard?tab=bugbot) for commit
ef7e546dbcca1893d68b07ed79e592ff97f2ceb4. This will update automatically
on new commits. Configure
[here](https://cursor.com/dashboard?tab=bugbot).</sup>
<!-- /CURSOR_SUMMARY -->

src/Lean/LibrarySuggestions/Basic.lean

@@ -300,7 +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 Lean.Linter.isDeprecated env name then return true
   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]!

tests/lean/run/library_suggestions_deprecated.lean

@@ -0,0 +1,26 @@
+import Lean.LibrarySuggestions.Basic
+
+-- Define a normal theorem that should appear in suggestions
+theorem normalTheorem : True := trivial
+
+-- Define a deprecated theorem that should be filtered out by isDeniedPremise
+@[deprecated "Use normalTheorem instead" (since := "1970-01-01")]
+theorem deprecatedTheorem : True := trivial
+
+-- Another normal theorem to verify filtering is selective
+theorem anotherNormalTheorem : 1 + 1 = 2 := rfl
+
+-- Test the currentFile selector which uses isDeniedPremise to filter
+set_library_suggestions Lean.LibrarySuggestions.currentFile
+
+-- This test verifies that deprecated theorems are filtered out by isDeniedPremise
+-- Expected: deprecatedTheorem should NOT appear in suggestions
+/--
+info: Library suggestions:
+  anotherNormalTheorem
+  normalTheorem
+-/
+#guard_msgs in
+example : True := by
+  suggestions
+  trivial