# Anti-patterns

Each entry: what it is, why it is harmful (not just that it is), and which
mechanism catches it. The meta-lesson from Mathlib's history: **review alone
does not catch these** — the first simp-normal-form linter found over one
hundred redundant simp lemmas that had all passed expert maintainer review.
Put the check in tooling.

## Proof-level

### Monolithic tactic blocks

One long unstructured tactic sequence. Harmful because the argument's
structure is invisible — the only way to follow it is to replay it in an
editor, and the only way to repair it after a library bump is to rebuild it
from scratch. Caught by: review ("long and unwieldy" → split). Fix: sorry
skeleton first, extraction ladder after.

### Unfocused multiple goals

Running tactics while several goals are active, relying on goal order.
Harmful because any change to an earlier tactic silently redirects later
tactics to different goals. Caught by: `multiGoal` linter. Fix: `·` blocks,
one per goal.

### Squeezed terminal simp

`simp only [thirty, lemmas, ...]` closing a goal. Harmful because it breaks
on any rename among the thirty and hides the one lemma that mattered.
Terminal `simp` calls stay unsqueezed; only _non-terminal_ calls get
squeezed (a bare non-terminal `simp` is the mirror-image anti-pattern: it
couples following tactics to the ambient simp set). Caught by: review; the
style guide states the rule.

### Dishonest `show`

`show` that actually changes the goal. Harmful because readers trust `show`
lines as documentation of the goal state; a goal-changing one is
documentation that lies. Caught by: `show` linter. Fix: `change`.

### `native_decide` in library code

Proves a proposition by compiling it to native code and trusting the
result (the `Lean.ofReduceBool` axiom). Harmful because it silently widens
the trust base from the kernel to the entire compiler and runtime;
Mathlib disallows it. Caught by: `#print axioms` (reports
`Lean.ofReduceBool`); Mathlib CI. Fix: `decide` where the kernel can
afford the computation, a certificate-based `norm_num` proof, or an
explicitly documented decision to accept the axiom.

### Leftover debugging scaffolding

`set_option pp.all true`, `trace`/`profiler`/`debug` options, unscoped
`maxHeartbeats`. Harmful as noise and as behavioral drift (heartbeat
overrides mask performance regressions). Caught by: `setOption` linter.

### Golfed nontrivial proofs

Compressing a real argument into a one-liner of chained combinators.
Harmful because review policy subordinates golfing to readability — the
short form is only acceptable when it reads at least as well. Trivial
results are the carve-out. Caught by: review.

### Non-canonical statements

Stating with `>` instead of `<`, or against a concrete spelling instead of
the designated simp-normal form. Harmful because simp and every API lemma
match syntactically — off-normal statements need duplicate API or never get
rewritten. Caught by: `simpNF` linter (for simp lemmas); review. The numeral
special case is easy to miss: a simp lemma keyed on `2 ^ 32` never fires on
a goal normalized to `4294967296` — the lemma is true, applicable-looking,
and dead. Prefer structural LHS patterns with no numeral at all.

### Copy-pasted resource budgets

The same `set_option maxHeartbeats N in` value on many declarations.
Harmful because at that density the annotations carry no information about
which proof is actually expensive, and every unmeasured budget masks the
regression it was meant to surface — audits have found "6.4M-heartbeat"
proofs that run at the default budget once measured. Caught by:
`#count_heartbeats` bisection; Mathlib's `maxHeartbeats` style linter (which
demands a justification comment on every override — the unscoped file-level
form is the `setOption` linter's, see "Leftover debugging scaffolding"
above). Fix: measure, keep only the overrides that are real, each scoped to
its declaration.

## Library-level

### Project conventions enforced only by review

A project-specific construct — a simp-set discipline, a required attribute,
a coverage rule like "every constructor the executor handles has a soundness
lemma" — with no linter behind it. Harmful because the failure mode is
forgetting the step on 1 of 30 declarations with no visible symptom, which
is precisely what review does not catch (and what models writing Lean get
wrong). Caught by: nothing — that is the problem. Fix: a declaration-level
`@[env_linter]` wired into CI's `#lint`, written alongside the construct,
not after the first regression. See [linting.md](linting.md).

### Definitional transparency abuse

Downstream proofs that `unfold`, use `erw`, or need a trailing `rfl` to see
through a definition. Harmful because each one couples a proof to the
implementation; the first refactor breaks them all. The style guide calls
this _missing API_. Caught by: review; the `erw`/trailing-`rfl` smell. Fix:
add the missing lemma next to the definition.

### Definitions without API

