Build the Lean project and restart LSP. Use only if needed (e.g. new imports).

Get imports and declarations with type signatures. Token-efficient.

Get compiler diagnostics (errors, warnings, infos) for a Lean file.

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.

Get the expected type at a position.

Get type signature and docs for a symbol. Essential for understanding APIs.

Get IDE autocompletions. Use on INCOMPLETE code (after . or partial name).

Get file where a symbol is declared. Symbol must be present in file first.

Find all references to a symbol (including the declaration). Position cursor at the symbol.

Try multiple tactics without modifying file. Returns goal state for each.

Run a code snippet and return diagnostics. Must include all imports.

Check theorem axioms + optional source scan. Only scans the given file, not imports.

Fast local search to verify declarations exist. Use BEFORE trying a lemma name.

Limit: 3req/30s. Search Mathlib via leansearch.net using natural language.

Examples: "sum of two even numbers is even", "Cauchy-Schwarz inequality",
"{f : A → B} (hf : Injective f) : ∃ g, LeftInverse g f"

Search Mathlib by type signature via loogle.lean-lang.org.

Examples: `Real.sin`, `"comm"`, `(?a → ?b) → List ?a → List ?b`,
`_ * (_ ^ _)`, `|- _ < _ → _ + 1 < _ + 1`

Limit: 10req/30s. Semantic search by mathematical meaning via Lean Finder.

Examples: "commutativity of addition on natural numbers",
"I have h : n < m and need n + 1 < m + 1", proof state text.

Limit: 6req/30s. Find lemmas to close the goal at a position. Searches premise-search.com.

Limit: 6req/30s. Get premise suggestions for automation tactics at a goal position.

Returns lemma names to try with `simp only [...]`, `aesop`, or as hints.

Get LSP code actions for a line. Returns resolved edits for TryThis suggestions (simp?, exact?, apply?) and other quick fixes.

Get panel widgets at a position (proof visualizations, #html, custom widgets). Returns raw widget data - may be large.

Get JavaScript source of a widget by hash. Useful for understanding custom widget rendering logic. Returns full JS module - may be large.

Run lean --profile on a theorem. Returns per-line timing and categories. SLOW - avoid on theorems that already hit heartbeat limits.