# 2.9 Rewriting with Equality

Rewriting is the main way to use equality in Lean. If you have a proof `h : a = b`, then `rw [h]` replaces matching occurrences of `a` with `b`. This is the proof assistant version of substitution.

## Problem

You have an equality hypothesis and want to use it to simplify the goal or a hypothesis.

```lean
h : a = b
⊢ a + 1 = b + 1
```

The left side of the goal contains `a`, but the target is easier after replacing `a` with `b`.

## Solution

Use `rw`.

```lean
theorem rw_basic
    (a b : Nat)
    (h : a = b) :
    a + 1 = b + 1 := by
  rw [h]
```

The command rewrites `a` to `b`, so the goal becomes:

```lean
⊢ b + 1 = b + 1
```

Lean closes the goal by reflexivity.

## Rewriting Direction

By default, `rw [h]` uses the equality from left to right.

```lean
h : a = b
```

means:

```lean
replace a with b
```

To rewrite in the other direction, use `←`.

```lean
theorem rw_reverse
    (a b : Nat)
    (h : a = b) :
    b + 1 = a + 1 := by
  rw [← h]
```

Now Lean replaces `b` with `a`, so the goal becomes:

```lean
⊢ a + 1 = a + 1
```

## Rewriting in a Hypothesis

Use `at` to rewrite inside a hypothesis.

```lean
theorem rw_at_hypothesis
    (a b : Nat)
    (h : a = b)
    (hp : a + 1 = 10) :
    b + 1 = 10 := by
  rw [h] at hp
  exact hp
```

Before rewriting:

```lean
hp : a + 1 = 10
⊢ b + 1 = 10
```

After:

```lean
hp : b + 1 = 10
⊢ b + 1 = 10
```

So `exact hp` closes the goal.

## Rewriting Everywhere

Use `at *` to rewrite in the goal and all hypotheses.

```lean
theorem rw_everywhere
    (a b : Nat)
    (h : a = b)
    (hp : a + 1 = 10) :
    a + 1 = 10 := by
  rw [h] at *
  exact hp
```

This is convenient, but it should be used carefully. It may change hypotheses in ways that make the proof harder to read.

## Rewriting Multiple Equalities

The rewrite list is applied from left to right.

```lean
theorem rw_multiple
    (a b c : Nat)
    (h₁ : a = b)
    (h₂ : b = c) :
    a + 1 = c + 1 := by
  rw [h₁, h₂]
```

First Lean rewrites `a` to `b`. Then it rewrites `b` to `c`.

## Rewriting with Named Theorems

A rewrite rule does not need to be a local hypothesis. It can also be a theorem.

```lean
theorem rw_zero_add (n : Nat) : 0 + n = n := by
  rw [Nat.zero_add]
```

Here `Nat.zero_add` is a theorem from the natural number library.

A common theorem is:

```lean
Nat.add_comm
```

which states commutativity of addition.

```lean
theorem rw_add_comm (a b : Nat) : a + b = b + a := by
  rw [Nat.add_comm]
```

## Rewriting with Arguments

Some rewrite theorems have arguments. Lean usually infers them.

```lean
theorem rw_add_zero (n : Nat) : n + 0 = n := by
  rw [Nat.add_zero]
```

You can also provide arguments explicitly when needed.

```lean
theorem rw_add_comm_explicit (a b : Nat) : a + b = b + a := by
  rw [Nat.add_comm a b]
```

Most of the time, the shorter form is preferred.

## Rewriting Inside Larger Expressions

Lean rewrites matching subexpressions.

```lean
theorem rw_inside_expression
    (a b c : Nat)
    (h : a = b) :
    (a + c) * 2 = (b + c) * 2 := by
  rw [h]
```

Only the occurrence of `a` is replaced. The surrounding expression remains unchanged.

## Rewriting Multiple Occurrences

If a term occurs more than once, `rw` rewrites all matching occurrences by default.

```lean
theorem rw_multiple_occurrences
    (a b : Nat)
    (h : a = b) :
    a + a = b + b := by
  rw [h]
```

