/lean4

Refactoring Long Proofs

Guide for breaking monolithic proofs into maintainable helper lemmas.

Refactoring Decision Tree

Is the proof 60-200 lines? (sweet spot for refactoring)
├─ Yes: Look for natural boundaries (use lean_goal at 4-5 key points)
│   ├─ Repetitive structure (lhs/rhs, symmetric args, or repeated case splits)?
│   │   └─ Extract common pattern to helper (Pattern 1.3)
│   ├─ Single large case split (30+ lines proving reusable fact)?
│   │   └─ Extract even if not repeated (Pattern 1.3 - single large case split)
│   ├─ Multiple properties proven separately, used together?
│   │   └─ Bundle with ∧, use obtain (Pattern 1.5)
│   ├─ Mixes multiple mathematical domains (combinatorics + analysis)?
│   │   └─ Extract each domain's logic separately (Pattern 1.2)
│   ├─ Starts with 50+ line preliminary calculation?
│   │   └─ Extract preliminary fact to helper (Pattern 1.1)
│   ├─ Same 5-10 line notation conversion repeated?
│   │   └─ Extract conversion helper (Pattern 1.6)
│   ├─ Found witness extraction (choose/obtain)?
│   │   └─ Extract to helper (Pattern 1.4 - clear input/output contract)
│   ├─ Found arithmetic bounds?
│   │   ├─ Can extract without `let` bindings? → Extract to private helper (Pattern 3.1)
│   │   └─ Uses complex `let` bindings? → Consider inlining (Pattern 2.3)
│   ├─ Found permutation construction?
│   │   └─ Reusable pattern? → Extract (ensure parameter clarity, Pattern 2.1)
│   ├─ Found "all equal, pick one" pattern?
│   │   ├─ Equality proof → Extract to helper (Pattern 2.4 - mathematical content)
│   │   └─ Choice of representative → Keep in main (proof engineering)
│   └─ Found measure manipulations?
│       └─ Uses `let` bindings? → Prefer inlining (Pattern 3.4 - definitional issues)
├─ > 200 lines? → Multiple refactorings needed (start with largest prelims, Pattern 1.1)
└─ < 60 lines? → Probably fine as-is (unless heavily repetitive)

When extracting:
1. Make helper `private` if proof-specific (Pattern 3.1: use regular -- comments, not /-- -/)
2. **Generic is better** (Pattern 2.1): Remove proof-specific constraints
3. Avoid `let` bindings in helper signatures (Pattern 2.3)
4. If omega fails, add explicit intermediate steps (Pattern 3.3: use calc)
5. Prefix unused but required parameters with underscore (Pattern 3.2: _hS)
6. Add structural comments that explain "why", not "what" (Pattern 4.2)
7. Test compilation after each extraction (Pattern 5.1: lean_diagnostic_messages)

When to Refactor

Sweet spot: Proofs between 60-200 lines benefit most from refactoring. Under 60 lines, overhead exceeds benefit. Over 200 lines, multiple refactorings needed.

Refactor when:

• Proof exceeds 100 lines (or 60+ with repetitive structure)
• Multiple conceptually distinct steps
• Intermediate results would be useful elsewhere
• Hard to understand/maintain
• Repeated patterns (especially lhs/rhs with near-identical proofs)
• Large preliminary calculations (50+ line have statements)
• Property bundling opportunities (multiple properties proven separately, used together)
• Elaboration timeouts from nested lemma applications (see performance-optimization.md Pattern 2)

Don't refactor when:

• Proof is short and linear (< 50 lines, no repetition)
• No natural intermediate milestones
• Extraction would require too many parameters
• Proof is already well-factored (see signs below)

Signs of a well-factored proof (skip these):

• Clear section comments delineate logical steps (e.g., "-- Step 1: Establish bounds", "-- Step 2: Apply induction")
• Natural linear flow without tangents or backtracking
• Core mathematical argument dominates (e.g., induction structure, case analysis, algebraic manipulation is the bulk)
• No large extractable blocks - all have statements are short (< 20 lines) or inherently tied to the main flow
• Readable without refactoring - you can follow the proof logic by reading comments and goals

