Auto-try?

After a command is elaborated, walk its info trees and run try? at positions of interest -- empty by blocks, terminal tactics that left goals unsolved, and sorry tactics -- to surface suggestions for completing the proof. Each trigger is gated by its own option: autoTry.onEmptyProof, autoTry.onUnsolvedGoal, autoTry.onSorry. The infotree walk is attached to the linter hook (addLinter), but the feature is not a "linter" in the user- facing sense; it just borrows that hook to find a convenient post-elaboration entry point.

Two heuristics decide when not to fire:

1. Tactic positions that were elaborated against more than one proof state are skipped: a single "Try this" suggestion can't replay against multiple goals. This catches the rhs of <;> (run once per subgoal via the focus / all_goals expansion), repeat/repeat', iterate, and similar.

2. The whole hook stays silent on commands that logged any error other than an "unsolved goals" error. If the user is in the middle of fixing a broken proof we don't want to distract them with suggestions.