A definition used bare, with lemmas about it scattered where they were
first needed. Harmful because every user re-derives basic facts, usually by
unfolding (see above). Caught by: PR review checklist ("do new definitions
come with lemmas about them?"). Fix: same-file `ext`/`simp`/coe/injectivity
lemmas before first use.

### Unbundled predicates for morphisms/subobjects

`IsHom f` predicates instead of a bundled `Hom` structure with `FunLike`.
Harmful because instance search cannot reliably discharge `IsHom (f ∘ g)`,
and the predicate form forfeits the algebraic structure of the hom-type
itself. Caught by: review guide (directs to FunLike/SetLike).

### Side conditions instead of junk values

Partial operations via subtypes or hypotheses on the _operation_ rather
than junk-value totalization. Harmful because the side condition reappears
at every use site ("every step slightly painful" — perfectoid retrospective
on the subtype approach). Fix: total function + junk value; hypotheses only
on the lemmas that need them.

### Global `Fact` instances

`instance : Fact (Nat.Prime 37)` at top level. Harmful because every
typeclass search everywhere now considers it. Fix: state as lemma, make a
local instance where needed.

### Premature typeclasses

A new class with no theory behind it. The bar: real mathematics to be done
with it, or genuine simplification from a factored substructure. Prefer
`extends` to mixin parameters.

## Claims to avoid making

When editing or reviewing, do **not** cite these as rules — they are
commonly repeated but unsupported or wrong:

- "One tactic per line is an absolute requirement" — Mathlib recommends one
  tactic invocation per line in general, but explicitly excepts a proof that
  closes the goal and fits entirely on one line. Apply the recommendation
  with that exception instead of inventing a hard rule.
- Any numeric proof-length threshold ("proofs over 20 lines must be split")
  — the review criterion is deliberately qualitative.

# Library design: definitions, APIs, and project decomposition

How Mathlib and the large formalization projects structure theory
development. Sources are Mathlib's style and PR review guides, the Mathlib
papers (CPP 2020; van Doorn–Ebner–Lewis, CICM 2020), the perfectoid spaces
retrospective (Buzzard–Commelin–Massot, CPP 2020), and Commelin–Topaz,
"Abstraction boundaries and spec driven development in pure mathematics"
(Bull. AMS, from the Liquid Tensor Experiment).

## Spec-driven development

Decompose before proving. The LTE methodology, recursively:

1. Isolate a target (definition or theorem).
2. Write its spec: the statement, plus the API lemmas it should satisfy.
3. Break both into lower-complexity parts.
4. Recurse, using `sorry` as a placeholder for **both data and proofs**.

State API lemmas *before the definition exists*:

```lean
def condensedAb : Type := sorry            -- data placeholder

lemma val_app_add (f g : condensedAb) : val (f + g) = val f + val g := sorry
```

Nobody can depend on an implementation detail, because there is no
implementation yet. Collaborators immediately build on the sorried
assertions in parallel and fill targets independently. Tao's PFR project
formalized a 33-page proof with ~20 collaborators in three weeks this way;
Tao: formalization "allows for individual subtasks in the project to be
precisely defined and verified independently of the other subtasks", so
projects "routinely involve scores of people who may have had no prior
interaction". Buzzard (FLT): "you do not have to understand the whole proof
of FLT in order to contribute."

For multi-contributor projects, consider a
[leanblueprint](https://github.com/PatrickMassot/leanblueprint) — a
human-readable outline whose `\uses{...}` annotations generate the
dependency graph and whose `\lean{...}`/`\leanok` links track formalization
status per node. No source prescribes node size; the working criterion is
that **one contributor can complete one node without global context**.

## Statements are the interface; proofs are disposable

Lean propositions are proof-irrelevant: only a theorem's statement can
affect later declarations. Consequences:

- Design effort concentrates on definitions and statements. Mathlib requires
  doc strings on definitions but not on ordinary theorems — statements are
  self-documenting; definitions need justification.
- Refactoring a proof is always safe; refactoring a statement or definition
  is a breaking change. Get statements right first (the sorry skeleton).

## Every definition ships its API, immediately, in the same file

Before a definition is used anywhere, write:

- the `@[simp]` lemmas that compute with it in its canonical form,
- an `@[ext]` lemma (stated *partially applied* — Mathlib's
  "partially-applied ext lemmas" convention — so later ext lemmas compose
  step-wise),
- coercion/`FunLike` lemmas, injectivity lemmas, and the rewrite lemmas that
  let users avoid definitional reasoning.

Explain the design decisions (typeclass choices, simp-normal form) in the
module docstring.

**The smell test**: needing `erw`, or a trailing `rfl` after `simp`/`rw`, is
the style guide's official signal of *missing API*. The fix is a new lemma,
never unfolding. Do not confuse this with the API lemmas themselves: an
`@[simp]` projection lemma *proved by* `rfl` next to its definition is the
boundary working as intended — the smell is a downstream proof *needing*
`rfl` to see through the definition.

## Abstraction boundaries are explicit decisions

- Definitions default to **semireducible** transparency; any deviation must
  be justified (in Mathlib: in the PR description).
- A **sealed** boundary is a one-field structure wrapper, not `irreducible`:

  ```lean
  structure MyDef where
    underlying : UnderlyingTerm
  ```

- `irreducible_def` only with a documented profiling reason.

## Optimized definitions keep a readable reference

When a definition must be rewritten for elaboration or reduction speed, do
not replace it — keep the readable definition as the reference semantics,
add the fast form beside it, and prove them equal for *every* input
(including degenerate and failure cases). Downstream proofs keep using the
readable form and repoint with a single `rw` where they touched the old
shape; the optimization cannot silently change meaning; and the intended
semantics stay legible. This is "statements are the interface" applied to
definitions under optimization. Mechanics and the reduction-cost diagnosis
that motivates it: [performance.md](performance.md).

## Simp-normal form

When a term has multiple equivalent spellings, designate one canonical form
— prefer the generic one (`‖x‖` over a concrete `padicNorm`, `<` over `>`) —
orient `@[simp]` lemmas to rewrite toward it, and state every subsequent API
lemma only for it. The simplifier matches up to syntactic equality; without
a normal form, every lemma needs restating for every spelling. The `simpNF`
linter checks that simp lemma left-hand sides are themselves in normal form.

## Total functions with junk values

Prefer totalizing a function with a junk value over restricting its domain:
in Mathlib, `(0 : ℝ)⁻¹ = 0` and division is total. The payoff is
modularity: the `x ≠ 0` side condition disappears from every use site, and
hypotheses appear only on the lemmas that genuinely need them —

```lean
theorem div_add_div_same (a b c : α) : a / c + b / c = (a + b) / c := ...
  -- unconditional: holds also when c = 0, both sides are junk

theorem mul_inv_cancel₀ (h : a ≠ 0) : a * a⁻¹ = 1 := ...
  -- the hypothesis lives only where the mathematics requires it
```

The perfectoid-spaces authors tried the alternative (a bundled subtype of
units) and reported that it made "every step slightly painful, because
inclusions are harder to ignore in formalised type theory."

## Bundling

- **Morphisms**: define a bundled structure plus a `FunLike`-style class,
  never an `IsHom f` predicate — instance search cannot reliably solve
  goals like `IsHom (f ∘ g)`, while a bundled `Hom` type gets its own
  composition and its own algebraic structure.

  ```lean
  structure MonoidHom (M N : Type*) [Monoid M] [Monoid N] where
    toFun : M → N
    map_one' : toFun 1 = 1
    map_mul' : ∀ a b, toFun (a * b) = toFun a * toFun b
  ```

- **Subobjects**: bundled carrier + `SetLike` instance.
- **Type classes**: semi-bundled — bundle all operations, leave only the
  carrier type as a parameter (`Monoid M`, not fully-bundled `Monoid` nor
  unbundled `IsMonoid M mul one`).

## Restraint on new abstractions

- Introduce a new algebraic typeclass only when there is real mathematics to
  do with it, or a genuine simplification from factoring out a shared
  substructure. Prefer `extends` over mixin parameters.
- `Fact` bridges a proposition into typeclass search *locally*:

  ```lean
  theorem foo (p : ℕ) (hp : p.Prime) : ... := by
    have := Fact.mk hp   -- local instance, scoped to this proof
    ...
  ```

  Never declare global `Fact` instances — they degrade instance search
  everywhere.

## Choosing the abstraction level is the dominant proof-shortener

Work at the highest level that expresses the mathematics. The perfectoid
retrospective's example: stating uniform continuity via filters instead of
unfolding to sets of pairs "allows to break the proofs into small lemmas
that are needed anyway", collapsing "uniformly continuous implies
continuous" to roughly twice the length of the sentence "this follows
immediately from definitions".

When informal mathematics silently identifies isomorphic constructions,
don't fight the identification — introduce a predicate characterizing the
object by its properties (the "abstract completion" move) and prove your
theorems for anything satisfying the predicate.

# Linting: gates in CI early, custom linters for your own constructs

## Contents

- [The sorry gate: ask the kernel, not grep](#the-sorry-gate-ask-the-kernel-not-grep)
- [Choose a project-specific linter profile](#choose-a-project-specific-linter-profile)
- [Adopting a linter that is not yet clean](#adopting-a-linter-that-is-not-yet-clean)
- [Custom linters](#custom-linters-every-project-convention-worth-having-is-worth-one)
- [Prove every check can fail](#prove-every-check-can-fail-before-trusting-that-it-passes)

**Set up an appropriate linter set, gated in CI, at the start of the project — and
write a custom linter for every project-specific convention.** Bugs and
unidiomatic proof patterns propagate by copy-paste: the first bad `simp` call
becomes the template for the next fifty, and a linter adopted late meets a
backlog instead of a single bad line (measured in one project: one deferred
linter had accumulated 438 warnings across 25 files; adopted on day one it
would have flagged one). Review does not substitute — the first simp-normal-
form linter found 100+ redundant simp lemmas in Mathlib that had all passed
expert maintainer review. This matters doubly when a model writes the Lean:
models follow a convention *almost* everywhere and forget the step with no
visible symptom; only a linter reliably catches "the attribute is missing on
29 of 30 declarations".

## The sorry gate: ask the kernel, not grep

Gate unproved obligations with axiom collection, never `grep sorry`. Grep is
wrong in both directions: it matches the word in comments and docstrings, and
it misses a theorem whose own text is clean but which applies an unproved
helper. `Lean.collectAxioms` catches exactly the real cases:

```lean
-- Save as scripts/AxiomCheck.lean in YOUR project; CI runs:
--   lake env lean scripts/AxiomCheck.lean
import MyProject
open Lean

/-- Axioms the library is known and intended to depend on. Anything else —
    a new `sorry`, a stray `native_decide` — fails loudly. -/
def expectedAxioms : List Name := [``propext, ``Classical.choice, ``Quot.sound]

/-- Is this declaration defined in one of our own modules (not Mathlib etc.)? -/
def isOurs (env : Environment) (n : Name) : Bool :=
  match env.getModuleIdxFor? n with
  | none => false          -- defined in the current file, not the library
  | some idx =>
      match env.header.moduleNames[idx.toNat]? with
      | some m => (`MyProject).isPrefixOf m
      | none => false

run_cmd Elab.Command.liftCoreM do
  let env ← getEnv
  let mut checked := 0
  for (n, _) in env.constants.toList do
    unless isOurs env n && !n.isInternal && !n.hasMacroScopes do continue
    checked := checked + 1
    let axs ← collectAxioms n
    if axs.contains ``sorryAx then throwError "unproved: {n}"
    let bad := axs.filter (!expectedAxioms.contains ·)
    unless bad.isEmpty do throwError "unexpected axioms on {n}: {bad.toList}"
  if checked == 0 then
    throwError "module filter matched nothing — the check is vacuous"
```

Assert the **whole footprint**, not just `sorryAx`: listing the expected
axioms turns "we think nothing else crept in" into a checked claim, so a new
trust assumption (someone adding `native_decide`) fails instead of landing
silently. And note the final line — see "Prove every check can fail" below.

## Choose a project-specific linter profile

Do **not** enable `linter.mathlibStandardSet` wholesale just because a project
depends on Mathlib. At Mathlib commit
[`50a1a360`](https://github.com/leanprover-community/mathlib4/blob/50a1a3609f97d1a965d8eaba5088d846dab11dce/Mathlib/Init.lean),
the set contains 26 lints with four different jobs:

- proof robustness and debugging;
- reusable public-API design;
- optional source-formatting conventions; and
- Mathlib's own repository policy.

Those are appropriate defaults for Mathlib, not one indivisible policy for
every downstream package. Select individual options according to who will
consume the code, and re-audit the list when updating the pinned Mathlib
revision.

### Recommended profile: self-contained project or proof

For a finished proof, executable specification, verification artifact, or
application whose declarations are not a downstream API, start with the
checks that prevent fragile proof scripts and leftover debugging state:

```lean
leanOptions := #[
  ⟨`weak.linter.auxLemma, true⟩,
  ⟨`weak.linter.style.maxHeartbeats, true⟩,
  ⟨`weak.linter.style.multiGoal, true⟩,
  ⟨`weak.linter.style.setOption, true⟩,
  ⟨`weak.linter.style.show, true⟩
]
```

Add `linter.flexible` if the artifact will be maintained across dependency
updates; it makes intermediate broad automation such as bare `simp` more
explicit, but can impose substantial cleanup on a short-lived proof. Add
the deprecated-syntax checks only when the project deliberately follows
Mathlib's tactic style. Do not enable public-API or documentation lints
merely to make the profile resemble Mathlib.

### Recommended profile: reusable library

For a library intended to be imported by other projects, also protect API
generality, module structure, and upgrade resilience:

```lean
leanOptions := #[
  ⟨`weak.linter.auxLemma, true⟩,
  ⟨`weak.linter.flexible, true⟩,
  ⟨`weak.linter.style.maxHeartbeats, true⟩,
  ⟨`weak.linter.style.missingEnd, true⟩,
  ⟨`weak.linter.style.multiGoal, true⟩,
  ⟨`weak.linter.style.openClassical, true⟩,
  ⟨`weak.linter.style.setOption, true⟩,
  ⟨`weak.linter.style.show, true⟩,
  ⟨`weak.linter.unusedDecidableInType, true⟩,
  ⟨`weak.linter.unusedFintypeInType, true⟩
]
```

This is a starting profile, not another aggregate to copy blindly. A library
with intentionally broad automation may omit `linter.flexible`; a package
whose modules are generated may omit structural style checks.
`linter.style.nameCheck` is not a member of `mathlibStandardSet`; it defaults
to `true` and catches double underscores, not the whole Mathlib naming
convention. A library adopting that convention should also run Batteries'
`#lint defsWithUnderscore` and use review for the rules no linter covers.

Apply the classification per target or module, not merely per repository. A
reusable library commonly includes terminal examples, tests, and regression
fixtures for which its public-source policy is inappropriate.

### Audit of every standard-set member

`Enable` means it belongs in the profile above. `Consider` means its value
depends on expected maintenance or local conventions. `Policy` requires an
explicit trust or repository decision. `Avoid` means that enabling it without
narrow scoping is likely to reject legitimate downstream code.

| Lint | What it protects | Reusable library | Self-contained project / proof |
|------|------------------|------------------|--------------------------------|
| `linter.auxLemma` | Avoids references to generated names such as `_proof_1` that can change after unrelated edits | Enable | Enable |
| `linter.flexible` | Makes non-terminal broad tactics such as bare `simp` explicit, reducing dependence on a changing environment | Enable for maintained libraries | Consider when upgrades matter |
| `linter.hashCommand` | Flags silent `#` commands, and all `#` commands under `warningAsError` | Consider only in production modules that forbid such probes | Usually omit: `#guard` may be an intentional assertion |
| `linter.oldObtain` | Replaces a Lean 3-style `obtain` form with an explicit proof block | Consider as readability style | Consider as readability style |
| `linter.privateModule` | Flags nonempty modules that expose only private declarations | Consider for modules meant to be imported; omit terminal and test modules | Avoid for terminal test and proof modules |
| `linter.style.cases` | Rejects Mathlib's discouraged `cases'` syntax | Consider when adopting Mathlib tactic style | Consider when adopting Mathlib tactic style |
| `linter.style.induction` | Rejects Mathlib's discouraged `induction'` syntax | Consider when adopting Mathlib tactic style | Consider when adopting Mathlib tactic style |
| `linter.style.refine` | Rejects Mathlib's discouraged `refine'` syntax | Consider when adopting Mathlib tactic style | Consider when adopting Mathlib tactic style |
| `linter.style.cdot` | Enforces Mathlib's spelling of the centered dot | Project style | Project style |
| `linter.style.docString` | Enforces Mathlib docstring formatting, not documentation coverage | Consider when adopting Mathlib documentation style | Usually omit |
| `linter.style.dollarSyntax` | Prefers `<|` over `$` | Project style | Project style |
| `linter.style.emptyLine` | Rejects blank lines within declarations | Project style; can be noisy | Project style; can be noisy |
| `linter.style.header` | Enforces Mathlib's license header, module docstring, and import restrictions | Avoid unless deliberately matching the exact Mathlib repository policy | Avoid |
| `linter.style.lambdaSyntax` | Prefers `fun` over `λ` | Project style | Project style |
| `linter.style.longLine` | Enforces a configurable line-length limit | Project style | Project style |
| `linter.style.longFile` | Enforces a chosen file-length limit; this option is a number, not a Boolean | Consider only with a locally chosen limit | Usually omit; generated artifacts may be long |
| `linter.style.multiGoal` | Prevents tactics from depending silently on the order of several active goals | Enable | Enable for finished, maintainable proofs |
| `linter.style.nativeDecide` | Warns about compiler-backed `native_decide` and `decide +native` | Policy: enable if the trust model forbids them | Policy: choose explicitly |
| `linter.style.openClassical` | Discourages global classical scope that can hide unnecessarily strong theorem assumptions | Enable for public APIs | Consider when theorem statements are reused |
| `linter.style.maxHeartbeats` | Requires an explanation next to scoped heartbeat overrides | Enable | Consider when budgets are allowed |
| `linter.style.missingEnd` | Makes namespace and section boundaries explicit | Enable | Consider for multi-section files |
| `linter.style.setOption` | Catches leftover traces, profilers, pretty-printer flags, and unscoped sensitive options | Enable outside dedicated fixtures | Enable outside dedicated fixtures |
| `linter.style.show` | Prevents `show` from silently changing the target; requires honest `change` | Enable | Enable |
| `linter.style.whitespace` | Enforces Mathlib declaration spacing | Project style | Project style |
| `linter.unusedDecidableInType` | Removes an unnecessary `Decidable` assumption from a theorem's public type | Enable | Consider only when statements are reused |
| `linter.unusedFintypeInType` | Removes or weakens an unnecessary `Fintype` assumption in a theorem's public type | Enable | Consider only when statements are reused |

The behavior classifications above come from the corresponding current
Mathlib implementations: [auxiliary names](https://github.com/leanprover-community/mathlib4/blob/50a1a3609f97d1a965d8eaba5088d846dab11dce/Mathlib/Tactic/Linter/AuxLemma.lean),
[flexible tactics](https://github.com/leanprover-community/mathlib4/blob/50a1a3609f97d1a965d8eaba5088d846dab11dce/Mathlib/Tactic/Linter/FlexibleLinter.lean),
[`#` commands](https://github.com/leanprover-community/mathlib4/blob/50a1a3609f97d1a965d8eaba5088d846dab11dce/Mathlib/Tactic/Linter/HashCommandLinter.lean),
[legacy `obtain`](https://github.com/leanprover-community/mathlib4/blob/50a1a3609f97d1a965d8eaba5088d846dab11dce/Mathlib/Tactic/Linter/OldObtain.lean),
[private modules](https://github.com/leanprover-community/mathlib4/blob/50a1a3609f97d1a965d8eaba5088d846dab11dce/Mathlib/Tactic/Linter/PrivateModule.lean),
[deprecated syntax](https://github.com/leanprover-community/mathlib4/blob/50a1a3609f97d1a965d8eaba5088d846dab11dce/Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean),
[general style](https://github.com/leanprover-community/mathlib4/blob/50a1a3609f97d1a965d8eaba5088d846dab11dce/Mathlib/Tactic/Linter/Style.lean),
[docstrings](https://github.com/leanprover-community/mathlib4/blob/50a1a3609f97d1a965d8eaba5088d846dab11dce/Mathlib/Tactic/Linter/DocString.lean),
[empty lines](https://github.com/leanprover-community/mathlib4/blob/50a1a3609f97d1a965d8eaba5088d846dab11dce/Mathlib/Tactic/Linter/EmptyLine.lean),
[headers](https://github.com/leanprover-community/mathlib4/blob/50a1a3609f97d1a965d8eaba5088d846dab11dce/Mathlib/Tactic/Linter/Header.lean),
[multiple goals](https://github.com/leanprover-community/mathlib4/blob/50a1a3609f97d1a965d8eaba5088d846dab11dce/Mathlib/Tactic/Linter/Multigoal.lean),
[whitespace](https://github.com/leanprover-community/mathlib4/blob/50a1a3609f97d1a965d8eaba5088d846dab11dce/Mathlib/Tactic/Linter/Whitespace.lean),
and [unused instances](https://github.com/leanprover-community/mathlib4/blob/50a1a3609f97d1a965d8eaba5088d846dab11dce/Mathlib/Tactic/Linter/UnusedInstancesInType.lean).

### Make the selected profile an actual gate

Most standard-set members are **off by default in dependent projects**. Five
mechanics matter:

- **`leanOptions` reach every module, and `-D` on an unregistered option is a
  hard error** — a Mathlib-provided `linter.style.*` option breaks any module
  in your package that imports only core Lean. The `weak.` prefix is the
  escape hatch: `⟨`weak.linter.style.multiGoal, true⟩` sets the option where
  it is registered and ignores it where it is not.
- **Use fully qualified individual option names.** Note that
  `linter.flexible` and the two `linter.unused*InType` options are not under
  `linter.style`. Reconfirm every name against the project's pinned Mathlib
  revision. Then add a known-trigger fixture for every option: the `weak.`
  prefix deliberately ignores unknown options, so a typo otherwise produces
  a green build with no linter running.
- **A linter is only a gate if warnings fail the build.** Check what you are
  *already* passing before adopting anything new: ~30 linters can be on and
  clean while nothing protects that compliance. Locking in what you already
  satisfy is cheaper and higher-value than any new adoption. Mechanically,
  warnings-as-errors is a CI step:

  ```sh
  set -o pipefail                        # or the build failure vanishes into tee
  lake build MyProject 2>&1 | tee build.log
  # Vacuity anchor: Lake caches per-module artifacts and linter warnings are
  # emitted only when a module is *recompiled*. On a restored cache with
  # nothing to rebuild, build.log is empty, the grep below matches nothing,
  # and the gate reports clean over live warnings and sorries. Prove the
  # sweep reached something before trusting its silence.
  grep -qE "^(info: )?\[[0-9]+/[0-9]+\]" build.log \
    || { echo "gate is vacuous: lake compiled no module" >&2; exit 1; }
  ! grep -n "warning:" build.log         # any warning (linter or sorry) fails CI
  ```

  The anchor is what makes this a gate rather than a report; the alternative
  is to build the gating job from a cold cache. This is the same discipline
  the `checked == 0` guard enforces in `AxiomCheck.lean` above, and the same
  one the sweep-counting rule below states in general — a check that cannot
  observe its own reach cannot fail.
- **Anything outside the default build target rots silently.** A test or
  regression file that nothing builds stops compiling and nobody notices.
  Give such files their own `lean_lib` target in the lakefile and build that
  target explicitly in CI.
- **Run declaration-level linters too.** The `leanOptions` profiles above
  activate syntax and command linters; they do not replace Batteries'
  `#lint`, whose checks include `simpNF`. Give the linter file a build target
  and execute it explicitly in CI.

When policy enables a lint, exempt a sanctioned violation **locally, never
globally**: `set_option linter.style.nativeDecide false in` immediately above
the one permitted use, with a comment saying why. The linter stays on
library-wide, so a *new* violation still fails, and the exemption is visible
exactly where a reviewer needs it.

## Adopting a linter that is not yet clean

- **A gate that fails is not a gate.** Enable a linter only once it reports
  zero; until then run it advisory with the *measured* backlog recorded next
  to it, and promote it when it reaches zero. Writing the count down is what
  keeps the backlog actionable and stops a later reader assuming the linter
  was rejected on principle.
- **Counts from a failed build are meaningless.** Modules that never compiled
  were never linted; a partial build reports a partial count that reads
  exactly like a clean result. Confirm the build reached the end first.
- **Reported counts can be lower bounds.** `linter.flexible` propagates a
  "stain" that stops at the first fix, so pinning one flagged `simp` unmasks
  the next in the same ladder (measured undercounts of 3×). When a file has a
  repeated idiom, fix *every* occurrence in one pass.
- **Never paste a linter's own `Try this:` suggestion.** The flexible
  linter's suggested `simp only [...]` list comes from re-running a *default*
  `simp`, dropping the arguments the original call passed. Run `simp?` in
  place instead. A tool's suggested fix is a hint about the shape of the fix,
  not a patch.
- **Rank the backlog by warnings-per-edit, not warnings.** One line can carry
  37 warnings and cost one token; a copy-pasted six-line idiom can hold a
  third of the total. Sort the work by idiom, most-duplicated first.
- Adopt for **your** consumers: Mathlib's set is calibrated for a
  million-line library with thousands of downstream users. A verification
  project with a small team should weight correctness- and trust-protecting
  linters up and house-style linters down (e.g. `hashCommand` is wrong for a
  test suite whose `#guard`s *are* the assertions).

## Custom linters: every project convention worth having is worth one

Any new construct your project introduces — a simp-set discipline, a naming
scheme for summary lemmas, an attribute that downstream automation consumes —
will be misused, because nothing enforces it. Defining a linter is genuinely
easy; write one alongside the construct, not after the first regression.

The declaration-level kind (what Batteries' `#lint` runs) is one structure:

```lean
@[env_linter] def mySummaryTagged : Batteries.Tactic.Lint.Linter where
  noErrorsFound := "all execution summaries are tagged"
  errorsFound := "summaries missing @[my_summary]:"
  test n := do
    -- full MetaM access: inspect the type, attributes, docstring, environment
    ...return (some msg) to flag, none to pass
```

`@[nolint mySummaryTagged]` gives per-declaration exemptions for free. (The
other kind — a syntax-level linter à la `linter.style.*` — needs a
`register_option`, a `Linter where run`, and an `initialize addLinter`; the
extra boilerplate buys file-local `set_option … false in` opt-outs. Reach for
it when exemptions must be positional rather than per-declaration.) The
highest-value checks are **coverage invariants** no generic linter can
express — "every constructor the executor handles has a corresponding
soundness lemma" — where the failure mode (extend the executor, forget the
lemma) compiles cleanly and leaves no trace. Implement those as a
declaration-level linter that does its work anchored on one declaration and
returns `none` for everything else.

Engineering rules, each learned the hard way:

- **Prefer a linter over a script that greps source.** Anything checked by
  scraping text (attributes, naming, doc comments) is checkable against the
  *declaration*, where comments, formatting, and renames cannot fool it —
  the same argument that makes `collectAxioms` beat `grep sorry`.
- **Test the shape of a declaration, not its name.** A suffix-keyed linter
  flags look-alikes and misses restatements; match the actual conclusion.
- **Know which side you are checking.** A rewrite's LHS must match the goal;
  its RHS may deliberately use a different spelling that downstream lemmas
  expect. Any statement-syntax check must distinguish the two.
- **Private declarations are not where you think:** `private theorem foo`
  lives at `_private.<module>.0.foo`, so `env.contains ``foo`` ` reports it
  missing. Use `mkPrivateNameCore` per candidate module.
- **Do no expensive per-constant work while iterating `env.constants`.**
  Real work per foreign constant will not finish against a Mathlib-sized
  environment (a string-processing probe over it timed out at 400 s). A cheap
  module-membership filter per constant is fine — the axiom audit above does
  exactly that — but anything heavier belongs behind targeted `env.find?`
  lookups, so cost is O(things you care about), not O(everything Mathlib
  defines).
- **Self-police allowlists:** report entries that no longer exist and entries
  that now satisfy the rule, or the list quietly outlives its justification.
- **Budget the check itself.** A linter can exhaust a module's heartbeat
  budget normalizing a 110-equation match — turning a green module red. Prefer
  a documented local opt-out over abandoning the gate everywhere.
- **Say what the linter does *not* protect**, in its docstring, so a future
  reader does not over-trust it.

## Prove every check can fail before trusting that it passes

A check that silently never fires is indistinguishable from a clean codebase.
For every new gate — linter, sweep, axiom audit:

- Introduce a deliberate violation *and* a near-miss control; confirm the
  first is flagged and the second is not. This regularly finds vacuous
  linters (e.g. a normalization step that never matches, so every candidate
  "passes").
- **Build the vacuity check in permanently**: anchor a sanity assertion on
  one known declaration ("this attribute must exist", "checked > 0"), so the
  gate fails loudly rather than reporting a codebase it never examined.
- Watch the plumbing: plain `lean -Dname=value` rejects an unknown option,
  while `lean -Dweak.name=value` intentionally ignores one so packages can
  span modules with different imports. Verify a weak option in a module that
  imports its linter and include a known violation, or a typo can report zero
  findings. A `#lint` run piped through `tee` without `pipefail` exits 0 even
  when Lean crashed; `git ls-files
  'Proj/**/*.lean'` silently excludes top-level files (`*` in a git pathspec
  matches `/`; `**/` requires an intervening directory — the more
  explicit-looking spelling is the narrower one). Print and assert the number
  of files each sweep reached.

# LLM-specific techniques

Techniques with direct evidence for model-written Lean, primarily from
ImProver (Ahuja, Avigad, Tetali, Welleck; ICLR 2025), plus the structural
practices that make proofs extendable by *other* models.

## Verification in the loop, always

Naively prompting a model to write or optimize Lean proofs largely fails
(ImProver: GPT-4o at 26% accuracy on length optimization, 19% on
readability rewriting). The same system with symbolic Lean context,
error-correction against compiler feedback, retrieval, and
verification-gated output scores 100% on the paper's accuracy metric — by
construction: when no rewritten proof verifies, ImProver falls back to the
unchanged input, so the gate guarantees a correct output rather than a
successful rewrite. That is the lesson: the guarantee comes from the gate,
not from better generation. Practical rule: never emit a proof you have not
compiled (`lake build` / `lake env lean file.lean`). Treat compiler errors
as the feedback channel, not as failure.

## Chain-of-States: annotate compiler-emitted goal states while drafting

The single most impactful technique in ImProver's ablations: before each
tactic, record the current goal state as a comment — *extracted from Lean's
InfoView or compiler output, never imagined*. In a headless agent workflow,
insert `trace_state` immediately before the tactic of interest and run
`lake env lean Path/To/File.lean`; Lean prints the local hypotheses, target,
and case name. A deliberate `done` is a useful assertion at a point where no
goals should remain: if any do, compilation fails and prints them. Goal
states contain information the tactic script omits (the expression after
simplification, the instantiated types).

```lean
theorem foo (h : a ≤ b) : a + c ≤ b + c := by
  -- ⊢ a + c ≤ b + c
  apply add_le_add_right
  -- ⊢ a ≤ b
  exact h
```

Drafting annotations are scaffolding: keep them while working, then strip
`trace_state`, deliberate failing `done`s, and routine comments. Keep only
comments marking non-obvious states (after a big `simp`, before a witness
choice) in the final proof — the same information belongs in `show` lines
where possible, since those are checked by Lean.

## Declarativity: typed `have` skeletons

ImProver operationalizes readable structure as the ratio of explicitly
typed `have` steps to total tactic invocations. Use it as a *signal*, not a
target (it is trivially gameable by stuffing unused `have`s): a proof whose
spine is explicitly-typed `have`/`suffices`/`calc` statements can be read —
and extended, and repaired — statement-by-statement without replaying
tactics. This is the property that lets a *different* model (or human) pick
up the proof later.

## Sorry skeletons are the multi-agent protocol

The spec-driven decomposition described in the library-design reference is
directly an LLM
workflow: one agent (or one pass) states the target, its lemmas, and their
API as compiling `sorry` stubs; independent agents then discharge
individual sorries with no shared context beyond the file. This is exactly
how PFR ran ~20 human contributors in parallel — the proof assistant
verifies each contribution independently, so contributors need not
understand the whole. Rules:

- Every stub must compile before fan-out (`lake build` on the skeleton).
- A filled sorry must not change any statement — statements are frozen
  interface; if a statement is wrong, that is a design change, surfaced
  rather than silently patched.
- Prefer many small stubs over few large ones: the granularity criterion is
  "one agent can discharge one stub without global context".

## Search by goal shape before deriving a helper

Predictable Mathlib names make a direct guess (`add_le_add_left`,
`Finset.sum_comm`) a useful fast path, but names are weak queries when only
the goal shape is known. Before deriving a helper:

1. State the exact fragment as a scratch `example` with a bare goal.
2. Run `exact?` and `apply?`; for rewrite-shaped goals, also try `rw?`.
3. Search by type pattern (`#find` in a Mathlib scratch file) and search the
   relevant source namespace for the conclusion's operators and types.
4. Only then derive a local helper or propose a new API lemma.

Replace successful search tactics with the named theorem they report in the
final proof. Never claim a Mathlib API gap without showing the failed bare-goal
search and at least one type-pattern or source search; otherwise a re-derived
theorem is evidence of a search failure, not a library gap.

## Automation tactics: draft freely, finalize deliberately

`omega`, `decide`, `norm_num`, `ring`, `positivity`, `gcongr`, and `grind`
are appropriate when the goal genuinely lies in their fragment. Treat a
broad `grind` success as a draft: run `grind?` and prefer its bounded
`grind only [...]` suggestion when that remains readable and measurably
reasonable. `bv_decide` is for fixed-width `BitVec` and Boolean combinatorial
goals, not ordinary `Nat` arithmetic merely described as “u32”; audit its
axioms against the project's trust policy and use `bv_decide?` when a checked
certificate should be persisted.

The failure mode to avoid is using heavyweight closers (`nlinarith`,
`polyrith`, unbounded `grind`/`aesop`, `decide` on large instances) to skip
*structuring* a nontrivial argument: the proof becomes a black box that
breaks opaquely and slowly. If a closer needs hand-fed auxiliary terms to
succeed, that is the signal the argument has structure worth writing out.

# Naming conventions

Mathlib names are computable from statements. This matters doubly for LLMs:
a predictable scheme lets you *guess* the name of the lemma you need
(`add_le_add_left`, `mul_pos`, `isOpen_iUnion`) instead of searching, and
lets you name your own lemmas so others can guess them. Source: the official
[naming guide](https://leanprover-community.github.io/contribute/naming.html).

## Build the name from the conclusion

Translate the symbols of the conclusion via the standard dictionary:

| Symbol / concept | Name fragment |
|------------------|---------------|
| `+` | `add` |
| `*` | `mul` |
| `⁻¹` | `inv` |
| `≤` / `<` | `le` / `lt` |
| `=` / `≠` | `eq` / `ne` |
| `∘` | `comp` |
| `→` (in conclusion structure) | `of` (see below) |
| `↔` | `iff` |
| `¬` | `not` |
| `0` / `1` | `zero` / `one` |

So `a + b = b + a` is `add_comm`; `a * b = b * a` is `mul_comm`;
`a ≤ b → c + a ≤ c + b` involves `add_le_add_left`.

## Hypotheses come after `of`, in statement order

`of` separates the conclusion from the hypotheses; hypotheses are listed in
the order they appear, *not* reversed. `A → B → C` is named `C_of_A_of_B`:

```lean
theorem lt_of_le_of_lt : a ≤ b → b < c → a < c
--      ^conclusion  ^hyp1   ^hyp2
```

## Casing

| Kind | Case | Example |
|------|------|---------|
| Proofs / theorem names | `snake_case` | `add_comm`, `lt_of_le_of_lt` |
| `Prop`s, `Type`s, structures, classes, inductives | `UpperCamelCase` | `Monoid`, `IsOpen`, `Continuous` |
| Other terms of types (functions, instances, fields) | `lowerCamelCase` | `toFun`, `instAddNat` |

When an `UpperCamelCase` name is embedded in a `snake_case` theorem name, it
is referenced in `lowerCamelCase`: a lemma about `IsOpen` is
`isOpen_compl_iff`, a lemma about `IsCompact` is `isCompact_iUnion`.

## Practical guidance

- Name the lemma *after* its statement is final. A renamed hypothesis or
  reordered implication changes the correct name.
- If you cannot derive a name from the statement, the statement is probably
  not in canonical form — check the simp-normal-form conventions first
  (e.g., state with `<` rather than `>`, `x ≠ 0` rather than `¬x = 0` per
  local convention).
- The guide documents exceptions (interval lemmas, historically established
  names, associativity ambiguity); when extending an existing file, imitate
  its local naming before inventing.
- Namespaces carry part of the name: `Nat.add_comm`, `List.map_map`. State
  lemmas about type `T` in namespace `T` so dot-notation (`h.symm`,
  `hf.comp hg`) works.

# Elaboration and reduction cost

Slow proofs and heartbeat timeouts are measurement problems before they are
optimization problems: most reported "regressions" dissolve under the right
probe, and most real ones live in the *shape of a definition*, not in the
tactic script. Evidence here is from a reflection-heavy program-verification
project; the mechanisms are general.

## Measure per-declaration cost, nothing else

- Use `#count_heartbeats in <decl>` (or time an isolated goal) with
  dependencies prebuilt. Build wall-clock misleads twice over: it mixes in
  parallelism and dependency rebuilds, and `lake`'s per-module figure is
  *cumulative* wall-clock, not that module's cost. One "regression" was
  reported as 500–1000×, then 2×, and finally measured at **+1 heartbeat**.
- **Treat every existing `set_option maxHeartbeats` as an unproven claim.**
  Measure by bisection before believing it: budgets get copy-pasted between
  declarations until they carry no information about which proof is actually
  expensive (one file held 82 identical per-lemma overrides; a
  "6.4M-heartbeat monolith" ran at the default budget once restructured).
  Keep overrides scoped per declaration (`set_option maxHeartbeats N in`) and
  only where measured; an unscoped file-level budget hands every later
  declaration in the file an allowance nobody measured for it.
- **Match the probe to what the consumer forces.** `whnf` is lazy: it stops
  at the head constructor, so a pathological definition and its fix can both
  probe at ~3 ms while the tactic's actual `Meta.reduce` costs 3000 ms vs
  5 ms. A lazy probe produces false "unreproducible" verdicts.
- **When a bottleneck resists diagnosis, build a payload-free control**: the
  emptiest input that still exhibits the cost. A body of pure `nop`s costing
  the same as the real body excludes every payload-level hypothesis at once.
  Cost that scales with the *number of steps* rather than the payload points
  at the fold or accumulator, not at the instructions.

## Where reduction cost actually comes from

- **When a goal is closed by `Eq.refl`/`rfl`/`decide`, the kernel replays the
  whole reduction.** Making the *tactic* reduce more cleverly buys nothing;
  only restructuring the proof term or the definition being reduced helps.
  Check which of the two you are optimizing before spending effort.
- **Count reduction paths, not term size.** Cost tracks how many times a
  definition's body mentions its recursive argument: those occurrences
  compose *multiplicatively* along a fold (~kⁿ distinct paths the evaluator
  cache cannot share), while the result term itself stays linear (sharing
  works — for the term). A case built from `List.set`/`eraseIdx`/index
  lookups that mentions the stack 9 times can be 150× the cost of an
  equivalent that destructures once with explicit patterns and rebuilds.
  Diagnose by counting occurrences per case; fix by pattern-matching instead
  of indexing-and-rebuilding.
- **A left-nested `++` on a fold accumulator is exponential** — even when
  everything appended is empty, because each step forces the whole
  accumulated list. Accumulate by reverse-prepending and reverse once at the
  end.
- **Unreduced intermediate terms compound.** Feeding one step's output to the
  next as an unreduced wrapper nests a level per step (~1.8× growth per
  iteration measured). Normalize between steps.
- **Know your kernel-reduction size ceiling.** Closing goals by reflection
  has a steep cost curve (measured: ~11 ms at 6 interpreted instructions,
  ~1.7 s at 28, unbounded past ~44). Past the knee no lemma work helps —
  decompose the goal into smaller units. Measure the curve before blaming
  your lemma set.

## Optimize the definition, keep the semantics

When a definition on the trusted path is too expensive to reduce, do not
rewrite it in place. Keep the readable definition as the reference semantics
and add the fast form beside it with an equality theorem:

```lean
/-- Reference semantics: the readable, obviously-correct form. -/
def execOps (ops : List Op) (s : State) : Option State := ...

/-- Reduction-friendly form (reverse-prepending accumulator). -/
def execOps' (ops : List Op) (s : State) : Option State := ...

theorem execOps'_eq_execOps : execOps' = execOps := ...
```

The equivalence covers every input, including degenerate and failure cases,
so the optimization cannot silently change meaning — and downstream proofs
keep folding over the original, swapping an `unfold` for one `rw`. That is
far cheaper than re-proving a soundness stack against a new shape, and the
intended meaning stays legible. (This is the library-design "statements are
the interface" rule applied to definitions under optimization.)

## Working habits that keep cost visible

- Land performance changes **independently** of functional ones; when a
  bundled pair regresses, the two are indistinguishable and both get
  reverted.
- A changed failure mode is progress: "goal is not an equation" → `whnf`
  timeout → `unsolved goals` is three distinct blockers stacked behind one
  symptom, each fix confirmed by the *category* of the next failure. Decide
  up front what partial success looks like.
- A well-evidenced negative result — "this construct is past the reduction
  ceiling, decompose instead" — is a deliverable that redirects effort;
  record it where the next person will look.

# Tactic proof style

How to structure the inside of a proof. Sources: Mathlib style and PR review
guides, Mathematics in Lean (MIL), Theorem Proving in Lean 4 (TPiL4), and
Massot's ITP 2024 paper on structured proofs. TPiL4's framing: structuring
devices exist because long unstructured tactic sequences "obscure the
structure of the argument" — structure makes proofs "more readable and
robust".

## Skeleton first

Outline the proof with `sorry` (or `_`) justifications, get Lean to accept
the structure, then fill each step. Keeping the skeleton intact is what
yields localized, useful error messages while you work. Filling in the
sorry skeleton from [SKILL.md](../SKILL.md) step 2 yields:

```lean
example (a b c d : ℝ) (h : c = d * a + b) (h' : b = a * d) : c = 2 * a * d := by
  calc
    c = d * a + b     := h
    _ = d * a + a * d := by rw [h']
    _ = 2 * a * d     := by ring
```

## calc replaces rewrite chains

A bare sequence of `rw` steps can only be understood by replaying it in an
editor. When rewrites chain equalities or inequalities, restate the chain as
`calc`: it works for any transitivity-supporting relation (`=`, `≤`, `<`,
`↔`, mixtures), each step discharged by `rw`/`simp`/`ring`/a lemma. Style:
align the relation symbols vertically; left-justify the continuation `_`.

There is no "N rewrites" threshold — the test is whether the intermediate
expressions carry information a reader needs.

## have and suffices

- `have h : X := ...` — forward stepping stone: "we first establish X".
  Intermediate `have`s are the primary structuring device of long proofs.
- `suffices h : X by ...` — backward reduction: "it suffices to show X".
  Use it when the natural narration reduces the goal; you prove the
  reduction first, then the reduced claim.

Always give `have` an explicit statement (`have h : X := ...`, not
`have h := someLemma foo`) when the type is not obvious — the explicitly
typed form is what makes the proof skimmable without an editor.

## Announce goals with show

Open each block of a multi-goal proof with a `show` stating the goal. It is
semantically redundant and structurally essential: MIL — using `show` "makes
the proof easier to read and maintain."

`show` must be honest: if the tactic would actually *change* the goal (up to
more than reducible defeq), use `change` instead. Mathlib's `show` linter
enforces the distinction.

## One focused goal at a time

Every tactic that produces multiple goals is followed by one `·`-focused,
indented block per goal:

```lean
  apply le_antisymm
  · show min a b ≤ min b a
    ...
  · show min b a ≤ min a b
    ...
```

Never operate on goal 2 while goal 1 is open — that couples the proof to
Lean's goal ordering, the classic source of fragility. Enforced by the
`multiGoal` linter. `<;>` and `all_goals` are fine when one tactic
uniformly closes all goals; named `case` blocks are a permitted alternative
to `·` when the case names add information.

## One tactic invocation per line, in general

Mathlib's
[style guide](https://leanprover-community.github.io/contribute/style.html)
recommends one tactic invocation per line **in general**, except when a proof
that closes the goal fits entirely on one line. It also permits short sequences
that express one mathematical idea, while preferring newlines. Apply this as
readability guidance, not as a parser-like rule: do not split a clear terminal
`by simpa using h` merely to satisfy a slogan, and do not compress unrelated
state-changing tactics onto one line. This is separate from goal focusing;
`linter.style.multiGoal` protects goal ownership, while line layout is reviewed
qualitatively.

## simp discipline

- **Terminal** `simp` (closes the goal): leave it as `simp` — do *not*
  squeeze it into `simp only [...]`. A squeezed terminal call names many
  lemmas, breaks when any is renamed, and buries the one that matters.
- **Non-terminal** `simp` (leaves a goal for later tactics): squeeze it to
  `simp only [...]` so the intermediate goal is stable; a non-terminal bare
  `simp` couples every following tactic to the current simp set.
- **Whether a `simp` is terminal is a property of the declaration, not the
  idiom.** Three sibling lemmas can look identical while one has a trailing
  `rw` that makes its `simp` non-terminal. Read each proof to the end before
  classifying; "the previous two were terminal" is not evidence about the
  third.
- **Derive every `simp only` list with `simp?` run at that site.** Lists do
  not transfer between look-alike goals — near-identical copy-pasted call
  sites routinely need different lists (one needs `or_self`, the next
  doesn't; one goal's numerals are already reduced, the next's aren't). The
  cost of probing each site is seconds; the cost of assuming transfer is a
  broken proof that looks like a typo.
- Adding a `@[simp]` lemma: its left-hand side must itself be in
  simp-normal form (checked by the `simpNF` linter).
- **One canonical spelling per domain constant — including numerals.**
  `u32Max`, `2 ^ 32`, and `4294967296` are one value in three spellings; if
  the definition, the API lemmas, and the normalized goal each use a
  different one, nothing matches, no rewrite fires, and simp burns its whole
  budget failing. Stronger form: prefer LHS patterns keyed on *structure*
  (a function application over operands) with no numeral in the pattern at
  all — those cannot miss for spelling reasons.
- **`simp`'s default `maxDischargeDepth = 2` silently truncates chained side
  conditions.** A conditional rewrite whose hypothesis is discharged by
  another conditional rewrite (and so on) stops firing past depth 2 — no
  diagnostic, just a goal that does not close and a burned heartbeat budget.
  If a conditional lemma provably applies but never fires on deeper
  instances, raise `maxDischargeDepth` before suspecting the lemma.
- **Traversal order can make a lemma unreachable.** simp rewrites subterms
  first, so a fusion lemma about `f (g x)` never fires if `g x` has already
  been rewritten away. Register such lemmas pre-order with `@[simp ↓]`.
  Symptom: a lemma that is obviously applicable, provably true, and never
  used.
- **"Redundant `@[simp]`" and "useful lemma" are independent.** When
  `simpNF` reports the default set already proves a lemma, drop the global
  `@[simp]` but consider keeping its membership in a scoped simp set —
  `simp only [myScopedSet]` does not include the default set, so the entry
  still does work there. Relatedly, a lemma reached only through
  `simp [mySet]` has zero by-name references and is fully live: check
  attribute consumption before deleting "dead" lemmas.

## Structure at the decisions, terseness at the routine

Massot's taxonomy: proofs alternate *safe, reversible* steps (introducing a
variable, destructuring an existential — no initiative required) with
*risky, irreversible* steps (choosing a witness, specializing a universal,
picking an induction). Spend the structural markers — `show`, explicitly
typed `have`, a comment — at the risky steps, where the reader needs to see
the decision. Routine steps can stay terse.

## Golfing

Mathlib review policy: "code golfing is okay as long as it doesn't sacrifice
readability, although golfing trivial results is generally okay." Shorten a
proof only when the short form reads at least as well; a trivial result
closed by `simp`/`omega`/`decide` needs no ceremony. Never golf away the
skeleton of a nontrivial argument.

## When review says "split it"

Mathlib's review guide: "Long standalone proofs are frequently an indication
that there is a worthwhile refactor lurking close at hand." The criterion is
qualitative ("long and unwieldy"); the only numeric threshold in the guide
(1000 lines) is for files. Apply the extraction ladder from
[SKILL.md](../SKILL.md); when
unsure, attempt the extraction — a fragment with a clean statement wanted to
be a lemma.

# Writing tactics and metaprograms

## Contents

- [Choose the smallest extension point](#choose-the-smallest-extension-point)
- [Define the tactic contract](#define-the-tactic-contract)
- [Normalize inputs deliberately](#normalize-inputs-deliberately)
- [Make speculative state transactional](#make-speculative-state-transactional)
- [Make failures local and actionable](#make-failures-local-and-actionable)
- [Bound proof search](#bound-proof-search)
- [Build tracing in from the start](#build-tracing-in-from-the-start)
- [Generate syntax and declarations safely](#generate-syntax-and-declarations-safely)
- [Structure tactic code for change](#structure-tactic-code-for-change)
- [Test the failure surface](#test-the-failure-surface)
- [Review checklist](#review-checklist)
- [Research sources](#research-sources)

Custom tactics, macros, simprocs, and elaborators have distinctive failure modes. A bug can
surface much later as a kernel error, silently leave automation in a partial state, or turn a
fast failure into an unbounded search. Design the extension so invalid states are hard to create
and every failure is attributable to one stage.

## Choose the smallest extension point

| Need | Prefer | Safeguard |
|------|--------|-----------|
| Syntax-only expansion | hygienic `macro` | preserve syntax refs; avoid `unhygienic` |
| One local simplification step | simp lemma, `simproc`, or `dsimproc` | return `.continue` when inapplicable |
| Reusable goal-directed search | a scoped Aesop rule set | classify rules by semantic safety |
| Custom input elaboration or goal mutation | tactic elaborator | define state, failure, and goal-list contracts |
| Repeated low-level operation | typed `MetaM` helper | test it independently of parser syntax |

Use ordinary lemmas before meta code. Recent Mathlib guidance treats simprocs as small steps in
a larger simplification algorithm, not as general-purpose automation. Prefer `Qq` typed
quotations for expression matching and proof construction when practical: raw `Expr` APIs allow
ill-typed proof terms to exist until a later check.

## Define the tactic contract

Before implementation, write down four observable outcomes:

1. **Applicable and successful:** which goals are closed or replaced, and in what order?
2. **Inapplicable:** is this an expected rule miss or a user-facing tactic error?
3. **Malformed input:** which syntax range receives which diagnostic?
4. **Resource exhaustion or invariant failure:** which error escapes, and what trace identifies
   the last completed phase?

An Aesop rule or simproc should normally fail softly when its pattern does not match. A tactic the
user invoked directly should fail loudly when the target has the wrong shape. Never convert an
internal invariant violation into a successful no-op.

Define success from the resulting goals, not from the helper's return value. A finishing tactic
must leave no owned subgoals; a normalizer may leave one demonstrably changed goal. Tactics such as
`simp` can return successfully after changing but not closing a goal, so wrap them in a terminal
combinator when “finish” is part of the interface.

Preserve goals the tactic does not own. Use `liftMetaTactic` or `replaceMainGoal` for a tactic that
transforms only the main goal; do not rebuild the whole goal list with `setGoals` unless reordering
all goals is part of the documented contract.

## Normalize inputs deliberately

- **Enter the goal context.** Wrap tactic entry points in `withMainContext`, and run lower-level
  goal operations inside `goal.withContext`. Operations such as `inferType` and `isDefEq` need the
  correct local context; otherwise dependent local hypotheses become unknown free variables.
- **Do not pattern-match a stale expression.** Use `instantiateMVars` before structural matching
  when assigned metavariables may remain in the expression. Use `cleanupAnnotations` when wrapper
  annotations are irrelevant, or `whnfR` when matching should unfold reducible definitions.
  Choose the weakest normalization that matches the tactic's stated semantics.
- **State the transparency mode.** A tactic that happens to work under an ambient transparency
  setting is not stable. Pass the intended mode to matching, reduction, and unification helpers.
- **Finish elaboration checkpoints.** After elaborating internal terms, use
  `synthesizeSyntheticMVarsNoPostponing` or an appropriate `withSynthesize` boundary. Otherwise a
  tactic can report success with pending coercion, typeclass, tactic, or postponed metavariables.
- **Assign only after a type check.** Raw `MVarId.assign` skips occurs, scope, and type checks. Use
  `assignIfDefeq`, `isDefEq` against the metavariable type, or an elaborator such as
  `elabTermEnsuringType` that performs the check before assignment.
- **Prefer optional destructors over panics.** A shape mismatch is ordinary for a rule. Prefer
  `foo?`, `let some`, and `let_expr ... | return .continue` over `foo!` and unreachable branches
  for inputs controlled by users or other tactics.

## Make speculative state transactional

Unification and definitional equality checks can assign metavariables even when they look like
queries. Treat every speculative branch as a transaction.

- In `MetaM`, raw `try`/`catch` does **not** restore state. Use `observing?` for an optional result,
  `withoutModifyingState` for a read-only probe, or `commitIfNoEx` before a catch-and-fallback path.
- In `TacticM`, exception handling backtracks tactic state. Do not expect the catch branch to see
  intermediate assignments or messages from the failed branch. If a diagnostic needs that state,
  collect it before failing or perform the narrow probe in `MetaM`/`TermElabM` with an explicit
  state contract.
- Keep recovery scopes small. Wrap the one expected-to-fail probe, not the entire tactic. A broad
  catch can misclassify heartbeat exhaustion, recursion limits, or implementation bugs as “rule
  did not apply.”
- Do not assume rollback erases everything. Caches, trace messages, and the global name generator
  are intentionally not fully backtracked. Traces should identify attempts without relying on
  generated names being reused.

## Make failures local and actionable

- **Disable recovery for generated tactic syntax.** If tactic code calls `evalTactic` on syntax it
  generated and expects to be correct, wrap the call in `withoutRecover`. Interactive recovery may
  otherwise log an error, insert `sorry`, and let the outer tactic appear to succeed.
- **Attach errors to the narrowest user syntax.** Use `withRef`/`withRef?` around parsing and
  elaboration of an argument. Use `throwTacticEx` for a goal-specific failure so the diagnostic
  includes the tactic name and current goal.
- **Use `MessageData`, not pre-rendered strings, for Lean expressions.** `m!"{expr}"` delaborates in
  context and remains readable; raw AST formatting usually hides the actual problem.
- **Name the failed phase and expectation.** “Expected a target of the form `P ∧ Q`; got …” is
  repairable. “Tactic failed” is not. Distinguish input validation, normalization, candidate
  selection, proof construction, metavariable synthesis, and final assignment.
- **Do not swallow resource failures.** If Lean cannot reliably distinguish an expected miss from
  a timeout in a broad handler, redesign the probe to return `Option` on ordinary misses and reserve
  exceptions for abnormal failures.

## Bound proof search

Every loop needs a progress argument and a machine-checkable limit. Heartbeats alone are not a
complete guard: a tactic can grow goals dramatically before hitting them, and some low-allocation
loops are poor heartbeat clients.

- Bound iterations, rule applications, recursion depth, generated candidates, and—where growth is
  possible—expression or goal size. Report which bound fired and include counters in the trace.
- Make normalization loops prove progress with a decreasing or non-repeating measure. A rule that
  “succeeds” without changing the normalized state must not restart the loop.
- In Aesop, mark a rule `safe` only if it preserves provability relative to the entire active rule
  set and is non-branching. A convenient rule is not automatically safe. Keep speculative choices
  unsafe so search can backtrack.
- Scope expensive or aggressive rules to named rule sets. Do not put a domain-specific finishing
  tactic in the global default set where it will run on every unrelated goal.
- Give optional fast paths a small local budget. A fail-soft fast path that consumes the ambient
  budget before falling back merely changes a quick failure into a slow one.
- When search can emit a deterministic script (`aesop?`, `simp?`, or a custom suggestion), validate
  the emitted script before replacing the search call. Metavariable dependencies can make apparently
  harmless tactic reorderings change behavior.

## Build tracing in from the start

Register a project-specific trace hierarchy with `registerTraceClass`; use `trace[...]` for leaves
and `withTraceNode` for nested phases. Follow Lean's trace design rules:

- Put the outcome in the collapsed top-level node.
- Emit one child per phase or candidate decision, with rejection reasons only at deeper levels.
- Record the input goal, normalized goal, active options/rule set, candidates tried, counters, and
  final subgoals or proof term. Keep the default view concise.
- Use the caller's syntax ref so messages and trace nodes navigate to the relevant token.
- Add a separate statistics trace for iteration counts, cache hits, goal size, and time. Do not make
  users infer a performance failure from thousands of low-level messages.

Keep `dbg_trace`, broad `pp.all`, and profiler options in local reproductions, not committed proof
files. For proof-construction bugs, inspect what automation produced with `show_term`, `by?`, an
Aesop proof trace, or the tactic's own final-proof trace. This separates “wrong search decision”
from “right decision, malformed proof term.”

## Generate syntax and declarations safely

- Prefer hygienic quotations and antiquotations. Use `unhygienic` only when name capture is the
  explicit interface, and cover that behavior with tests.
- Preserve source locations with quotations, `withRef`, `mkIdentFrom`, or `mkIdentFromRef`.
  Synthetic syntax whose ref spans a whole command produces unusable diagnostics and hover data.
- Treat names as structured data. `` `foo ++ `bar `` is the dotted name `foo.bar`, not `foo_bar`.
  Build atomic generated names with `Name.mkSimple` on an explicitly constructed string.
- Macro-generate repetitive lemma families, but verify the migration mechanically. For every old
  statement, compile an `example` proving that exact statement with the generated declaration under
  the calling convention downstream code uses. Also assert the expected declarations exist by name.

## Structure tactic code for change

- Separate parsing, normalization, search, proof construction, and goal mutation. Pure or narrowly
  stateful helpers are easier to test than one elaborator that performs every phase.
- Extract shared cores from near-duplicate tactic families. Two ladders differing only in “recurse”
  versus “return” will drift when only one receives a new fast path or guard.
- When two canonical variants are plausible, build the full proof suite both ways and record the
  result near the decision: which input failed, which invariant differed, and the measured cost.
- An identity function at deliberate call sites may be a reserved normalization hook. Before
  deleting it, decide whether the call sites mark a stable phase boundary; if so, document the
  intended future invariant rather than leaving an unexplained no-op.
- Verify dependency trigger conditions from source. “Runs only on failure” versus “runs on every
  call” changes an optimization from free to pay-per-call.

## Test the failure surface

Test behavior, not private helper order. Every expected failure path needs a test that demonstrates
both the diagnostic and the absence of state leakage.

| Case | Assertion |
|------|-----------|
| Dependent local context | local variables remain in scope and generated terms type-check |
| Wrong target or malformed syntax | direct tactic fails at the relevant token with an actionable message |
| Rule or simproc miss | reports “not applicable” to its caller and leaves expression/state unchanged |
| Assigned metavariables, annotations, abbreviations | matching behavior follows the documented normalization |
| Multiple active goals | only owned goals change; remaining goal order is preserved |
| Pending synthetic metavariables | tactic completes synthesis or fails before reporting success |
| Non-terminal helper success | a finisher backtracks or fails if owned subgoals remain |
| Speculative branch mutates then fails | fallback observes the original metavariable and goal state |
| Looping or goal-growing rule | explicit bound fires and trace reports the responsible rule and counters |
| Generated proof or declaration family | exact old statements compile; negative fixtures are rejected |
| Trace disabled/enabled | default output stays quiet; trace identifies the failed phase and source ref |

Use `fail_if_success`, `guard_target`, `#check_failure`, and `#guard_msgs` where appropriate. Include
at least one known-trigger fixture: a checker or rule suite that is only tested on clean inputs can
silently match zero items forever.

## Review checklist

- [ ] The extension point is no more powerful than the job requires.
- [ ] Applicable, inapplicable, malformed, and exhausted outcomes are distinct.
- [ ] Local context, normalization, transparency, and synthesis boundaries are explicit.
- [ ] Every metavariable assignment is type-checked.
- [ ] Every speculative mutation has rollback semantics and a narrow recovery scope.
- [ ] Generated `evalTactic` syntax runs under `withoutRecover`.
- [ ] Errors carry a source ref, tactic name, goal, phase, and expected shape.
- [ ] Search has progress checks, explicit bounds, and scoped rules.
- [ ] Opt-in traces show outcomes, decisions, counters, and final proof/subgoals.
- [ ] Negative, state-leakage, multiple-goal, and pathological-growth tests exist.

## Research sources

Community articles and guides:

- Yaël Dillies and Paul Lezeau,
  [Fantastic Simprocs and How to Write Them](https://leanprover-community.github.io/blog/posts/simprocs-tutorial/)
- Yaël Dillies and Paul Lezeau,
  [Simp, made simple](https://leanprover-community.github.io/blog/posts/simp-made-simple/)
- Mathlib community,
  [Metaprogramming gotchas](https://github.com/leanprover-community/mathlib4/wiki/Metaprogramming-gotchas)
- Lean community,
  [Metaprogramming in Lean 4: `MetaM`](https://leanprover-community.github.io/lean4-metaprogramming-book/main/04_metam.html)
  and [Tactics](https://leanprover-community.github.io/lean4-metaprogramming-book/main/09_tactics.html)
- Lean API documentation,
  [trace messages and trace-class design](https://leanprover-community.github.io/mathlib4_docs/Lean/Util/Trace.html)

Forum discussions:

- Kyle Miller on
  [`withoutRecover` for generated `evalTactic` code](https://leanprover-community.github.io/archive/stream/217875-Is-there-code-for-X%3F/topic/pretty.20print.20of.20Nat.html)
- Eric Wieser and Kyle Miller on
  [broad exception handling in tactics](https://leanprover-community.github.io/archive/stream/287929-mathlib4/topic/bug.20in.20convert.html)
- Jannis Limperg and Sebastian Ullrich on
  [diagnosing unbounded Aesop goal growth](https://leanprover-community.github.io/archive/stream/270676-lean4/topic/aesop.20gets.20stuck.html)
- Jannis Limperg on
  [Aesop's safe-rule and debugging semantics](https://leanprover-community.github.io/archive/stream/270676-lean4/topic/Aesop.20dev.20updates.html)

Papers by Lean tactic and metaprogramming developers:

- Jannis Limperg and Asta Halkjær From,
  [Aesop: White-Box Best-First Proof Search for Lean](https://people.compute.dtu.dk/ahfrom/aesop-camera-ready.pdf)
- Jannis Limperg,
  [Tactic Script Optimisation for Aesop](https://doi.org/10.1145/3703595.3705877)
- Sebastian Ullrich and Leonardo de Moura,
  [Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages](https://arxiv.org/abs/2001.10490)
- Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura,
  [A Metaprogramming Framework for Formal Verification](https://lean-lang.org/papers/tactic.pdf)