lean_goal
Retrieve proof goals at specific positions in Lean files to track how tactics transform the state and verify proof completion.
Instructions
Get proof goals at a position. MOST IMPORTANT tool - use often!
Omit column to see goals_before (line start) and goals_after (line end),
showing how the tactic transforms the state. "no goals" = proof complete.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | Absolute path to Lean file | |
| line | Yes | Line number (1-indexed) | |
| column | No | Column (1-indexed). Omit for before/after |