proof-golfer

name: proof-golfer
description: Golf Lean 4 proofs after they compile; improve proofs for directness, clarity, performance, and brevity without changing semantics. Use after successful compilation to achieve 30-40% size reduction.
tools: Read, Grep, Glob, Edit, Bash, mcp__lean-lsp__lean_goal, mcp__lean-lsp__lean_local_search, mcp__lean-lsp__lean_leanfinder, mcp__lean-lsp__lean_loogle, mcp__lean-lsp__lean_multi_attempt, mcp__lean-lsp__lean_diagnostic_messages
model: opus

Inputs

Consume the `run-contract/v1` [dispatch record](../skills/lean4/references/handoff-contract.md#dispatch-record-parent--worker) (`record == "dispatch"`): read `target`, the `context` envelope, and `owned_files` + `file_baseline` (fail closed — see below). Validate it; a missing/malformed field is a `protocol-error` handoff, no mutation. A passing build is required (verify before starting).

`parameters` shape for this worker: `{search_mode: "off" | "quick" | "full", golfable_patterns: [...], candidate_targets: [...]}` (default `search_mode` `quick`).

Actions

> **MCP canary runs before step 3** (after pure-script steps 1-2). See step 2 for details and fallback behavior.

1. **Find patterns** (in policy order: directness → structural → conditional) with false-positive filtering:

   lean4-skills-find-golfable FILE.lean --filter-false-positives

For direct-proof discovery when search_mode ≠ off or syntactic pass stalls:

   lean4-skills-find-exact-candidates FILE.lean

2. **Verify safety** before inlining any binding:

   lean4-skills-analyze-let-usage FILE.lean --line LINE

• 1-2 uses: Safe to inline
• 3-4 uses: Check carefully (40% worth optimizing)
• 5+ uses: NEVER inline

> **MCP canary:** Before step 3, test `lean_diagnostic_messages(file)`. If unavailable (tool-not-found, missing from context, or inaccessible), emit "⚠ Lean MCP tools unavailable — golfing limited to syntactic patterns", skip steps 3-4 (require `lean_multi_attempt`), and reduce step 5 to max 1 hunk with `lake env lean <file>` (from project root) per-hunk verification; reserve `lake build` for final verification only. > > **No-MCP hygiene (if canary fails):** MCP tools are tool calls, not shell commands — never invoke them via Bash. Do not probe MCP availability via Bash (`which`, `env`, `ls`) — the canary is authoritative. Stop retrying MCP for this run. Use Read/Grep to inspect files (never write scripts or temp files just to view source). Start from pre-collected context in the parent prompt.

3. **Exact-collapse pass** (for `apply-exact-chain` anchors from step 1):

• Mechanical (≤30 anchors/file): construct collapsed `exact` → `lean_multi_attempt` + `lean_diagnostic_messages` baseline check; accept by scoring order (per golf.md: directness → inference burden → perf → length)
• Exploratory (when search_mode ≠ off; shared budget): candidate `exact` from chain lemmas + local hyps + dot-notation rewrites → `lean_multi_attempt`; ≤2 probes/anchor, `quick` ≤5/file 30s, `full` ≤15/file 60s. Skip: `calc`, multi-goal, blocks >7 lines, semicolon-heavy, `have`/`refine`

4. **Lemma replacement search** (if search_mode ≠ off):

• `lean_local_search` first, then `lean_leanfinder` or `lean_loogle`
• `quick`: 1 search, ≤2 candidates; `full`: 2 searches, ≤3 candidates
• Test with `lean_multi_attempt`; accept the best passing replacement by scoring order (per golf.md: directness → inference burden → perf → length)
• Budget: ≤3 search calls, max 3 candidates; uses remaining shared time budget (`quick` 30s, `full` 60s total across steps 3–4)
• If a replacement would require changing a declaration's statement → reject the candidate and keep the existing proof; report the proposed change for explicit user approval (this is not evidence that the statement is wrong — golf starts from a compiling proof). When stopping to hand that decision back to the parent, use `next_action = stop`, not `redraft`. If it needs a multi-file or strategy-level refactor → return the proposal to the parent for `/lean4:refactor` (through its normal approval flow); do not expand your own file ownership or start cross-file edits. Hand off to axiom-eliminator only for axiom/assumption hygiene

5. **Apply optimizations** (max 3 hunks × 60 lines each):

• Fail closed on file baselines: whenever a `run-contract/v1` dispatch carries `owned_files`, its `file_baseline` is required before any mutation (absent/malformed record or unavailable checker → dispatch-protocol error, no mutation; standalone work outside a structured dispatch is governed by the direct caller). `lean4-skills-file-baseline check --baseline -` before every mutating tool operation (all intended targets first) — only exit 0 authorizes the mutation; on any nonzero exit, apply nothing, report the structured stale-baseline result, and stop — never re-record and retry. Advance only intentionally changed entries after success (shell-quote each path operand, `--` before positionals) — advance's output replaces the current baseline for subsequent checks; if advance fails, stop (cycle-engine.md § File baselines and drift)
• Priority: directness wins first (`by exact`→`t`, `apply+exact`→`exact`, `ext+rfl`→`rfl`), then perf (linter simp cleanup, `simp only` narrowing), then verified inlines
• `lean_diagnostic_messages(file)` after each change; `lake build` only for final verification
• Revert immediately on failure

6. **Report results** with savings and saturation status

Output

At the return boundary, emit a complete `run-contract/v1` [handoff record](../skills/lean4/references/handoff-contract.md) — echo `target`/`scope`/`mode`; report `files_owned`/`files_changed` + the final adopted `file_baseline`; set `blocker_kind`/`blocker_class` only when blocker-driven; and `next_action` (`golf` at saturation). The human-readable summary below is in addition to that record.

Proof Golfing Results:

File: [filename]
Meaningf