| name | improve |
| description | Improve Lean proofs: style, readability, and golfing. Use when asked to improve, golf, compress, shorten, or clean up Lean proofs. |
| paths | ["**/*.lean"] |
Improve Lean Proofs
Style, readability, and golfing techniques for Lean proofs.
Mandatory verification
Every change MUST be verified before committing. Run all four checks
from AGENTS.md in order and READ the output — warnings count as failures:
lake exe cache get
lake build BridgelandStability
lake exe runLinter
lake exe lint-style
If there are ANY new warnings compared to the baseline, revert.
Workflow
Two phases: a file-wide scan (tiers 1-3), then theorem-by-theorem improvements (tiers 4-8). Verify each edit with lean_diagnostic_messages before moving on.
Phase 1: File-wide
1. Extract helpers for duplicated proof skeletons
The single highest-ROI technique. If 2+ proofs differ only in the function/lemma/constant applied, extract the skeleton into a parameterized helper. Typical savings: 10-30 lines per extraction. Scan for pairs of proofs with identical structure before doing anything else.
Also look for deduplication via:
wlog for symmetric cases — eliminates one branch entirely.suffices to deduplicate symmetric case splits — extract the common proof, have each branch only produce the witness.by_cases hoisting — when two branches share the same conclusion, hoist it to a have ... by block containing the by_cases.
2. Replace with mathlib or derive from neighbours
- Replace private helpers with mathlib lemmas — use
lean_loogle with the type signature to find exact matches.
- Derive lemmas from each other — build on what's already proven nearby rather than reproving from scratch.
3. Run the pattern checker
python3 "${CLAUDE_SKILL_DIR}/check_patterns.py" <file.lean>
Detects mechanical improvements: push_neg → push Not (deprecated),
consecutive blank lines, consecutive rw, := by exact → :=,
grind [.symm], duplicate open, long lines (>100 codepoints).
Fix all findings before moving to per-theorem work.
Phase 2: Theorem-by-theorem
Work through each declaration individually. Verify with lean_diagnostic_messages after each edit.
Instant wins (always apply)
| Before | After |
|---|
ext x; rfl | rfl |
simp; rfl | simp |
constructor; exact h1; exact h2 | exact ⟨h1, h2⟩ |
apply f; exact h | exact f h |
:= by exact t | := t |
push_neg | push Not |
Minimum value filter
1-line savings are only worth making if (a) zero-risk syntax cleanup (e.g. by exact → term) or (b) they also improve clarity or performance. Don't churn code for marginal compression.
4. linear_combination for algebraic goals
Try on EVERY proof that ends in ring or ring_nf and has hypotheses in context. Closes goals that ring can't when hypotheses are needed. For goals involving I² = -1: linear_combination (coefficient) * I_sq. Does not work on Prop-valued goals or goals with ofReal casts.
5. Inline single-use have blocks
The highest-volume technique. have h := X; exact h.foo → exact X.foo. Inline into function arguments: have hf := ...; apply g hf → apply g (...). Best targets: single-use haves where the body is ≤1 line.
Caveat: grind and omega are context-sensitive — grind [lemma] can time out in large proof contexts. Keep standalone lemmas when inlining causes timeouts.
6. grind subsumption
grind often subsumes preceding tactics — try deleting what comes before it:
rw [h]; grind → grind (when h is a local hypothesis or simple rewrite)congr 1; grind → grindsimp; grind → grindsimp [lemmas] <;> grind → grind [lemmas]rw [ht]; omega → grind (when ht is a substitution)grind [lemma.symm] → grind [lemma] (grind handles symmetry internally)
7. API shortcuts
fun_prop for continuity/differentiability — (by fun_prop : Continuous _).continuousOn inlines 3-line proofs.field_simp + ring replaces verbose calc chains with denominators. field is shorthand for field_simp; ring.push_cast; ring for ℝ→ℂ cast goals.gcongr for monotonicity/congruence goals.nlinarith [explicit_product_hint] for nonlinear inequalities.simp only [def, h₁, h₂] at h to replace unfold foo; rw [if_pos h1]; rw [if_neg h2] chains.refine ⟨..., ?_, ?_⟩ <;> grind [def, key_fact] to close multiple structurally similar goals at once.- Collapse
calc to term-mode: calc a ≤ b := h1; _ ≤ c := h2 → le_trans h1 h2. Two-step calc with gcongr → rw [...]; gcongr.
8. Remove unused parameters
Check for "unused variable" warnings and remove the parameter + all caller arguments. Grep for _h prefix to find them quickly.
Known-bad patterns (DO NOT apply without LSP verification)
rw [...]; exact t → rwa [...] — Only works when t is a
bare local hypothesis. rwa calls assumption, which cannot find
library lemmas, function applications, or complex expressions.
ALWAYS verify with lean_diagnostic_messages after applying.by_contra! — Expands to by_contra; push_neg, and push_neg
is deprecated in current Mathlib. Do NOT use.show T from inferInstance → inferInstance — The show
provides a type hint needed for instance synthesis. Do NOT remove
without LSP verification.
What doesn't work
- Semicolon joins in multiline proofs — banned antipattern.
grind — rarely closes goals with zpow, Even/Odd, or cast arithmetic.- Analysis boilerplate — integrability/measurability/continuity proofs resist compression without new API. These are the hardest to golf.
- Modular form slash action proofs — specialized API doesn't simplify further.
- Dominated convergence proofs — each sub-proof (bound, summability, pointwise convergence) is already near-minimal.
