merge

Adds `atomicWithSuggestions` to `try?` that attempts `grind? +suggestions`
and `simp_all? +suggestions` in parallel using `attempt_all`.

The implementation ensures that only resolved forms like `grind only [X]`
and `simp_all only [X]` appear in the output, not intermediate forms with
`+suggestions`.

Key changes:
- Added `configHasSuggestions` helper to detect `+suggestions` modifier
- Added `mkAtomicWithSuggestionsStx` to create the suggestion tactics
- Modified `mkTryEvalSuggestStx` to include `atomicWithSuggestions` after
  regular atomic tactics
- Updated `evalSuggestGrindTrace` to output only resolved forms when
  `+suggestions` is present
- Implemented `evalSuggestSimpAllTrace` to handle library suggestions for
  `simp_all?` similar to how `SimpTrace.lean` handles them

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>

src/Lean/Elab/Tactic/Try.lean

@@ -739,6 +739,28 @@ private def mkAllFunIndStx (info : Try.Info) (cont : TSyntax `tactic) : MetaM (T
   let tacs ← info.funIndCandidates.calls.mapM (mkFunIndStx uniques · cont)
   mkFirstStx tacs
 
+/-! Vanilla induction generators -/
+
+open Try.Collector in
+private def mkIndStx (cand : InductionCandidate) (cont : TSyntax `tactic) :
+    MetaM (TSyntax `tactic) := do
+  let fvar := mkFVar cand.fvarId
+  let isAccessible ← isExprAccessible fvar
+  withExposedNames do
+    let stx ← PrettyPrinter.delab fvar
+    let tac₁ ← `(tactic| induction $stx:term <;> $cont)
+    -- if fvar has no inaccessible names, use as is
+    if isAccessible then
+      pure tac₁
+    else
+      -- if it has inaccessible names, still try without, in case they are all implicit
+      let tac₂ ← `(tactic| (expose_names; $tac₁))
+      mkFirstStx #[tac₁, tac₂]
+
+private def mkAllIndStx (info : Try.Info) (cont : TSyntax `tactic) : MetaM (TSyntax `tactic) := do
+  let tacs ← info.indCandidates.mapM (mkIndStx · cont)
+  mkFirstStx tacs
+
 /-! Main code -/
 
 /-- Returns tactic for `evalAndSuggest` -/
@@ -749,10 +771,10 @@ private def mkTryEvalSuggestStx (info : Try.Info) : MetaM (TSyntax `tactic) := d
   let atomic ← `(tactic| attempt_all | $simple:tactic | $simp:tactic | $grind:tactic | simp_all)
   let atomicSuggestions ← mkAtomicWithSuggestionsStx
   let funInds ← mkAllFunIndStx info atomic
+  let inds ← mkAllIndStx info atomic
   let extra ← `(tactic| (intros; first | $simple:tactic | $simp:tactic | exact?))
-  `(tactic| first | $atomic:tactic | $atomicSuggestions:tactic | $funInds:tactic | $extra:tactic)
+  `(tactic| first | $atomic:tactic | $atomicSuggestions:tactic | $funInds:tactic | $inds:tactic | $extra:tactic)
 
--- TODO: vanilla `induction`.
 -- TODO: make it extensible.
 
 @[builtin_tactic Lean.Parser.Tactic.tryTrace] def evalTryTrace : Tactic := fun stx => do

src/Lean/Meta/Tactic/Try/Collect.lean

@@ -123,7 +123,9 @@ def visitApp (e : Expr) (declName : Name) (args : Array Expr) : M Unit := do
   saveLibSearchCandidates e
 
 def checkInductive (localDecl : LocalDecl) : M Unit := do
-  let .const declName _ ← whnfD localDecl.type | return ()
+  let type ← whnfD localDecl.type
+  -- Use getAppFn to handle both `T` and `T α β ...` cases
+  let .const declName _ := type.getAppFn | return ()
   let .inductInfo val ← getConstInfo declName | return ()
   if (← isEligible declName) then
     unless (← Grind.isSplit declName) do

tests/lean/run/try_induction.lean

