fix: allow exact? to suggest local private declarations (#11736)

This PR fixes an issue where `exact?` would not suggest private
declarations defined in the current module.

## Problem

When using `exact?` in a file with private declarations, those private
declarations were not being suggested even though they are valid and
accessible:

```lean
module

axiom P : Prop
private axiom p : P
example : P := by exact? -- error: could not find lemma
```

The problem was that `blacklistInsertion` in `LazyDiscrTree` was
filtering out all declarations whose names matched `isInternalDetail`,
which includes private names due to their `_private.Module.0.name`
structure.

## Solution

The fix adds a helper function `isPrivateNameOf` that checks if a
private declaration belongs to a specific module. The
`blacklistInsertion` function now allows private declarations belonging
to the current module (`env.header.mainModule`) to pass through the
filter.

Private declarations from imported modules are still filtered out, as
they may reference internal declarations that aren't accessible (which
would cause processing errors).

Zulip discussion:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/.60exact.3F.60.20and.20private.20declarations/near/564586152

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude <noreply@anthropic.com>

src/Lean/Meta/LazyDiscrTree.lean

@@ -802,10 +802,17 @@ structure Cache where
 
 def Cache.empty (ngen : NameGenerator) : Cache := { ngen := ngen, core := {}, «meta» := {} }
 
+/-- Check if a private name belongs to the given module -/
+private def isPrivateNameOf (declName : Name) (mainModule : Name) : Bool :=
+  if let some pfx := privatePrefix? declName then
+    pfx == Name.mkNum (privateHeader ++ mainModule) 0
+  else
+    false
+
 def blacklistInsertion (env : Environment) (declName : Name) : Bool :=
   !allowCompletion env declName
   || declName == ``sorryAx
-  || declName.isInternalDetail
+  || (declName.isInternalDetail && !isPrivateNameOf declName env.header.mainModule)
   || (declName matches .str _ "inj")
   || (declName matches .str _ "noConfusionType")
 

tests/lean/run/exact_private.lean

@@ -0,0 +1,18 @@
+module
+
+/-!
+# Tests for `exact?` with private declarations
+
+This tests that `exact?` can suggest private theorems defined locally in the same module.
+-/
+
+-- Test that exact? suggests private declarations
+axiom P : Prop
+private axiom p : P
+
+/--
+info: Try this:
+  [apply] exact p
+-/
+#guard_msgs in
+example : P := by exact?

tests/lean/run/try_parallelism.lean

@@ -16,9 +16,11 @@ public meta import Lean.Elab.Tactic.Try
 
 open Lean Meta Elab Tactic Try
 
--- An opaque goal that built-in tactics (including solve_by_elim) won't solve
+-- An opaque goal that built-in tactics (including solve_by_elim) won't solve.
+-- The axiom name starts with `_` so that `exact?` treats it as an implementation detail and
+-- won't suggest it directly, allowing us to test parallelism of user-defined suggestion generators.
 opaque ParallelTestGoal : Prop
-axiom parallelTestGoalHolds : ParallelTestGoal
+axiom _parallelTestGoalHolds : ParallelTestGoal
 
 -- Magic seed value to signal parallelism
 meta def magicSeed : Nat := 314159265
@@ -29,14 +31,14 @@ elab "wait_and_check_seed" : tactic => do
   let gen ← IO.stdGenRef.get
   let expected := mkStdGen magicSeed
   if gen.s1 == expected.s1 && gen.s2 == expected.s2 then
-    evalTactic (← `(tactic| exact parallelTestGoalHolds))
+    evalTactic (← `(tactic| exact _parallelTestGoalHolds))
   else
     throwError "seed not changed (sequential execution detected)"
 
 -- Tactic that immediately sets seed and succeeds
 elab "set_seed_and_succeed" : tactic => do
   IO.setRandSeed magicSeed
-  evalTactic (← `(tactic| exact parallelTestGoalHolds))
+  evalTactic (← `(tactic| exact _parallelTestGoalHolds))
 
 -- Register both tactics as user suggestions
 -- High priority tactic: reset seed first (to ensure clean state), then return waiting tactic
@@ -53,9 +55,6 @@ meta def setFlagSolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSynt
 
 -- If parallel: both tactics succeed (tactic 1 sees seed change after waiting)
 -- If sequential: only tactic 2 succeeds (tactic 1 sees unchanged seed)
