/lean4

Common Compilation Errors in Lean 4

This reference provides detailed explanations and fixes for the most common compilation errors encountered in Lean 4 theorem proving.

Quick Reference Table

⚡ WORKING WITH SUB-σ-ALGEBRAS?

If you're defining multiple MeasurableSpace instances (sub-σ-algebras), STOP and read this first:

📚 instance-pollution.md - Essential guide to prevent:

• Subtle bugs: Lean picks wrong instance (even from outer scopes!)
• Timeout errors: 500k+ heartbeat explosions
• Cryptic errors: "synthesized: m, inferred: inst✝⁴"

Quick fix: Pin ambient instance BEFORE defining sub-σ-algebras (see instance-pollution.md for details).

Detailed Error Explanations

1. Failed to Synthesize Instance

Full error message:

failed to synthesize instance
  IsProbabilityMeasure μ

What it means: Lean cannot automatically infer the required type class instance.

Common scenarios:

• Working with sub-σ-algebras: m ≤ m₀ but Lean can't infer instances on m
• Trimmed measures: check whether synthesis already succeeds — given [IsFiniteMeasure μ], IsFiniteMeasure (μ.trim hm) is a Mathlib instance now, and SigmaFinite (μ.trim hm) follows from it ([SigmaFinite μ] alone is not enough)
• Conditional expectations requiring multiple measure properties

Solutions:

