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 LSP code actions for a line. Returns resolved edits for TryThis suggestions (simp?, exact?, apply?) and other quick fixes.

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).

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 the source of a symbol's declaration (declaration slice + context).

Set full_file=True for the whole file (can be very large).

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

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

Limit: 90req/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.

The `version` argument selects which mathlib snapshot to query
(v4.19.0, v4.24.0, or v4.28.0). Default: v4.28.0.

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.

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.

For each explicit (h : T) hypothesis of a theorem, drop it and re-elaborate a scratch copy of the file. Reports which hypotheses are load-bearing and which are actually unused. Skips implicit {x : α} and instance [inst : C] binders (those are usually inferable / always load-bearing). Does not rewrite the proof body — a body that names h will fail to elaborate without the binder, which is the truthful answer (load-bearing).

Variants are checked in parallel on scratch documents; the file is never edited.

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

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.