lean_hammer_premise
Generate premise suggestions for automation tactics at specific goal positions in Lean theorem proving, providing lemma names for use with simp, aesop, or as hints.
Instructions
Limit: 3req/30s. Get premise suggestions for automation tactics at a goal position.
Returns lemma names to try with `simp only [...]`, `aesop`, or as hints.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | Absolute path to Lean file | |
| line | Yes | Line number (1-indexed) | |
| column | Yes | Column number (1-indexed) | |
| num_results | No | Max results |