# 4.5 Directed Rewriting with `rw`

# 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:

```lean
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.

```lean
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:

```lean
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:

```lean
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:

```lean
rw [h] at H
```

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

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

or combine them:

```lean
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:

```lean
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:

```lean
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.

```lean
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.