---
--- EXPECTED ON MASTER (sequential): Only one suggestion
--- EXPECTED ON try_par (parallel): Two suggestions
 /--
 info: Try these:
   [apply] wait_and_check_seed

tests/lean/run/try_user_suggestions.lean

@@ -7,21 +7,23 @@ public meta import Lean.Elab.Tactic.Try
 
 open Lean Meta Elab Tactic Try
 
--- Define an opaque predicate that built-in tactics (including solve_by_elim) won't solve
+-- Define an opaque predicate that built-in tactics (including solve_by_elim) won't solve.
+-- The axiom name starts with `_` so that `exact?` treats it as an implementation detail and
+-- won't suggest it directly, allowing us to test user-defined suggestion generators.
 opaque CustomProp : Prop
-axiom customPropHolds : CustomProp
+axiom _customPropHolds : CustomProp
 
 section BasicTest
 -- Define a generator that suggests the custom lemma
 @[local try_suggestion]
 meta def customPropSolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
-  return #[← `(tactic| exact customPropHolds)]
+  return #[← `(tactic| exact _customPropHolds)]
 
 -- Test that try? picks up the user-defined suggestion
 -- Built-in tactics won't solve this, so only user suggestion appears
 /--
 info: Try this:
-  [apply] exact customPropHolds✝
+  [apply] exact _customPropHolds✝
 -/
 #guard_msgs in
 example : CustomProp := by
@@ -32,11 +34,11 @@ section PriorityTest
 -- Test priority ordering with multiple generators
 @[local try_suggestion 2000]
 meta def highPrioritySolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
-  return #[← `(tactic| apply customPropHolds)]
+  return #[← `(tactic| apply _customPropHolds)]
 
 @[local try_suggestion 1000]
 meta def midPrioritySolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
-  return #[← `(tactic| exact customPropHolds)]
+  return #[← `(tactic| exact _customPropHolds)]
 
 @[local try_suggestion 500]
 meta def lowPrioritySolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
@@ -46,8 +48,8 @@ meta def lowPrioritySolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (T
 -- Note: constructor doesn't work on opaque types, so lowPrioritySolver's suggestion is filtered out
 /--
 info: Try these:
-  [apply] apply customPropHolds✝
-  [apply] exact customPropHolds✝
+  [apply] apply _customPropHolds✝
+  [apply] exact _customPropHolds✝
 -/
 #guard_msgs in
 example : CustomProp := by
@@ -82,15 +84,15 @@ section DoubleSuggestion
 -- Use CustomProp which built-ins can't solve
 @[local try_suggestion]
 meta def doubleSuggestionSolver (_goal : MVarId) (_info : Try.Info) : MetaM (Array (TSyntax `tactic)) := do
-  return #[← `(tactic| show_term apply customPropHolds)]
+  return #[← `(tactic| show_term apply _customPropHolds)]
 
 -- Double-suggestion: when show_term produces a "Try this" message,
 -- both the original tactic and the extracted suggestion should appear
 -- The message from show_term during extraction is suppressed
 /--
 info: Try these:
-  [apply] show_term apply customPropHolds✝
-  [apply] exact customPropHolds
+  [apply] show_term apply _customPropHolds✝
+  [apply] exact _customPropHolds
 -/
 #guard_msgs in
 example : CustomProp := by
@@ -99,23 +101,23 @@ end DoubleSuggestion
 
 section RegisterCommand
 -- Test the register_try?_tactic convenience command
-register_try?_tactic (priority := 500) exact customPropHolds
+register_try?_tactic (priority := 500) exact _customPropHolds
 
 /--
 info: Try this:
-  [apply] exact customPropHolds
+  [apply] exact _customPropHolds
 -/
 #guard_msgs in
 example : CustomProp := by
   try?
 
 -- Test without explicit priority (should default to 1000, so appear before exact at 500)
-register_try?_tactic apply customPropHolds
+register_try?_tactic apply _customPropHolds
 
 /--
 info: Try these:
-  [apply] apply customPropHolds
-  [apply] exact customPropHolds
+  [apply] apply _customPropHolds
+  [apply] exact _customPropHolds
 -/
 #guard_msgs in
 example : CustomProp := by