lean_multi_attempt
Test multiple tactics in Lean theorem prover without modifying files. Returns goal state results for each tactic to help identify effective proof strategies.
Instructions
Try multiple tactics without modifying file. Returns goal state for each.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | Absolute path to Lean file | |
| line | Yes | Line number (1-indexed) | |
| snippets | Yes | Tactics to try (3+ recommended) |