4.5 Directed Rewriting with `rw`

Rewriting is the primary way to apply propositional equalities in Lean. The tactic rw performs a single, directed replacement using a proof of equality. It is precise, local, and predictable. This section focuses on controlling direction, location, and sequencing.

The basic form is:

rw [h]

where h : a = b. This replaces occurrences of a with b in the goal. The replacement is structural: Lean matches subterms equal to the left-hand side of h and substitutes them.

example (a b : Nat) (h : a = b) :
  a + 1 = b + 1 := by
  rw [h]

Direction matters. If the goal requires replacing b with a, you reverse the equality:

rw [← h]

This uses the symmetric form of h. Choosing the correct orientation is often the difference between progress and a stuck proof.

Multiple rewrites can be chained in a single step:

rw [h₁, h₂, h₃]

These are applied from left to right. Each rewrite updates the goal before the next one is attempted. Order therefore affects the result.

Rewriting also works inside hypotheses. To rewrite a hypothesis H, use:

rw [h] at H

This updates H in place. You can rewrite both the goal and hypotheses:

rw [h₁] at H
rw [h₂]

or combine them:

rw [h₁, h₂] at H

A common pattern is to normalize hypotheses before using them.

Targeting specific locations improves control. If a term appears multiple times, rw replaces all matching occurrences by default. To restrict rewriting, you can use pattern arguments:

rw [h] at *

applies the rewrite everywhere in the context. More precise control often requires restructuring the goal so that only the intended occurrence matches.

Rewriting with lemmas is routine. Many library lemmas are oriented for rewriting. For example:

example (a b : Nat) :
  a + b = b + a := by
  rw [Nat.add_comm]

The lemma Nat.add_comm has type a + b = b + a, so it can be used directly.

Rewriting can fail for several reasons. The most common are:

The left-hand side does not match any subterm.
The direction is incorrect.
The term is hidden under a binder or abstraction.
The equality requires additional arguments that are not inferred.

When rewriting fails, inspect the goal and the type of the lemma. Often the issue is a mismatch in structure or missing arguments.

Rewriting under binders requires care. If the occurrence is inside a lambda or quantifier, rw may not reach it directly. In such cases, you may need to introduce variables or transform the goal before rewriting.

example (a b : Nat) (h : a = b) :
  (fun x => x + a) = (fun x => x + b) := by
  funext x
  rw [h]

Here funext exposes the body of the function, making rewriting possible.

A useful discipline is to keep rewriting steps small and explicit. Each rw should perform a clear transformation. Long chains are better expressed with structured steps or calc blocks when readability matters.

In summary, rw is a single-step, directed rewrite. It gives you fine control over equality application. Effective use depends on choosing the correct direction, ordering rewrites carefully, and shaping goals so that matching succeeds.