feat: make try? find induction proofs for forall-quantified goals

This PR enables `try?` to find induction-based proofs for goals with leading
foralls (e.g., `∀ n, n ≤ fib n + 1`) by collecting candidates after temporarily
stripping the foralls and generating tactics prefixed with `intro`.

Previously, `try?` could find `fun_induction fib` for `(n : Nat) : n ≤ fib n + 1`
but not for `∀ n, n ≤ fib n + 1` because the candidate collector skipped
expressions with loose bound variables. Rather than modifying the collector,
this change uses `forallTelescope` during tactic generation to collect under
the foralls and wraps the resulting tactics with `intro <names>;`.

For regular induction (not function induction), the code generates tactic syntax
using the intro names directly rather than FVarIds, since the FVarIds from the
temporary forallTelescope context are invalid outside that scope.

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

.claude/CLAUDE.md

@@ -11,6 +11,15 @@ When asked to implement new features:
 
 All new tests should go in `tests/lean/run/`. These tests don't have expected output; we just check there are no errors. You should use `#guard_msgs` to check for specific messages.
 
+## Writing tests for bugs/features
+
+**A test for a bug must FAIL (non-zero exit code) until the bug is fixed.**
+
+- Write the test showing what SHOULD work
+- The test file should fail to compile/run until you implement the fix
+- Do NOT use `#guard_msgs` to capture expected errors - that makes the test pass
+- Do NOT add workarounds - that also makes the test pass
+
 ## Success Criteria
 
 *Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass.

src/Lean/Elab/Tactic/Try.lean