Pattern 1: Explicit instance declaration (plain have — it registers the instance; haveI only inlines the value, which is irrelevant in a proof and is flagged by Mathlib's haveI/letI linter)

have : IsProbabilityMeasure μ := ⟨measure_univ⟩
-- Check first whether synthesis already succeeds: with `[IsFiniteMeasure μ]`,
-- `IsFiniteMeasure (μ.trim hm)` is a Mathlib instance (`isFiniteMeasure_trim`)
-- and `SigmaFinite (μ.trim hm)` follows from it. Freeze only if it helps:
have : SigmaFinite (μ.trim hm) := inferInstance

Pattern 2: Using Fact for inequalities

have h_le : m ≤ m₀ := ...
have : Fact (m ≤ m₀) := ⟨h_le⟩

Pattern 3: Explicit instance passing

@condExp Ω ℝ m₀ m (by exact inst) μ (by exact hm) f

Pattern 4: Exclude unwanted section variables

-- When section has `variable [MeasurableSpace Ω]` but lemma doesn't need it
omit [MeasurableSpace Ω] in
/-- Docstring for the lemma -/
lemma my_lemma : Statement := by
  proof

• Line order matters: omit … in before the docstring — see § 21 for the rule and the error it produces
• Common when section variables cause unwanted instance requirements
• Can omit multiple: omit [inst1] [inst2] in

⚡ CRITICAL for sub-σ-algebras: If working with multiple MeasurableSpace instances, read instance-pollution.md FIRST to avoid subtle bugs and timeout errors!

For deep patterns with sub-σ-algebras, conditional expectation, and measure theory type class issues, see: measure-theory.md

Debug with:

set_option trace.Meta.synthInstance true in
theorem my_theorem : Goal := by
  infer_instance

2. Typeclass Synthesis Timeout (and the separate maxRecDepth limit)

Full error message:

(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached

What it means: Type class synthesis is stuck in a loop or the search is too complex. This is synthInstance.maxHeartbeats, a search budget. The differently worded maximum recursion depth has been reached is maxRecDepth, an elaboration/whnf recursion limit — raise it with set_option maxRecDepth 2000 in or restructure the term; a bigger synthesis budget does nothing for it.

Common causes:

• Circular instance dependencies
• Very deep instance search trees
• Ambiguous instances competing

Solutions:

Solution 1: Provide instance manually

let m0 : MeasurableSpace Ω := m₀  -- Freeze (pin) the instance; plain `let` registers it
-- Now Lean won't search

Solution 2: Increase search limit

set_option synthInstance.maxHeartbeats 40000 in
theorem my_theorem : Goal := ...

Solution 3: Check for instance loops

-- ❌ WRONG: Creates loop
instance [Foo A] : Bar A := ...
instance [Bar A] : Foo A := ...

-- ✅ CORRECT: One-directional
instance [Foo A] : Bar A := ...

3. Type Mismatch

Full error message:

type mismatch
  x
has type
  ℕ
but is expected to have type
  ℝ

What it means: The term's type doesn't match what's expected.

Common scenarios:

• Natural number used where real number expected
• Integer used where rational expected
• General coercion needed

Solutions:

Pattern 1: Explicit coercion

-- Natural to real
(n : ℝ)  -- Preferred
↑n       -- Alternative

-- Integer to real
(z : ℝ)

-- Custom coercion
⟨x, hx⟩ : {x : ℝ // x > 0}

Pattern 2: Check actual types

#check x        -- See current type
#check (x : ℝ)  -- Verify coercion works

Pattern 3: Function application

-- If f : ℝ → ℝ and n : ℕ
f ↑n    -- Apply after coercion
f (n : ℝ)  -- Explicit

Pattern 4: Bypass coercion unification with calc

When automatic coercion (π/6 : Real.Angle) won't unify with explicit ((π/6 : ℝ) : Real.Angle), use calc chain with coercion-free middle steps:

calc ((Real.pi / 6 : ℝ) : Real.Angle)
    = ∠ A C H := by rw [← h_angle]  -- Explicit coercion matches helper signature
  _ = ∠ A C B := by simp [h_eq]      -- Pure angle equality (no coercion!)
  _ = ((4 * Real.pi / 9 : ℝ) : Real.Angle) := by rw [angle_ACB]

4. Tactic 'exact' Failed

Full error message:

tactic 'exact' failed, type mismatch
  term
has type
  A → B
but is expected to have type
  ∀ x, A x → B x

What it means: The term's type is close but not exactly the goal type.

Solutions:

Solution 1: Use apply instead

-- exact doesn't work but apply might
apply my_lemma
-- Leaves subgoals to fill

Solution 2: Restructure term

-- Wrong order
exact ⟨h.1, h.2⟩  -- Type mismatch

-- Correct order
exact ⟨h.2, h.1⟩  -- Works

Solution 3: Add intermediate steps

-- Instead of: exact complex_term
have h1 := part1
have h2 := part2
exact ⟨h1, h2⟩

5. Unknown Identifier (Missing Tactic or Namespace Open)

Full error message:

unknown identifier 'ring'
unknown identifier 'Tendsto'

What it means: Tactic not imported OR namespace not opened.

Local variables: for a local variable that was present earlier, inspect how the context changed; rintro … rfl or subst may have eliminated it. See the rintro … rfl pitfall in tactic-patterns.md.

Cause 1: Missing tactic import

Common missing imports:

import Mathlib.Tactic.Ring          -- ring, ring_nf
import Mathlib.Tactic.Linarith      -- linarith, nlinarith
import Mathlib.Tactic.FieldSimp     -- field_simp
import Mathlib.Tactic.Continuity    -- continuity
import Mathlib.Tactic.Measurability -- measurability
import Mathlib.Tactic.Positivity    -- positivity

Quick fix:

1. See error for tactic name
2. Add import Mathlib.Tactic.TacticName
3. Rebuild

Cause 2: Missing open declarations

Names like Tendsto and atTop live in the Filter namespace. Without opening it, Lean cannot resolve them:

-- ❌ WRONG: bare identifiers without open
have h : Tendsto f atTop (𝓝 x) := ...

-- ✅ CORRECT: open the relevant namespaces
open Filter Topology in
have h : Tendsto f atTop (𝓝 x) := ...

Alternatively, you can fully qualify the names (Filter.Tendsto, Filter.atTop), but open Filter Topology is the standard mathlib practice.

6. Equation Compiler Failed (Termination)

Full error message:

fail to show termination for
  my_recursive_function
with errors
  ...

What it means: Lean can't automatically prove the function terminates.

Solutions:

Pattern 1: Add termination_by clause

def my_rec (n : ℕ) : ℕ :=
  if n = 0 then 0
  else my_rec (n - 1)
termination_by n  -- Decreasing argument

Pattern 2: Well-founded recursion

def my_rec (l : List α) : Result :=
  match l with
  | [] => base_case
  | h :: t => combine h (my_rec t)
termination_by l.length

Pattern 3: Use sorry for termination proof

def my_rec (x : X) : Y := ...
termination_by measure_func x
decreasing_by sorry  -- TODO: Prove later

7. Unsolved Goals (Nat.pos_of_ne_zero and Arithmetic)

Full error message:

unsolved goals
h : m ≠ 0
h2 : (4 : ℝ) / ε ≤ ↑m
⊢ False

What it means: After introducing a contradiction hypothesis, the goal is False but the tactic can't derive the contradiction.

Common scenario: Proving m > 0 from m ≠ 0 and some bound, but norm_num fails because the expressions are symbolic (not concrete numbers).

Why norm_num fails:

• norm_num works on concrete numerical expressions (like 2 + 2 = 4)
• When you have symbolic variables like 4/ε, norm_num can't evaluate them
• After rw [h] where h : m = 0, you get 4/ε ≤ 0, but norm_num can't derive False from this

Solution: Use simp to eliminate variables, then linarith

-- ❌ WRONG: norm_num can't solve symbolic arithmetic
have hm_pos' : m > 0 := Nat.pos_of_ne_zero (by
  intro h
  rw [h] at h2  -- Now h2 : 4/ε ≤ 0
  norm_num at h2  -- FAILS: can't derive False because 4/ε is symbolic
  )
-- Error: unsolved goals ⊢ False

-- ✅ CORRECT: simp eliminates the variable, then linarith
have hm_pos' : m > 0 := Nat.pos_of_ne_zero (by
  intro h
  simp [h] at h2  -- Now h2 : 4/ε ≤ 0 AND we eliminated m entirely
  have : (4 : ℝ) / ε > 0 := by positivity  -- Explicit positivity proof
  linarith)  -- Can now derive contradiction: 0 < 4/ε ≤ 0

Key insight:

• norm_num = numerical normalization (concrete numbers)
• simp = simplification (eliminates variables, unfolds definitions)
• linarith = linear arithmetic solver (works with inequalities and symbolic expressions)

General pattern for contradiction proofs:

1. simp [hypothesis] to eliminate the contradictory assumption
2. Establish any needed positivity facts with positivity
3. linarith to derive the contradiction from inequalities

When to use each tactic:

• norm_num: Concrete arithmetic (2 + 2 = 4, 7 < 10)
• simp: Simplify using hypotheses and definitions
• linarith: Linear inequalities with variables (a + b ≤ c, x > 0 → x + 1 > 0)
• omega: Integer linear arithmetic (works on ℕ and ℤ)

8. Unexpected Token/Identifier in Proof (Section Doc Comments)

Full error message:

unexpected identifier; expected command
unexpected token 'have'; expected command

What it means: Section doc comments /-! ... -/ in tactic mode can terminate proof parsing.

CRITICAL: Section doc comments terminate proof context, causing everything after to be interpreted as top-level declarations.

-- ❌ WRONG: Section comments break proof
lemma my_proof := by
  classical
  set mW := ... with hmW

  /-! ### Step 0: documentation -/

  set φp := ... with hφp  -- ERROR: unexpected identifier
  have h := ...           -- ERROR: unexpected token 'have'

-- ✅ CORRECT: Use regular comments
lemma my_proof := by
  classical
  set mW := ... with hmW
  -- Step 0: documentation
  set φp := ... with hφp  -- ✓ Works
  have h := ...           -- ✓ Works

Best practice: Use -- for in-proof comments, reserve /-! -/ for top-level documentation only.

9. Variable Shadowing in Lambda

Full error message:

type mismatch
  a
has type
  Set ℝ≥0∞
but is expected to have type
  α

What it means: Lambda variable shadows outer variable, causing type confusion.

-- ❌ WRONG: 'a' in lambda shadows outer 'a'
have h_sp_le : ∀ n a, (sp n a) ≤ φp a := by
  intro n a
  have := SimpleFunc.iSup_eapprox_apply
    (fun a ↦ ENNReal.ofReal (max (φ a) 0))  -- 'a' shadows!
    ... a  -- ERROR: which 'a'?

-- ✅ CORRECT: Rename lambda variable or add type annotation
have h_sp_le : ∀ n a, (sp n a) ≤ φp a := by
  intro n a
  have := SimpleFunc.iSup_eapprox_apply
    (fun (x : α) ↦ ENNReal.ofReal (max (φ x) 0))
    ... a  -- ✓ Clear: outer 'a'

Prevention: Use different variable names in nested lambdas or add explicit type annotations.

10. No Goals After Tactic

Full error message:

no goals to be solved

What it means: Previous tactic already completed the proof, but another tactic remains.

-- ❌ WRONG: simp already solved goal
have hφp_nn : ∀ a, 0 ≤ φp a := by
  intro a
  simp [φp]
  exact le_max_right _ _  -- ERROR: no goals left

-- ✅ CORRECT: Remove redundant tactic
have hφp_nn : ∀ a, 0 ≤ φp a := by
  intro a
  simp [φp]  -- ✓ simp completes proof

Debug: Check goal state after each tactic. If "no goals" appears, proof is done.

Quick Debug Workflow

When encountering any error:

1. Read error location carefully - Often points to exact issue
2. Use #check - Verify types of all terms involved
3. Simplify - Try to create minimal example that fails
4. Search mathlib - Error might be documented in lemma comments
5. Ask Zulip - Lean community is very helpful

Quick Checklist for "Unexpected" Errors in Proofs

When facing "unexpected identifier/token" in long proofs:

1. ☐ Search for /-! ... -/ section comments → replace with --
2. ☐ Check for bare identifiers (Tendsto, atTop) → open Filter Topology
3. ☐ Look for lambda shadowing → rename variables or add type annotations
4. ☐ Check for "no goals" after simp → remove redundant tactics
5. ☐ For section variables + explicit params → rely on section, use (by infer_instance)
6. ☐ For sub-σ-algebra work → ensure hmW_le : mW ≤ _ proof exists

Additional Common Errors

11. Dot Notation Namespace Confusion

Error message:

type mismatch
  expected Filter
  got Measure

What it means: You're using dot notation for a lemma name that conflicts with a type constructor.

Example:

-- ❌ WRONG: Interpreted as EventuallyEq constructor call
have := h.EventuallyEq.comp_measurePreserving
--        ^ EventuallyEq constructor called with μ as first argument
--          Expected Filter but got Measure

Solution: Use snake_case standalone names instead of dot notation:

-- ✅ CORRECT: Call the lemma function
have := EventuallyEq.comp_measurePreserving h ...

Pattern: If you see type errors where:

• A Measure is expected to be a Filter
• A Set is expected to be a different type
• "Expected X but got Y" for completely unrelated types

Check if you're using dot notation for a lemma that shares a name with a type constructor.

Rule: For private helper lemmas extending common type names (EventuallyEq, Tendsto, Continuous, etc.), use standalone function call syntax, not dot notation.

12. Numerals in Propositional Contexts

Error message:

numerals are data but expected type is Prop

What it means: You're passing a value (numeral) where a proof term is expected.

Example:

-- ❌ WRONG: 1 is a numeral (data), not a proof
have := h1.atTop_add 1
--                    ^ Expected: Tendsto proof
--                      Got: numeral 1

Solution: For constant function limits, use tendsto_const_nhds:

-- ✅ CORRECT: Pass a proof term
have := h1.atTop_add (tendsto_const_nhds : Tendsto (fun _ ↦ (1 : ℝ)) atTop (nhds 1))

Pattern: Functions like atTop_add work on limits and need proof terms:

• Tendsto f atTop (nhds a) ← This is a Prop (needs proof)
• 1 ← This is data (ℕ or ℝ)

Common fixes:

-- For constant functions
tendsto_const_nhds : Tendsto (fun _ ↦ c) filter (nhds c)

-- For simple expressions
use lemmas like Filter.tendsto_id, Filter.tendsto_const_pure

13. Error Location Can Be Misleading

Problem: Lean reports errors where elaboration fails, not always where the mistake is.

Example:

error: type mismatch at line 4238

But the actual mistake is at line 4231.

Why: Elaborator processes code sequentially and reports failure at the point where it can't continue, which may be several lines after the actual error.

Strategy:

When investigating an error:

1. Read 5-10 lines before the reported location
2. Look for recent changes (especially new let bindings, have statements, or tactic calls)
3. Check for missing hypotheses or incorrect variable names
4. Verify that all previous lines actually compile in isolation

Example workflow:

-- Error reported at line 4238
-- Start reading from line 4228-4230

-- Line 4231: Ah! Wrong variable name here
let μX := pathLaw μ X  -- Should be Y not X

-- Lines 4232-4237: These all assumed μX was correct
-- Line 4238: Where elaboration finally failed

Pattern: The mistake is often in:

• Most recent let or have before error (wrong RHS)
• Most recent tactic (applied wrong lemma)
• Missing hypothesis from 2-5 lines before

Don't: Assume the error line is where you need to fix. Do: Trace backwards from error to find the root cause.

Two named instances of this: a universe error reported at an argument when the cause is a bare : Type result annotation (§ 20), and unexpected token 'omit' reported at a docstring when the cause is the line order below it (§ 21).

14. Alpha/Beta-Equivalence Issues (Binder Mismatches)

Problem: Lean fails to match expressions because binder names differ (α-equivalence) or beta-redexes aren't reduced.

Error message:

tactic 'simp' failed
  binder x doesn't match goal's binder ω

Example failure:

have h := integral_condExp (f := fun ω ↦ μ[g|m] ω * ξ ω)
-- h : ∫ (x : Ω), F x ∂μ = ∫ (x : Ω), μ[F|m] x ∂μ
-- Goal: ∫ (ω : Ω), μ[g|m] ω * ξ ω ∂μ = ...

simpa using h.symm  -- Error: binder x ≠ binder ω

Why it fails: Lean doesn't automatically recognize that fun x ↦ F x and fun ω ↦ F ω are the same when comparing goal to hypothesis.

Solution: Use set ... with pattern to name expression once

-- Name the integrand once and for all
set F : Ω → ℝ := fun ω ↦ μ[g | m] ω * ξ ω with hF

-- Apply lemma to named function F
have h_goal :
    ∫ (ω : Ω), μ[g | m] ω * ξ ω ∂μ
  = ∫ (ω : Ω), μ[(fun ω ↦ μ[g | m] ω * ξ ω) | m] ω ∂μ := by
  simpa [hF] using
    (MeasureTheory.integral_condExp (μ := μ) (m := m) (hm := hm) (f := F)).symm

exact h_goal.symm

Why this works:

• set F := ... gives the expression an explicit name
• Lean never compares different lambda expressions
• simpa [hF] unfolds F uniformly in both places
• No binder name mismatches because we use the same name throughout

Pattern:

1. set F := <complex expr> with hF
2. Apply lemma to the named F
3. Unfold with simpa [hF] or rw [hF]

See also: lean-phrasebook.md - "Name complex expression to avoid alpha/beta-equivalence issues"

15. Invalid 'import' Command (Module Docstring Before Imports)

Problem: A module-level /-! ... -/ docstring placed before the import block turns the imports into a parse error.

Full error message:

error: invalid 'import' command, it must be used in the beginning of the file

What's wrong: In Lean 4, imports must appear before any command or module-docstring content in the file. Plain comments such as the copyright header are allowed before imports, but a module docstring (/-! ... -/) is parsed as file content — everything after it is treated as the file body, so the subsequent import lines become invalid.

Example failure:

-- ✗ Fails:
/-! # My Module -/
import Mathlib.Data.Real.Basic

-- ✓ Works:
import Mathlib.Data.Real.Basic
/-! # My Module -/

Fix: Move the /-! ... -/ module docstring after the import block. The error message names import, not the docstring — the docstring's position is the cause.

See also: mathlib-style.md § 2 Placement for the canonical file-top order — copyright → imports → module docstring in plain files; in module-system files, copyright → module → imports → module docstring → public section (mathlib-style.md § 1).

16. Cannot Import Non-Module from Module

Problem: A file that starts with module imports a file that does not.

Full error message:

error: cannot import non-`module` Foo from `module`

What's wrong: All imports of a module file must themselves be modules. The named file Foo is not a module. Two things cause this exact error; a third is a common companion problem that does not:

1. Foo is your own source file lacking the module keyword. Add module after the copyright block (canonical template in mathlib-style.md § 1).
2. Foo is a plain-style generated aggregator (a generated root-import aggregator such as Mathlib.lean or Mathlib/Tactic.lean). Inspect its header. Plain lake exe mk_all preserves the existing style — it refreshes a module-style aggregator as a module and leaves a plain aggregator plain, so on a plain aggregator the non-module error persists. Use lake exe mk_all --module to create or convert an aggregator to module style (it emits a module header with public import lines):

   module
   
   public import Mathlib.Tactic.Basic
   public import Mathlib.Tactic.Ring

3. Aggregator staleness is a separate companion problem. After files are added, renamed, or deleted, an aggregator's import list goes stale; refresh it with lake exe mk_all. Staleness does not change the aggregator's module status, so it does not cause this specific non-module error — though it causes other failures: adding a file may leave the aggregator buildable but incomplete, while a rename or deletion may leave it importing the old module and failing with a missing/unknown-module error.

Fix: Case 1 → add the module header to Foo. Case 2 → lake exe mk_all --module to convert (or create) a module-style aggregator; plain mk_all will not convert it. Case 3 → lake exe mk_all to refresh the import list.

17. Module Visibility: Name Exists Upstream but Is Not Exported

Problem: Declarations inside a module are private by default; public import re-exports only the imported module's public scope. Code that worked with plain imports can fail against module-system dependencies. Three distinct signatures, each with its own remedy:

Signature A — the name is simply missing:

error: Unknown identifier `greeting`

The declaration exists in the imported module's private scope. Before treating this as a missing-import problem (§ 5), check whether the defining file is a module and the name is non-public. Remedies, in order: use the module's public API instead; within the same Lake package (tests, internal files), import all TheModule adds its private scope — by default import all is allowed only within the same package (a package may set the Lake allowImportAll option to open its private scope to other packages), but never use import all on a downstream dependency's private API you don't control; if the export gap is the actual bug, fix it upstream by making the declaration public.

Signature B — the name resolves but its body won't unfold:

error: Invalid simp theorem `greeting`: Expected a definition with an exposed body

The definition is public but its body is not exposed (plain public section exports signatures while keeping implementations opaque). The remedy depends on where you are:

• Within the same package (an internal lemma or test that legitimately needs the body), import the module's private scope with import all — the reference demonstrates exactly this to unfold a definition in a proof:

  module
  
  import all Tree.Basic   -- brings Tree.Basic's private scope in, so its body can unfold here

• Across a package boundary, do not unfold — use the module's API lemmas.
• If definitional unfolding is intentionally part of the public API, the upstream fix is @[expose] on the definition.

Signature C — a transitional warning, not an error:

Private declaration `drop2` accessed publicly

The rest of the emitted line names a backward-compatibility transition option (the current reference cites backward.privateInPublic; the exact suffix may vary by toolchain version). A public declaration's signature (or default argument) refers to a private declaration; it compiles only under that option. Recognize it as a visibility problem in the definition's interface, not an importer-side one. Concrete fixes: make the referenced declaration public; make the consuming declaration private; or rewrite the public signature so it no longer mentions the private declaration. Prefer a real fix over leaving the option enabled.

18. Meta-Phase Errors (meta import, public meta import)

Problem: The module system separates the compile-time (meta) phase from the ordinary phase. There are two opposite failure directions — do not apply the same fix to both.

Direction A — meta code lacks a meta-phase dependency:

error: Invalid `meta` definition `myMacro`, `helper` not marked `meta`

A macro/tactic/elaborator uses a declaration that is not available at the meta phase. If helper is in the current module, mark it meta; if it comes from another module, meta import that module:

meta import Macros.Helper

Use public meta import only when the meta dependency must propagate through a public metaprogram (i.e. it is reachable from a public meta definition) — this re-exports it at the meta phase to downstream modules:

public meta import Macros.Helper

Direction B — ordinary code uses meta-only code:

error: Invalid definition `colors`, may not access declaration `toPalindrome` marked as `meta`

This is the reverse: a runtime definition accesses something that exists only at the meta phase. meta import is not the fix here. Either the consumer must itself become meta, or the shared code moves to its own module imported at both phases — a meta import for compile time and a regular import for runtime. The reference demonstrates this by moving the shared toPalindrome into Phases.Pal:

meta import Phases.Pal
import Phases.Pal

19. Old-Style Header in a Module-System Repo

Problem: A file starts with plain top-of-file import lines (no module keyword) in a repository whose files use the module system — commonly a file generated from a pre-module-system template. It may elaborate on its own, but a module-style importer or aggregator cannot import it at all (§ 16).

What's wrong: The current mathlib header shape is: copyright block → module → grouped public import / plain import blocks (blank line between them) → /-! docstring → public section. Declarations in a module are private by default, so a converted file also needs the public section (or per-declaration public) to export its API.

Fix: Rewrite the header to the canonical template in mathlib-style.md § 1, then refresh generated root-import files with lake exe mk_all. Command-side: /lean4:draft and /lean4:formalize emit this shape for mathlib-targeted --output=file writes (--mathlib-template).

20. Bare Type Result Annotation Forces Universe 0

Problem: : Type means Type 0, not "some type". Elaboration pushes that constraint backwards into the arguments, so the error can land on an argument (or the application) of a universe-polymorphic definition and read as if that definition were broken.

Full error message (reported at the argument α, Lean 4.33.1):

error: Application type mismatch: The argument
  α
has type
  Type u
of sort `Type (u + 1)` but is expected to have type
  Type
of sort `Type 1` in the application
  WrappedType α

Example failure:

universe u
def WrappedType (α : Type u) : Type u := α

-- ✗ Fails at `α`: the result annotation means `Type 0`
example (α : Type u) : Type := WrappedType α
-- ✗ An explicit universe argument cannot override the annotation; the error
--   moves to the application ("Type mismatch  WrappedType α …")
example (α : Type u) : Type := WrappedType.{u} α

-- ✓ Infer the result universe …
example (α : Type u) : Type _ := WrappedType α
-- ✓ … or state the universe relationship explicitly
example (α : Type u) : Type u := WrappedType α

Fix: use Type _ when the universe should be inferred, or Type u (naming the universe) when the relationship to the arguments is part of the statement. Write a bare : Type only when universe zero is intended. Neither _ nor a named universe is universally preferable: _ asks for inference, u documents a relationship.

Why it matters: the apparent conclusion is "the definition under test is uninstantiable", when the probe's annotation is the cause. All four forms above are in tests/fixtures/reference_snippets/diagnostic_snippets.lean (the two failures as #guard_msgs controls).

21. Declaration Prefix Ordering (omit … in, Attributes, Docstring)

Problem: the pieces that can precede a declaration have a fixed order. A docstring (/-- … -/) binds to the next command; omit [...] in and set_option … in are command prefixes that must come before it, and attributes (@[simp]) come after it, immediately before the declaration keyword. Put the docstring first and omit is parsed as a separate command, which is exactly what the message says.

Full error message (Lean 4.33.1; reported at the docstring's position, not the omit line — an instance of § 13):

error: unexpected token 'omit'; expected '#guard_msgs', 'abbrev', 'add_decl_doc', 'axiom', … 'theorem' or 'unif_hint'

The searchable part is unexpected token 'omit'; the alternative list is long and toolchain-dependent.

Example failure:

section
variable [Inhabited Nat]

-- ✗ Fails, error reported at the docstring:
/-- Doc comment placed before omit. -/
omit [Inhabited Nat] in
theorem bad : True := trivial

-- ✓ Prefix first, then docstring, then declaration:
omit [Inhabited Nat] in
/-- Doc comment after omit. -/
theorem good : True := trivial
end

The rule, in one place:

This is declaration prefix ordering. File-header ordering (copyright → module → imports → module docstring → public section) is a different rule with its own error, invalid 'import' command: see § 15 and mathlib-style.md § 2 Placement.

The repair is a tests/fixtures/reference_snippets/diagnostic_snippets.lean entry and the failure is the must-fail diagnostic_omit_negative.lean beside it (a parse error, so #guard_msgs cannot wrap it); domain-patterns.md Pattern 7 shows the measure-theory use and links here rather than restating the rule.

Type Class Debugging Commands

-- See synthesis trace
set_option trace.Meta.synthInstance true in
theorem test : Goal := by infer_instance

-- See which instance was chosen
#check (inferInstance : IsProbabilityMeasure μ)

-- Check all implicit arguments
#check @my_lemma

Common Patterns to Avoid

❌ Fighting the Type Checker

-- Repeatedly trying variations until something compiles
exact h
exact h.1
exact ⟨h⟩
exact (h : _)  -- Guessing

✅ Understanding Then Fixing

#check h  -- See what h actually is
#check goal  -- See what's needed
-- Now fix systematically

❌ Ignoring Error Messages

-- "It says type mismatch, let me try random things"

✅ Reading Carefully

-- Error says "has type A but expected B"
-- Solution: Convert A to B or restructure

OOM from Large Dependent Type Signatures

A file with all-sorry proof bodies can still OOM or take tens of minutes to build if the type signatures are expensive to elaborate. sorry skips the proof, but Lean must still fully elaborate every type signature at the definition site and every call site that destructures the result; importing or downstream files can also become slow or time out.

Watch for this when:

• Return type has 6+ existential/conjunction components with dependent types
• Types reference List/Vector/Array with length-indexed proof terms
• Types contain Fin.cast, by omega, or by simp; omega inside binder types
• File takes minutes to build even though all proofs are sorry

Symptom: lake build consumes multi-GB RAM and is OOM-killed (exit code 137), or LSP times out on any file importing the module.

Fixes:

1. Isolate pathological signatures into small, rarely-recompiled files
2. Break dependency chains — extract structure definitions into lightweight files so editing proof files doesn't trigger re-elaboration of heavy signatures
3. Sorry call sites too — when obtain ⟨...many binders...⟩ := heavy_thm ... is itself expensive, sorry the caller until the callee is ready

Not a concern when: signatures are small (3-4 binders or fewer), types don't have deeply nested proof-term dependencies, or file builds in seconds.

Build Log Capture

For debugging persistent build errors, capture the full log for inspection:

Basic Capture

LOG=$(mktemp -t lean4_build_XXXXXX.log)
lake build 2>&1 | tee "$LOG"

# Quick scans
tail -n 120 "$LOG"
rg -n "error|warning|failed" "$LOG"

With Git Hash (Conflict-Safe)

HASH=$(git rev-parse --short HEAD 2>/dev/null || date +%s)
LOG="/tmp/lean4_build_${HASH}_$RANDOM.log"
lake build 2>&1 | tee "$LOG"

Benefits:

• Preserves logs across rebuilds for comparison
• Avoids filename clashes between runs
• Enables grep without rebuilding
• Links log to specific commit state

See also: Repair Mode (live repository copy) for escalation-only repair policy.