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.

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.

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:

⊢ b + 1 = b + 1

Lean closes the goal by reflexivity.

Rewriting Direction

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

h : a = b

means:

replace a with b

To rewrite in the other direction, use ←.

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:

⊢ a + 1 = a + 1

Rewriting in a Hypothesis

Use at to rewrite inside a hypothesis.

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:

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

After:

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.

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.

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.

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:

Nat.add_comm

which states commutativity of addition.

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.

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

You can also provide arguments explicitly when needed.

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.

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.

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.

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.

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.

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.

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:

⊢ P a

to:

⊢ P b

which matches hp.

Rewriting with Definitions

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

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

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.

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.

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

The same theorem can be proved by:

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.

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

rw [h]

To rewrite backward:

rw [← h]

To rewrite in a hypothesis:

rw [h] at hp

To rewrite everywhere:

rw [h] at *

To rewrite several rules:

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

To rewrite one occurrence:

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.