Example of already-clean proof:

theorem foo : Result := by
  -- Step 1: Base case
  have base : P 0 := by simp

  -- Step 2: Inductive step
  suffices ∀ n, P n → P (n + 1) by
    intro n; induction n <;> assumption

  -- Main induction argument (this IS the proof)
  intro n hn
  cases n with
  | zero => exact base
  | succ n' =>
    have ih := hn n' (Nat.lt_succ_self n')
    calc P (n' + 1) = ... := by ...
                  _ = ... := by ih

  -- Conclusion follows immediately
  exact result

Why not refactor: The induction structure IS the content. Extracting pieces would obscure the mathematical flow. Comments already clarify structure.

Pattern Quick Reference

When refactoring, ask yourself:

1. Identify opportunities (Pattern 1): What signals extraction?

   • 50+ line preliminary? → 1.1
   • Mixing domains? → 1.2
   • Repetitive structure (lhs/rhs, symmetric args, large case splits)? → 1.3
   • Witness extraction? → 1.4
   • Properties always together? → 1.5
   • Recurring conversion? → 1.6

2. Design helpers (Pattern 2): How to make them reusable?

   • Generalize constraints → 2.1
   • Minimize assumptions → 2.2
   • Avoid let bindings → 2.3
   • Separate math from engineering → 2.4

3. Follow conventions (Pattern 3): Lean-specific rules?

   • Private? Use -- not /-- -/ → 3.1
   • Unused param? Add _ prefix → 3.2
   • Omega failing? Add intermediate steps → 3.3
   • Measure theory? Watch definitional equality → 3.4

4. Structure main proof (Pattern 4): After extraction?

   • Named steps with comments → 4.1
   • Explain "why" not "what" → 4.2

5. Safe workflow (Pattern 5): How to refactor safely?

   • Test after each extraction → 5.1
   • Check goals at 4-5 points → 5.2
   • One at a time → 5.3
   • Use LSP for fast feedback → 5.4

6. Document (Pattern 6): What to explain?

   • What it proves → 6.1
   • Why it's true → 6.2
   • How it's used → 6.3

LSP-Based Refactoring Workflow

Strategy: Use lean_goal (from Lean LSP MCP) to inspect proof state at different locations, then subdivide at natural breakpoints where intermediate goals are clean and reusable.

Step 1: Survey the Proof

Walk through the proof checking goals at 4-5 key points:

# Check goals at 4-5 key locations in the long proof
lean_goal(file, line=15)   # After initial setup
lean_goal(file, line=45)   # After first major step
lean_goal(file, line=78)   # After second major step
lean_goal(file, line=120)  # After third major step
lean_goal(file, line=155)  # Near end

What to look for:

• Clean, self-contained intermediate goals
• Natural mathematical milestones
• Points where context significantly changes
• Repetitive structure (same proof pattern for lhs/rhs)

Step 2: Identify Extraction Points

Look for locations where:

• Goal is clean: Self-contained statement with clear meaning
• Dependencies are local: Depends only on earlier hypotheses (no forward references)
• Useful elsewhere: Goal would be reusable in other contexts
• Natural meaning: Intermediate state has clear mathematical interpretation

Good breakpoints:

• After establishing key inequalities or bounds
• After case splits (before/after by_cases)
• After measurability/integrability proofs
• Where intermediate result has a clear name
• After computing/simplifying expressions
• Before/after applying major lemmas

Bad breakpoints:

• Mid-calculation (no clear intermediate goal)
• Where helper would need 10+ parameters
• Where context is too tangled to separate cleanly
• In the middle of a calc chain
• Where goal depends on later bindings

Step 3: Extract Helper Lemma

-- BEFORE: Monolithic proof
theorem big_result : Conclusion := by
  intro x hx
  have h1 : IntermediateGoal1 := by
    [30 lines of tactics...]
  have h2 : IntermediateGoal2 := by
    [40 lines of tactics...]
  [30 more lines...]

-- AFTER: Extracted helpers
lemma helper1 (x : α) (hx : Property x) : IntermediateGoal1 := by
  [30 lines - extracted from h1]

lemma helper2 (x : α) (h1 : IntermediateGoal1) : IntermediateGoal2 := by
  [40 lines - extracted from h2]

theorem big_result : Conclusion := by
  intro x hx
  have h1 := helper1 x hx
  have h2 := helper2 x h1
  [30 lines - much clearer now]

Step 4: Verify with LSP

After each extraction:

lean_diagnostic_messages(file)  # Check for errors
lean_goal(file, line)           # Confirm goals match

Verify extraction is correct:

# Original line number where `have h1 : ...` was
lean_goal(file, line=old_h1_line)
# → Should match helper1's conclusion

# New line number after extraction
lean_goal(file, line=new_h1_line)
# → Should show `h1 : IntermediateGoal1` available

Non-LSP Refactoring (Manual)

If you don't have LSP access, use this manual workflow:

Step 1: Read and Understand

Read through the proof identifying conceptual sections:

• What is the proof trying to establish?
• What are the major steps?
• Are there repeated patterns?

Step 2: Mark Candidates

Add comments marking potential extraction points:

theorem big_result : ... := by
  intro x hx
  -- Candidate 1: Establish boundedness
  have h1 : ... := by
    ...
  -- Candidate 2: Prove measurability
  have h2 : ... := by
    ...

Step 3: Extract One at a Time

Extract one helper at a time, compile after each:

1. Copy have proof to new lemma
2. Identify required parameters
3. Replace original with have h := helper args
4. lean_diagnostic_messages(file) per-edit, lake env lean <path/to/File.lean> for file gate (from project root); once a refactor has touched an imported module, gate with lake lean <path/to/File.lean> instead — the file gate reads stale .oleans (File Gate Scope)
5. Commit if successful

Step 4: Iterate

Repeat until proof is manageable.

Naming Extracted Helpers

Good names describe what the lemma establishes:

• bounded_by_integral - establishes bound
• measurable_composition - proves measurability
• convergence_ae - proves a.e. convergence

Avoid vague names:

• helper1, aux_lemma - meaningless
• part_one, step_2 - based on structure, not content
• temp, tmp - should be permanent

Mathlib-style conventions:

• Use snake_case
• Include key concepts: integral, measure, continuous, etc.
• Add context if needed: of_, _of, _iff

Real Refactoring Example

Context: 63-line monolithic proof about exchangeable measures with strict monotone functions.

Step 1: Identify natural boundaries

Using lean_goal at different points revealed:

• Line 15: After establishing hk_bound : ∀ i, k i < n (clean arithmetic result)
• Line 35: After constructing permutation (conceptually distinct)
• Line 50: After projection proof (measure theory manipulation)

Step 2: Extract arithmetic helper

Found this embedded calculation:

have hk_bound : ∀ i : Fin (m' + 1), k i < n := by
  intro i
  simp only [n]
  have : k i ≤ k ⟨m', Nat.lt_succ_self m'⟩ := by
    apply StrictMono.monotone hk_mono
    exact Fin.le_last i
  omega

Extracted to:

/-- Strictly monotone functions satisfy k(i) ≤ k(last) for all i -/
private lemma strictMono_all_lt_succ_last {m : ℕ} (k : Fin m → ℕ)
    (hk : StrictMono k) (i : Fin m) (last : Fin m)
    (h_last : ∀ j, j ≤ last) :
    k i ≤ k last := by
  apply StrictMono.monotone hk
  exact h_last i

Result: Main proof now just calls helper, much clearer.

Step 3: Verify with LSP

lean_diagnostic_messages(file)  # No errors ✓
lean_goal(file, line=15)        # Shows helper available ✓

Final structure:

• Original: 63 lines monolithic
• Refactored: 45 lines main + 33 lines helpers = 78 lines total
• Success: Much clearer structure, each piece testable independently

Key insight: Success measured by clarity, not brevity.

Refactoring Patterns

6 high-level patterns cover all refactoring scenarios. Each contains specific sub-patterns you can apply directly.

Pattern 1: Identify Extraction Opportunities

What to look for: These signals indicate a helper should be extracted.

1.1. Large Preliminary Calculations

Trigger: Proof starts with 50+ line have statement before the main argument.

Example:

theorem main_result ... := by
  -- 51 lines proving preliminary bound
  have hAux : ∑ i, |p i - q i| ≤ 2 := by
    [massive calculation]
  -- Main argument obscured above
  calc ...

Action: Extract to private lemma preliminary_bound ...

Why: Preliminary fact has independent mathematical interest, makes main proof immediately visible, enables testing the preliminary calculation separately.

1.2. Domain Separation

Trigger: Proof mixes independent mathematical domains (combinatorics + functional analysis, algebra + topology).

Example: 130-line proof mixing finite probability distributions (combinatorics) with L² bounds (functional analysis).

Action: Extract each domain's logic into separate helpers.

Why: Each helper uses only tools from its domain, main theorem reads at correct abstraction level, helpers highly reusable.

1.3. Repetitive Structure (lhs/rhs and Case Splits)

Trigger: Nearly identical proofs for both sides of equation, symmetric arguments, or multiple cases with same structure.

Basic pattern (literal repetition):

-- Symmetric sides of equation
have hlhs : P lhs := by [20 lines]
have hrhs : P rhs := by [20 lines, nearly identical!]

-- Symmetric objects/arguments (P and Q, left and right, forward and backward)
have hP : Property P := by [14 lines]
have hQ : Property Q := by [14 lines, exact duplicate!]

Action: Extract private lemma has_property_P (expr : α) : P expr

Single large case split (even if not repeated):

Even a SINGLE 30+ line case split should be extracted if it proves a standalone mathematical fact.

Trigger: One large case analysis (30+ lines) that proves a reusable identity.

Example:

-- Before: 37-line case split inline
have h := by
  by_cases hY : ω ∈ Y ⁻¹' A <;> by_cases hZ : ω ∈ Z ⁻¹' B
  · -- 9 lines for case 1
    ...
  · -- 9 lines for case 2
    ...
  · -- 9 lines for case 3
    ...
  · -- 9 lines for case 4
    ...

-- After: Clean one-liner
have h := prod_indicators_eq_indicator_intersection X k B

When to extract single case splits: The case analysis proves a fact that:

• Could be stated as a standalone lemma with clear mathematical meaning
• Doesn't depend on specific context of the current proof
• Would be reusable in other proofs

Advanced pattern (abstract structural repetition):

When the same case-split structure appears multiple times for slightly different goals, extract the shared structure. The key is recognizing that the proof pattern is the same even if the specific goals differ.

Example: Same 4-case structure for different goals

-- First occurrence: proving product of indicators = single indicator for A×B
have h1 : (A.indicator 1 * B.indicator 1) x = (A ×ˢ B).indicator 1 x := by
  by_cases ha : x ∈ A <;> by_cases hb : x ∈ B
  · -- Case 1: x ∈ A, x ∈ B → both sides = 1
    simp [ha, hb]
  · -- Case 2: x ∈ A, x ∉ B → both sides = 0
    simp [ha, hb]
  · -- Case 3: x ∉ A, x ∈ B → both sides = 0
    simp [ha, hb]
  · -- Case 4: x ∉ A, x ∉ B → both sides = 0
    simp [ha, hb]

-- Second occurrence: proving intersection of preimages for indicators
have h2 : (f⁻¹'A.indicator 1 * g⁻¹'B.indicator 1) x = (f⁻¹'A ∩ g⁻¹'B).indicator 1 x := by
  by_cases ha : x ∈ f⁻¹'A <;> by_cases hb : x ∈ g⁻¹'B
  · -- Same 4-case structure!
    simp [ha, hb]
  · simp [ha, hb]
  · simp [ha, hb]
  · simp [ha, hb]

Extract the abstract pattern:

-- Captures: product of indicators = indicator of combined set
private lemma indicator_mul_eq_indicator {α : Type*} (s t : Set α) (x : α) :
    s.indicator (1 : α → ℝ) x * t.indicator 1 x = (s ∩ t).indicator 1 x := by
  by_cases hs : x ∈ s <;> by_cases ht : x ∈ t <;> simp [hs, ht]

-- Now both uses become one-liners
have h1 := indicator_mul_eq_indicator A B x
have h2 := indicator_mul_eq_indicator (f⁻¹'A) (g⁻¹'B) x

Why this works:

• The mathematical structure (4-case split on membership) is identical
• Only the specific sets differ (A×B vs A∩B, direct sets vs preimages)
• Helper captures the abstract pattern, works for any sets
• Main theorem reads at higher level of abstraction

Recognition pattern: If you find yourself writing the same by_cases structure multiple times with the same number of cases and similar reasoning in each case, even if the goals look different on the surface, there's likely an abstract pattern to extract.

Summary rules:

• Literal repetition: Copy-paste with only variable names changed (lhs/rhs, P/Q) → extract
• Single large case split: 30+ line case analysis proving reusable fact → extract even if not repeated
• Abstract structural repetition: Same case-split structure for different goals → extract abstract pattern
• Why: Write logic once, changes apply automatically, helpers reusable, main proof reads at higher abstraction level

1.4. Witness Extraction

Trigger: choose or multiple obtain extracting witnesses from existentials.

Example:

have : ∀ i, ∃ T, MeasurableSet T ∧ s = f ⁻¹' T := by [proof]
choose T hTmeas hspre using this

Action: Extract obtain ⟨T, hTmeas, hspre⟩ := witnesses_helper ...

Why: Clear input/output contract (hypotheses → witnesses), helper testable independently, construction logic reusable.

1.5. Property Bundling

Trigger: Multiple related properties proven separately but always used together.

Example:

have h1 : Property1 x := by [proof]
have h2 : Property2 x := by [proof]
have h3 : Property3 x := by [proof]
exact final_lemma h1 h2 h3  -- Always used together

Action: Bundle with ∧, extract obtain ⟨h1, h2, h3⟩ := bundle_properties x

When to bundle: Properties share hypotheses, always proven together, conceptually related.

When NOT: Different hypotheses, sometimes used independently.

1.6. Notation Conversions

Trigger: Same 5-10 line conversion between notations repeated multiple times.

Common conversions:

• Set builder ↔ pi notation: {x | ∀ i, x i ∈ s i} ↔ Set.univ.pi s
• Measure ↔ integral: μ s ↔ ∫⁻ x, s.indicator 1 ∂μ
• Preimage ↔ set comprehension

Action: Extract conversion helper with clear purpose.

Why: Conversion written once, main proof focuses on mathematics not notation.

Pattern 2: Design Reusable Helpers

How to extract: Make helpers generic and broadly applicable.

2.1. Generic is Better

Principle: Remove proof-specific constraints when extracting.

Techniques:

1. Relax equality to inequality: n = 42 → 1 ≤ n
2. Remove specific values: Use parameters instead of constants
3. Weaken hypotheses: Use only what's needed in proof
4. Broaden types: Fin 10 → Fin n if bound doesn't matter

Example:

-- ❌ Too specific
private lemma helper (n : ℕ) (hn : n = 42) : Property n

-- ✅ Generic
private lemma helper (n : ℕ) (hn : 1 ≤ n) : Property n

Balance: Don't over-generalize to 10+ parameters.

2.2. Isolate Hypothesis Usage

Principle: Extract helpers with minimal assumptions for maximum reusability.

Example: In a proof using surjectivity, only ONE helper needs it - others work without.

Practice:

• Extract helper with minimal assumptions first
• Build specialized helpers on top
• Creates reusability hierarchy

2.3. Avoid Let Bindings in Helper Signatures

Problem: Let bindings create definitional inequality - helper's let proj ≠ main's let proj even if syntactically identical.

Solutions:

• Option A: Explicit parameters with equality proofs

  private lemma helper (μX : Measure α) (hμX : μX = pathLaw μ X) ...
  -- Call site: helper μX rfl  -- ✓ Unifies perfectly

• Option B: Inline the proof (for measure theory manipulations)

Why: Definitional inequality causes rewrite failures even with identical-looking expressions.

2.4. "All Equal, Pick One" Pattern

Pattern: "All things are equal, so pick one canonical representative."

Structure:

1. Mathematical content (all candidates equal) → Extract to helper
2. Proof engineering (choice of which to use) → Keep in main
3. Use equality from helper → Main proof

Why separate: Equality proof has mathematical content worth reusing. Choice is arbitrary proof engineering.

Pattern 3: Lean-Specific Conventions

Code quality: Follow Lean syntax and style conventions.

3.1. Private Lemmas Use Regular Comments

Rule: private declarations use -- comments, not /-- -/ doc comments.

-- ✅ Correct
-- Helper for extracting witnesses
private lemma helper ...

-- ❌ Wrong
/-- Helper for extracting witnesses -/  -- Error: unexpected token '/--'
private lemma helper ...

Why: Doc comments are for public API. Private declarations don't appear in generated docs.

3.2. Unused Parameters Need Underscore

Rule: Intentionally unused parameters get underscore prefix.

-- Parameter needed in type signature but unused in proof
∀ n (S : Set (Fin n → α)) (_hS : MeasurableSet S), ...

Why: Signals "intentionally unused" to linter. Parameter required in signature but proof doesn't explicitly reference it.

3.3. Omega Limitations

Problem: omega fails on arithmetic goals that seem obvious.

Solution: Provide intermediate steps with calc or explicit equalities as hypotheses.

Example:

-- ❌ Fails
have : m ≤ k last + 1 := by omega

-- ✅ Works
have (h_last_eq : last.val + 1 = m) : m ≤ k last + 1 := by
  calc m = last.val + 1 := h_last_eq.symm
       _ ≤ k last + 1 := Nat.add_le_add_right h_mono 1

3.4. Measure Theory Requires Exact Alignment

Problem: Measure theory lemmas sensitive to definitional equality. Measure.map compositions must align exactly.

Solution: For measure manipulations with let bindings, prefer inlining over extraction (definitional inequality issues).

Pattern 4: Structure the Main Proof

After extraction: Reorganize main proof for clarity.

4.1. Named Steps with Comments

Pattern: Use semantically meaningful names for intermediate results. Only use generic names like step1, step2 when there's no better alternative and the results are private to this proof.

Prefer meaningful names:

theorem main_result ... := by
  -- Variance formula: E(∑cᵢξᵢ)² = E(∑cᵢ(ξᵢ-m))² using ∑cⱼ = 0
  have variance_formula : ... := by ...

  -- Covariance expansion: = ∑ᵢⱼ cᵢcⱼ cov(ξᵢ, ξⱼ)
  have covariance_expansion : ... := by ...

  -- Final: Combine steps
  calc ...

When meaningful names aren't obvious, use generic sequence:

theorem main_result ... := by
  -- Step 1: E(∑cᵢξᵢ)² = E(∑cᵢ(ξᵢ-m))² using ∑cⱼ = 0
  have step1 : ... := by ...

  -- Step 2: = ∑ᵢⱼ cᵢcⱼ cov(ξᵢ, ξⱼ) by expanding square
  have step2 : ... := by ...

  -- Final: Combine steps
  calc ...

Use step1, step2 only when:

• Results are private to this proof (not extracted as helpers)
• Used sequentially in a linear chain
• No clear mathematical names suggest themselves
• Proof is exploratory and may be refactored later

Benefits: Meaningful names aid comprehension, generic names show sequencing. Reads like textbook proof either way, mathematical narrative clear, easy to locate issues.

4.2. Structural Comments Explain "Why"

Good comments:

• Explain mathematical goal (not Lean syntax)
• Highlight where key hypotheses are used
• Make proof understandable from comments alone

Examples:

-- ✅ Good: Explains proof strategy
-- Extract witnesses Tᵢ such that s = f ⁻¹' Tᵢ for each i

-- ❌ Bad: Describes what code does
-- Choose the witnesses Tᵢ along with measurability

Pattern 5: Safe Refactoring Workflow

Process: Refactor incrementally with continuous verification.

5.1. Test After Every Extraction

Rule: Build after EACH extraction, not in batches.

With LSP (fast):

# After each edit
lean_diagnostic_messages(file_path)
lean_goal(file_path, line)

Without LSP:

lake env lean FILE.lean  # After each extraction (run from project root)
lake lean path/to/FILE.lean   # Instead, once an extraction moved code into an imported module (see cycle-engine.md#file-gate-scope)

Why: Errors compound. One error at a time is faster than five mixed together.

5.2. Examine Goal States at Key Points

Strategy: Use lean_goal at 4-5 strategic locations (not every line).

lean_goal(file, line=15)   # After initial setup
lean_goal(file, line=45)   # After first major step
lean_goal(file, line=78)   # After second major step
lean_goal(file, line=120)  # After third major step
lean_goal(file, line=155)  # Near end

What to look for:

• Clean, self-contained intermediate goals
• Natural mathematical milestones
• Points where context significantly changes
• Repetitive structure (same pattern for lhs/rhs)

5.3. One Helper at a Time

Workflow:

1. Extract one helper
2. Verify with lean_diagnostic_messages
3. Update main theorem
4. Verify again
5. Commit if successful
6. Repeat

Don't: Make multiple changes then check - errors compound!

5.4. LSP Works Even When Build Fails

Observation: lean_diagnostic_messages works even when lake build fails due to dependency issues.

Why useful: Verify refactoring locally using LSP at file/module level, don't wait for full project build.

Pattern 6: Document Helpers

Every helper should explain:

6.1. What It Proves

In mathematical terms, what does this lemma establish?

-- For a strictly monotone function k : Fin m → ℕ, we have m ≤ k(m-1) + 1
private lemma strictMono_length_le_max_succ ...

6.2. Why It's True

Key insight or technique used.

-- This uses the fact that strictly monotone functions satisfy i ≤ k(i) for all i

6.3. How It's Used

If not obvious from context.

-- Used to bound the domain length in the permutation construction

Full example:

/--
Helper lemma: The length of the domain is bounded by the maximum value plus one.

For a strictly monotone function `k : Fin m → ℕ`, we have `m ≤ k(m-1) + 1`.
This uses the fact that strictly monotone functions satisfy `i ≤ k(i)` for all `i`.
-/
private lemma strictMono_length_le_max_succ ...

Benefits of Refactoring

Maintainability:

• Easier to understand small proofs
• Easier to modify without breaking
• Clear dependencies between lemmas

Reusability:

• Helper lemmas useful in other contexts
• Avoid reproving same intermediate results
• Build library of project-specific lemmas

Testing:

• Test helpers independently
• Isolate errors to specific lemmas
• Faster compilation (smaller units)

Collaboration:

• Easier to review small lemmas
• Clear boundaries for parallel work
• Better documentation opportunities

Anti-Patterns

❌ Over-refactoring:

• Creating helpers used only once
• Extracting every have statement
• Too many small lemmas (harder to navigate)

❌ Under-refactoring:

• 500+ line proofs
• Multiple independent results in one theorem
• Repeated code instead of shared helpers

❌ Poor parameter choices:

• Extracting with 15+ parameters
• Including unnecessary generality
• Making helpers too specific to one use case

✅ Good balance:

• Extract when reusable or conceptually distinct
• Aim for 20-80 line helpers
• Parameters capture essential dependencies only

See Also

• lean-lsp-tools-api.md - LSP tools for goal inspection
• proof-golfing.md - Simplifying proofs after compilation
• mathlib-style.md - Naming conventions