4.25 Common Pitfalls and Debugging

Rewriting failures in Lean usually come from a small set of recurring issues. This section lists the typical failure modes and the corresponding fixes, with a bias toward fast diagnosis.

Pattern mismatch

rw [h] does nothing when the left-hand side of h does not match any subterm.

-- h : a = b
-- goal contains f a, but rewrite expects a

Fix by matching the exact shape:

• Apply congruence: rw [congrArg f h]
• Reshape the goal: unfold definitions or introduce arguments
• Use simp [h] if normalization is intended

Wrong orientation

The equality is correct but used in the wrong direction.

rw [h]     -- no effect
rw [← h]   -- works

Always check both orientations. Prefer the direction that moves toward a canonical form.

Hidden occurrences under binders

rw cannot reach terms inside lambdas or quantifiers.

-- goal: (fun x => x + a) = (fun x => x + b)

Fix by exposing the body:

funext x
rw [h]

or use conv for targeted rewriting.

Missing arguments or implicit inference failure

A lemma requires parameters that are not inferred.

rw [Nat.add_comm]   -- ambiguous

Fix by supplying arguments:

rw [Nat.add_comm a b]

or by reshaping the goal so inference succeeds.

Rewriting too much

rw replaces all matching occurrences, which can break structure.

-- multiple occurrences of a
rw [h]   -- changes all

Fix with conv to target a specific occurrence.

Rewrite loops and instability

simp or repeated rw oscillates between equivalent forms.

-- conflicting rules
a + b ↔ b + a

Fix by:

• Removing symmetric rules from the simp set
• Using simp only [...]
• Applying rw explicitly for non-canonical steps

Dependent type mismatch

Rewriting changes indices and breaks types.

-- goal: P b, hypothesis: P a, h : a = b

Fix by rewriting in the correct place:

rw [← h]
exact Ha

or rewrite the hypothesis instead of the goal.

Function equality not reducing

Trying to rewrite functions directly fails.

-- goal: f = g
rw [h]   -- no effect

Fix with extensionality:

funext x
rw [h]

Structure equality not decomposed

Rewriting a whole structure fails when field-level reasoning is needed.

-- goal: p = q
rw [h]   -- insufficient

Fix with ext:

ext
-- prove field equalities

Simplifier not doing what you expect

simp may miss a rule or apply too many.

Fix by:

• Adding lemmas locally: simp [h]
• Restricting rules: simp only [...]
• Inspecting suggestions: simp?

Diagnostic workflow

When rewriting fails:

1. Inspect the goal shape.
2. Check the lemma type and orientation.
3. Identify whether the occurrence is visible.
4. Try rw in both directions.
5. Switch to simp, calc, or conv if needed.
6. Reduce the problem to a smaller subgoal.

Minimal example reduction

Isolate the issue:

-- extract a smaller goal
have : ... := by
  ...

Work on the reduced form until the rewrite succeeds, then reinsert into the main proof.

Summary

Most rewriting issues reduce to mismatched patterns, wrong direction, hidden structure, or uncontrolled rule sets. A systematic approach to inspecting goals, choosing tools, and applying small steps resolves these problems efficiently.