lean_goal
Read-onlyIdempotent
Inspect proof goals at a line position in Lean files. Shows the state before and after a tactic, indicating proof completeness or ongoing elaboration.
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. status='complete' means the
proof is finished at this point; status='no_goal_at_position' means the
position carries no proof state (e.g. outside a proof).
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| line | Yes | Line number (1-indexed) | |
| column | No | Column (1-indexed). Omit for before/after | |
| format | No | Output format: 'text' (default) or 'structured' | text |
| file_path | Yes | Absolute or project-root-relative path to Lean file | |
| timeout_s | No | Max seconds to wait for elaboration. On timeout returns status='still_elaborating' - poll again. |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| goals | No | Goal list at specified column position | |
| status | No | Goal status: 'goals' (open goals), 'complete' (no goals left - proof finished here), 'no_goal_at_position' (position carries no proof state), or 'still_elaborating' (timeout_s hit - poll again) | |
| goals_after | No | Goals at line end (when column omitted) | |
| goals_before | No | Goals at line start (when column omitted) | |
| line_context | Yes | Source line where goals were queried |