@@ -0,0 +1,126 @@
+/-
+Tests for `try?` suggesting `induction` tactic.
+
+NOTE: Tests using Nat or List from the standard library don't work because
+induction candidates are filtered by `isEligible` in Try/Collect.lean, which
+only accepts types defined in the current module and/or namespace.
+This is why we use custom inductive types below.
+
+Real working examples from the library (like grind_hyper_ex.lean) use:
+  `induction k with grind`
+to prove things like `hyperoperation 1 m k = m + k`. However, `try?` won't
+suggest these because `k : Nat`.
+-/
+
+-- Simple list-like structure
+inductive MyList (α : Type _) where
+  | nil : MyList α
+  | cons : α → MyList α → MyList α
+
+axiom MyListProp : MyList α → Prop
+
+@[grind .] axiom mylist_nil : MyListProp (MyList.nil : MyList α)
+@[grind .] axiom mylist_cons : ∀ (x : α) (xs : MyList α), MyListProp xs → MyListProp (MyList.cons x xs)
+
+/--
+info: Try these:
+  [apply] (induction xs) <;> grind
+  [apply] (induction xs) <;> grind only [mylist_nil, mylist_cons]
+-/
+#guard_msgs (info) in
+example (xs : MyList α) : MyListProp xs := by
+  try?
+
+-- Expression tree
+inductive Expr where
+  | const : Nat → Expr
+  | add : Expr → Expr → Expr
+  | mul : Expr → Expr → Expr
+
+axiom ExprProp : Expr → Prop
+
+@[grind .] axiom expr_const : ∀ n, ExprProp (Expr.const n)
+@[grind .] axiom expr_add : ∀ e1 e2, ExprProp e1 → ExprProp e2 → ExprProp (Expr.add e1 e2)
+@[grind .] axiom expr_mul : ∀ e1 e2, ExprProp e1 → ExprProp e2 → ExprProp (Expr.mul e1 e2)
+
+/--
+info: Try these:
+  [apply] (induction e) <;> grind
+  [apply] (induction e) <;> grind only [expr_const, expr_add, expr_mul]
+-/
+#guard_msgs (info) in
+example (e : Expr) : ExprProp e := by
+  try?
+
+-- For now, `try?` will not do induction on `Nat`, so we use a custom Nat-like type.
+
+inductive MyNat where
+  | zero : MyNat
+  | succ : MyNat → MyNat
+
+abbrev ℕ := MyNat
+
+def add : MyNat → MyNat → MyNat
+  | .zero, n => n
+  | .succ m, n => .succ (add m n)
+
+/--
+info: Try these:
+  [apply] (induction n) <;> grind [= add]
+  [apply] (induction n) <;> grind only [add]
+-/
+#guard_msgs in
+@[grind =]
+theorem add_zero (n : ℕ) : add n .zero = n := by
+  try?
+
+/--
+info: Try these:
+  [apply] (fun_induction add) <;> grind [= add]
+  [apply] (fun_induction add) <;> grind only [add]
+-/
+#guard_msgs in
+@[grind =]
+theorem add_succ (m n : ℕ) : add m (.succ n) = .succ (add m n) := by
+  try?
+
+def hyperoperation : ℕ → ℕ → ℕ → ℕ
+  | .zero, _, k => .succ k
+  | .succ .zero, m, .zero => m
+  | .succ (.succ .zero), _, .zero => .zero
+  | .succ (.succ (.succ _)), _, .zero => .succ .zero
+  | .succ n, m, .succ k => hyperoperation n m (hyperoperation (.succ n) m k)
+
+attribute [local grind] hyperoperation add
+
+/--
+info: Try these:
+  [apply] grind
+  [apply] grind only [hyperoperation]
+-/
+#guard_msgs in
+@[grind =]
+theorem hyperoperation_zero (m k : ℕ) : hyperoperation .zero m k = .succ k := by
+  try?
+
+/--
+info: Try these:
+  [apply] grind
+  [apply] grind only [hyperoperation]
+-/
+#guard_msgs in
+@[grind =]
+theorem hyperoperation_recursion (n m k : ℕ) :
+    hyperoperation (.succ n) m (.succ k) = hyperoperation n m (hyperoperation (.succ n) m k) := by
+  try?
+
+/--
+info: Try these:
+  [apply] (induction k) <;> grind
+  [apply] (induction k) <;>
+    grind only [hyperoperation, = add_zero, = hyperoperation_zero, = hyperoperation_recursion, = add_succ]
+-/
+#guard_msgs in
+@[grind =]
+theorem hyperoperation_one (m k : ℕ) : hyperoperation (.succ .zero) m k = add m k := by
+  try?