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

[kim-em]

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>;.

Example:

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

-- Previously worked:
example (n : Nat) : n ≤ fib n + 1 := by try?

-- Now also works:
example : ∀ n, n ≤ fib n + 1 := by try?
-- Suggests: intro n; fun_induction fib <;> grind [= fib]

🤖 Prepared with Claude Code and OpenAI Codex