Both occurrences of `a` are replaced by `b`.

## Rewriting One Occurrence

When only one occurrence should be rewritten, use `nth_rewrite`.

```lean
theorem rw_one_occurrence
    (a b : Nat)
    (h : a = b) :
    a + a = b + a := by
  nth_rewrite 1 [h]
```

The first matching occurrence of `a` is rewritten, leaving the second occurrence unchanged.

Occurrence control is useful when a full rewrite would overshoot the target.

## Rewriting Under a Function

Equality can be rewritten under ordinary functions.

```lean
theorem rw_under_function
    (a b : Nat)
    (h : a = b)
    (f : Nat -> Nat) :
    f a = f b := by
  rw [h]
```

Lean replaces `a` with `b` inside the function application.

## Rewriting Predicates

Equality can also rewrite propositions.

```lean
theorem rw_predicate
    (a b : Nat)
    (P : Nat -> Prop)
    (h : a = b)
    (hp : P a) :
    P b := by
  rw [h] at hp
  exact hp
```

The hypothesis `hp : P a` becomes `hp : P b`.

This is often called transport along equality.

## Rewriting Backward in a Predicate

Sometimes the goal contains `P a`, but the available proof has type `P b`.

```lean
theorem rw_predicate_reverse
    (a b : Nat)
    (P : Nat -> Prop)
    (h : a = b)
    (hp : P b) :
    P a := by
  rw [h]
  exact hp
```

After `rw [h]`, the goal changes from:

```lean
⊢ P a
```

to:

```lean
⊢ P b
```

which matches `hp`.

## Rewriting with Definitions

You can rewrite using definitions if the definition has a theorem-like unfolding rule.

```lean
def twice (n : Nat) : Nat :=
  n + n
```

```lean
theorem rw_definition (n : Nat) : twice n = n + n := by
  rfl
```

Usually, `rfl` is enough when both sides are definitionally equal.

If Lean does not unfold automatically, use `unfold`.

```lean
theorem rw_unfold_definition (n : Nat) : twice n = n + n := by
  unfold twice
  rfl
```

## Rewriting and Simplification

`rw` applies the rules you give it. `simp` applies a larger collection of simplification rules.

```lean
theorem rw_needs_rule (n : Nat) : n + 0 = n := by
  rw [Nat.add_zero]
```

The same theorem can be proved by:

```lean
theorem simp_same_goal (n : Nat) : n + 0 = n := by
  simp
```

Use `rw` when you want explicit control. Use `simp` when the goal should reduce by standard simplification.

## Rewriting Can Fail

A rewrite fails when Lean cannot find a matching expression.

```lean
-- This fails:
-- theorem rw_no_match
--     (a b c : Nat)
--     (h : a = b) :
--     c + 1 = c + 1 := by
--   rw [h]
```

The goal contains no occurrence of `a`, so `rw [h]` has nothing to rewrite.

This kind of failure usually means one of three things: the rewrite direction is wrong, the expression is hidden under a definition, or the expression has a different shape than expected.

## Common Patterns

To rewrite the goal:

```lean
rw [h]
```

To rewrite backward:

```lean
rw [← h]
```

To rewrite in a hypothesis:

```lean
rw [h] at hp
```

To rewrite everywhere:

```lean
rw [h] at *
```

To rewrite several rules:

```lean
rw [h₁, h₂, Nat.add_zero]
```

To rewrite one occurrence:

```lean
nth_rewrite 1 [h]
```

## Common Pitfalls

Do not use `rw` when no matching expression exists. Inspect the goal first.

Do not rewrite everywhere unless you want every matching occurrence changed.

Do not assume `rw [h]` and `rw [← h]` are interchangeable. Direction matters.

Do not use `simp` when you need exact step-by-step control. It may solve the goal, but it can hide the proof shape.

## Takeaway

Rewriting is controlled substitution. A proof of equality gives a rewrite rule. The command `rw [h]` applies that rule to the goal, `rw [h] at hp` applies it to a hypothesis, and `rw [← h]` reverses the direction. Most elementary equality proofs in Lean are built from these moves.