`autoTry.onSorry` suggests using the current theorem to solve the goal

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Setting the option autoTry.onSorry to true makes sorries suggest using the theorem they're in to solve itself.

Context

#lean4 > autoTry suggests recursion

Steps to Reproduce

set_option autoTry.onSorry true

/--
warning: declaration uses `sorry`
---
info: Try this:
  [apply] exact _root_.foo1
-/
#guard_msgs in
theorem foo1 : False := by
  sorry

/--
warning: declaration uses `sorry`
---
info: Try this:
  [apply] exact _root_.foo2 a b
-/
#guard_msgs in
theorem foo2 (a b : Nat) : a = b := by
  sorry

Expected behavior: The first sorry should suggest impossible by simp as would happen if we replace the sorry with try?, and the second sorry should not output anything as try? in its place says Tactic `try?` failed.

Actual behavior: As the #guard_msgs show, autoTry.onSorry always suggests using the current theorem to solve itself. Applying the Try this suggestions produces an Unknown identifier error. Removing the _root_ changes the error to fail to show termination.

Versions

Lean 4.35.0-nightly-2026-08-14
Target: x86_64-unknown-linux-gnu Linux

Additional Information

N/A

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Run the supplied minimal reproducer with autoTry.onSorry enabled and compare its output with replacing each sorry by try?. Trace the autoTry.onSorry and try? entry points to see why the current theorem is included in suggestions. Done means the first case suggests impossible by simp, while the second produces no misleading self-application suggestion.