@@ -954,10 +954,105 @@ private def mkAllIndStx (info : Try.Info) (cont : TSyntax `tactic) : MetaM (TSyn
   let tacs ← info.indCandidates.mapM (mkIndStx · cont)
   mkFirstStx tacs
 
+/-! Helpers for forall-quantified goals -/
+
+/-- Wrap a tactic with `intro <names>;` if names is non-empty. -/
+private def wrapWithIntros (names : Array Name) (tac : TSyntax `tactic) : CoreM (TSyntax `tactic) :=
+  if names.isEmpty then
+    return tac
+  else
+    let idents := names.map mkIdent
+    `(tactic| (intro $idents*; $tac))
+
+/-- Result of collecting under foralls: info, intro names, and fvarId-to-name mapping. -/
+structure UnderForallsResult where
+  info : Try.Info
+  introNames : Array Name
+  /-- Maps FVarIds from the temporary context to their user-facing names -/
+  fvarIdToName : Std.HashMap FVarId Name
+
+/-- Collect fun_induction and induction candidates after stripping leading foralls.
+    Returns collection result or none if goal has no leading foralls. -/
+private def collectUnderForalls (goal : MVarId) (config : Try.Config) :
+    MetaM (Option UnderForallsResult) := goal.withContext do
+  let goalType ← goal.getType
+  unless goalType.isForall do return none
+  forallTelescope goalType fun fvars body => do
+    -- Create a temporary mvar with the body type to collect on
+    let tmpMVar ← mkFreshExprMVar body
+    let tmpGoal := tmpMVar.mvarId!
+    let info ← Try.collect tmpGoal config
+    -- Build intro names and fvarId-to-name mapping in one pass
+    let mut introNames : Array Name := #[]
+    let mut fvarIdToName : Std.HashMap FVarId Name := {}
+    for fvar in fvars do
+      let fvarId := fvar.fvarId!
+      let name ← fvarId.getUserName
+      introNames := introNames.push name
+      fvarIdToName := fvarIdToName.insert fvarId name
+    return some { info, introNames, fvarIdToName }
+
+/-- Generate all induction tactics using names instead of FVarIds (for forall case). -/
+private def mkAllIndStxFromNames (info : Try.Info) (fvarIdToName : Std.HashMap FVarId Name)
+    (cont : TSyntax `tactic) : CoreM (TSyntax `tactic) := do
+  let mut tacs : Array (TSyntax `tactic) := #[]
+  for cand in info.indCandidates do
+    if let some name := fvarIdToName[cand.fvarId]? then
+      let ident := mkIdent name
+      tacs := tacs.push (← `(tactic| induction $ident:term <;> $cont))
+  mkFirstStx tacs
+
+/-- Convert an Expr to term syntax, mapping FVars to names from the given map.
+    Returns none if the expr contains FVars not in the map. -/
+private partial def exprToTermSyntaxWithNames (e : Expr) (fvarIdToName : Std.HashMap FVarId Name) :
+    Option (MetaM (TSyntax `term)) :=
+  match e with
+  | .fvar fvarId =>
+    match fvarIdToName[fvarId]? with
+    | some name => some (pure ⟨mkIdent name⟩)
+    | none => none
+  | .const name _ => some do
+    let ident ← toIdent name
+    pure ⟨ident⟩
+  | .app fn arg =>
+    match exprToTermSyntaxWithNames fn fvarIdToName, exprToTermSyntaxWithNames arg fvarIdToName with
+    | some fnStxM, some argStxM => some do
+      let fnStx ← fnStxM
+      let argStx ← argStxM
+      `($fnStx $argStx)
+    | _, _ => none
+  | _ => none  -- Other expr kinds not supported
+
+/-- Generate fun_induction tactic syntax using names (for forall case). -/
+private def mkFunIndStxFromNames (uniques : NameSet) (expr : Expr)
+    (fvarIdToName : Std.HashMap FVarId Name) (cont : TSyntax `tactic) :
+    MetaM (Option (TSyntax `tactic)) := do
+  let fn := expr.getAppFn.constName!
+  if uniques.contains fn then
+    -- If it is unambiguous, use `fun_induction foo` without arguments
+    pure (some (← `(tactic| fun_induction $(← toIdent fn):term <;> $cont)))
+  else
+    -- Need to specify which call - convert expr to syntax using names
+    match exprToTermSyntaxWithNames expr fvarIdToName with
+    | some stxM =>
+      let stx ← stxM
+      pure (some (← `(tactic| fun_induction $stx:term <;> $cont)))
+    | none => pure none
+
+/-- Generate all fun_induction tactics using names instead of FVarIds (for forall case). -/
+private def mkAllFunIndStxFromNames (info : Try.Info) (fvarIdToName : Std.HashMap FVarId Name)
+    (cont : TSyntax `tactic) : MetaM (TSyntax `tactic) := do
+  let uniques := info.funIndCandidates.uniques
+  let mut tacs : Array (TSyntax `tactic) := #[]
+  for call in info.funIndCandidates.calls do
+    if let some tac ← mkFunIndStxFromNames uniques call fvarIdToName cont then
+      tacs := tacs.push tac
+  mkFirstStx tacs
+
 /-! Main code -/
 
 /-- Returns tactic for `evalAndSuggest` (unsafe version that can evaluate user generators) -/
-private unsafe def mkTryEvalSuggestStxUnsafe (goal : MVarId) (info : Try.Info) : MetaM (TSyntax `tactic) := do
+private unsafe def mkTryEvalSuggestStxUnsafe (goal : MVarId) (info : Try.Info) (config : Try.Config) : MetaM (TSyntax `tactic) := do
   let simple ← mkSimpleTacStx
   let simp ← mkSimpStx
   let grind ← mkGrindStx info
@@ -967,6 +1062,23 @@ private unsafe def mkTryEvalSuggestStxUnsafe (goal : MVarId) (info : Try.Info) :
   let atomicOrSuggestions ← `(tactic| first | $atomic:tactic | $atomicSuggestions:tactic)
   let funInds ← mkAllFunIndStx info atomicOrSuggestions
   let inds ← mkAllIndStx info atomicOrSuggestions
+
+  -- Also collect under foralls for induction tactics (only when goal has leading foralls)
+  let underForallsTacs? ← do
+    if let some result ← collectUnderForalls goal config then
+      -- Build atomicOrSuggestions with the info from under foralls (includes equation candidates)
+      let grindUnderForalls ← mkGrindStx result.info
+      let atomicUnderForalls ← `(tactic| attempt_all_par | $simple:tactic | $simp:tactic | $grindUnderForalls:tactic | simp_all)
+      let atomicOrSuggestionsUnderForalls ← `(tactic| first | $atomicUnderForalls:tactic | $atomicSuggestions:tactic)
+      -- Use names instead of FVarIds (FVarIds are invalid outside forallTelescope)
+      let funInds' ← mkAllFunIndStxFromNames result.info result.fvarIdToName atomicOrSuggestionsUnderForalls
+      let inds' ← mkAllIndStxFromNames result.info result.fvarIdToName atomicOrSuggestionsUnderForalls
+      let funIndsWrapped ← wrapWithIntros result.introNames funInds'
+      let indsWrapped ← wrapWithIntros result.introNames inds'
+      pure (some (funIndsWrapped, indsWrapped))
+    else
+      pure none
+
   let extra ← `(tactic| (intros; first | $simple:tactic | $simp:tactic | exact?))
 
   -- Collect user-defined suggestions (runs after built-in tactics)
@@ -984,14 +1096,20 @@ private unsafe def mkTryEvalSuggestStxUnsafe (goal : MVarId) (info : Try.Info) :
       logWarning m!"try_suggestion generator {entry.name} failed: {e.toMessageData}"
 
   -- Build final tactic: built-ins first, then user suggestions as fallback
-  if userTactics.isEmpty then
-    `(tactic| first | $atomic:tactic | $atomicSuggestions:tactic | $funInds:tactic | $inds:tactic | $extra:tactic)
-  else
+  let mut tacs := #[atomic, atomicSuggestions, funInds]
+  if let some (funIndsWithIntro, _) := underForallsTacs? then
+    tacs := tacs.push funIndsWithIntro
+  tacs := tacs.push inds
+  if let some (_, indsWithIntro) := underForallsTacs? then
+    tacs := tacs.push indsWithIntro
+  tacs := tacs.push extra
+  if !userTactics.isEmpty then
     let userAttemptAll ← `(tactic| attempt_all_par $[| $userTactics:tactic]*)
-    `(tactic| first | $atomic:tactic | $atomicSuggestions:tactic | $funInds:tactic | $inds:tactic | $extra:tactic | $userAttemptAll:tactic)
+    tacs := tacs.push userAttemptAll
+  mkFirstStx tacs
 
 @[implemented_by mkTryEvalSuggestStxUnsafe]
-private opaque mkTryEvalSuggestStx (goal : MVarId) (info : Try.Info) : MetaM (TSyntax `tactic)
+private opaque mkTryEvalSuggestStx (goal : MVarId) (info : Try.Info) (config : Try.Config) : MetaM (TSyntax `tactic)
 
 /-- Wraps a tactic suggestion as a term suggestion by prefixing with `by `. -/
 private def wrapSuggestionWithBy (sugg : Tactic.TryThis.Suggestion) : TacticM Tactic.TryThis.Suggestion := do
@@ -1028,7 +1146,7 @@ private def evalAndSuggestWithBy (tk : Syntax) (tac : TSyntax `tactic) (original
     withUnlimitedHeartbeats do
       let goal ← getMainGoal
       let info ← Try.collect goal config
-      let stx ← mkTryEvalSuggestStx goal info
+      let stx ← mkTryEvalSuggestStx goal info config
       if config.wrapWithBy then
         evalAndSuggestWithBy tk stx originalMaxHeartbeats config
       else

tests/lean/run/try_forall_induction.lean

@@ -0,0 +1,42 @@
+/-!
+# Tests for `try?` with forall-quantified goals
+
+When the goal has leading foralls, `try?` should still find induction-based proofs
+by collecting candidates from under the forall binders.
+
+These examples require function induction to solve. With n in context, try?
+finds `fun_induction fib/double`. With ∀ n, try? should also find the proof
+(by doing intro first, then function induction).
+-/
+
+-- A recursive function where proofs require function induction
+def fib : Nat → Nat
+  | 0 => 0
+  | 1 => 1
+  | n + 2 => fib n + fib (n + 1)
+
+-- Another simple recursive function
+def double : Nat → Nat
+  | 0 => 0
+  | n + 1 => double n + 2
+
+/-! ## Baseline tests: n in context (these already work) -/
+
+example (n : Nat) : n ≤ fib n + 1 := by try?
+example (n : Nat) : double n = 2 * n := by try?
+
+/-! ## Forall tests: these should also work (after intro + function induction) -/
+
+example : ∀ n, n ≤ fib n + 1 := by try?
+example : ∀ n, double n = 2 * n := by try?
+
+/-! ## Multiple function induction candidates under forall -/
+
+-- When there are multiple calls to the same function, fun_induction needs to specify which call
+example : ∀ n m, fib n + fib m = fib m + fib n := by try?
+
+/-! ## Regular induction under forall (not just function induction) -/
+
+inductive MyNat where | zero | succ : MyNat → MyNat
+
+example : ∀ n : MyNat, n = MyNat.zero ∨ ∃ m, n = MyNat.succ m := by try?