Module 2 · Lesson 2

rw — Rewriting

rw replaces one term with an equal term in your goal. It is how you use an equation you already have: a hypothesis, a definition, or a library lemma.

The Basic Idea

If you know a = b, you can replace awith b anywhere in your goal. This is the fundamental principle of substitution in equality reasoning:

lean

Try it

1example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
2  rw [h]
3  -- Goal was: a + 1 = b + 1
4  -- After rw: b + 1 = b + 1, which rw closes by trying rfl
5
6example (x y : Nat) (h : x = y) : x * x = y * y := by
7  rw [h]
8  -- Both x's get replaced with y
9  -- Goal: y * y = y * y, closed by rfl

The rw [h] tactic finds a in the goal and replaces it with b (because h : a = b). All occurrences are replaced by default. After rewriting, rw triesrfl, so a goal that becomes trivially true is closed for you; writing another rfl afterwards is an error ("no goals to be solved").

When to Use rw

Reach for rw when you:

Have an equality hypothesis: You have h : a = band need to substitute
Know a useful lemma: A library lemma like Nat.add_zerocan simplify your goal
Need precise control: Unlike simp, you control exactly what gets rewritten
Want step-by-step transformation: Building a proof by gradually transforming the goal

Key Takeaway

rw [h] replaces left→right: if h : a = b, it replaces a with b.
rw [← h] replaces right→left: replaces bwith a.

Direction Matters

By default, rw replaces the left side with the right side. Sometimes you need to go the other direction. Use ←(typed as \l or \leftarrow):

lean

Try it

1example (a b : Nat) (h : a = b) : b = a := by
2  rw [h]      
3  -- h says a = b, so we replace a with b
4  -- Goal: b = b ✓
5
6example (a b : Nat) (h : a = b) : b + 1 = a + 1 := by
7  rw [← h]    -- ← reverses direction: replace b with a
8              -- Goal becomes: a + 1 = a + 1, closed by rfl
9
10-- When to use ←:
11example (x y : Nat) (h : x = y + 1) : y + 1 = x := by
12  rw [← h]  -- Replace y + 1 (RHS of h) with x

Using Library Lemmas

You can rewrite with named lemmas from the library. This is how you use standard mathematical facts in your proofs:

lean

Try it

1example (n : Nat) : n + 0 = n := by
2  rw [Nat.add_zero]
3  -- Nat.add_zero : ∀ n, n + 0 = n
4  -- Replaces n + 0 with n
5
6example (a b : Nat) : a + b = b + a := by
7  rw [Nat.add_comm]
8  -- Nat.add_comm : ∀ a b, a + b = b + a
9  -- Goal becomes: b + a = b + a
10
11example (n : Nat) : 0 + n = n := by
12  rw [Nat.zero_add]
13  -- Nat.zero_add : ∀ n, 0 + n = n
14
15example (a b c : Nat) : (a + b) + c = a + (b + c) := by
16  rw [Nat.add_assoc]
17  -- Nat.add_assoc : ∀ a b c, (a + b) + c = a + (b + c)

Multiple Rewrites

Chain rewrites in a single rw call for cleaner proofs:

lean

Try it

1example (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by
2  rw [h1, h2]
3  -- First: replace a with b → Goal: b = c
4  -- Then: replace b with c → Goal: c = c
5
6example (n : Nat) : 0 + n + 0 = n := by
7  rw [Nat.zero_add, Nat.add_zero]
8  -- First: 0 + n → n, giving: n + 0 = n
9  -- Then: n + 0 → n, giving: n = n
10
11-- Order matters!
12example (a b : Nat) : (a + 0) + b = b + a := by
13  rw [Nat.add_zero, Nat.add_comm]
14  -- First: a + 0 → a, giving: a + b = b + a  
15  -- Then: a + b → b + a, giving: b + a = b + a

Rewriting in Hypotheses

Use rw [...] at h to rewrite in a hypothesis instead of the goal:

lean

Try it

1example (a b : Nat) (h1 : a = b) (h2 : a + 1 = 5) : b + 1 = 5 := by
2  rw [h1] at h2
3  -- Before: h2 : a + 1 = 5
4  -- After:  h2 : b + 1 = 5
5  exact h2
6
7example (n : Nat) (h : n + 0 = 5) : n = 5 := by
8  rw [Nat.add_zero] at h
9  -- h becomes: n = 5
10  exact h
11
12-- Rewrite at multiple hypotheses
13example (a b : Nat) (h : a = b) (h1 : a > 0) (h2 : a < 10) : b > 0 ∧ b < 10 := by
14  rw [h] at h1 h2
15  exact ⟨h1, h2⟩

Rewriting Everywhere

lean

Try it

1example (a b : Nat) (h : a = b) (h2 : a + a = 10) : b + b = 10 := by
2  rw [h] at *
3  -- Rewrites in ALL hypotheses and the goal
4  exact h2

Common Mistakes

Mistake 1: Wrong direction

lean

Try it

1example (a b : Nat) (h : a = b) : b = a := by
2  -- rw [h] works here, but why?
3  -- h : a = b, so we look for 'a' in goal 'b = a'
4  -- Wait, there's no 'a' on the left... but there IS on the right!
5  -- rw replaces ALL occurrences of 'a' with 'b'
6  rw [h]  -- Goal: b = b, closed by rfl
7
8-- More intuitive approach:
9example (a b : Nat) (h : a = b) : b = a := by
10  rw [← h]  -- Explicitly swap: replace b with a; goal a = a is closed by rfl

Mistake 2: Rewriting something that doesn't exist

lean

Try it

1-- If the LHS of the equation isn't in your goal, rw does nothing
2example (x : Nat) : x = x := by
3  -- rw [Nat.add_zero]  -- ❌ Error: can't find n + 0 in goal
4  rfl  -- ✓ Just use rfl
5
6-- Make sure the lemma matches what's in your goal!

Mistake 3: Forgetting that rw replaces ALL occurrences

lean

1example (a b : Nat) (h : a = b) : a + a = b + b := by
2  rw [h]  -- Replaces BOTH a's with b
3  -- Goal: b + b = b + b ✓
4
5-- If you only want to rewrite one occurrence, use nth_rewrite (Mathlib)
6example (a : Nat) : a + a = a + a := by
7  nth_rewrite 1 [← Nat.add_zero a]  -- Only rewrite first 'a'
8  rw [Nat.add_zero]

Common Lemmas for Rewriting

Addition

lean

Try it

1#check Nat.add_zero      -- n + 0 = n
2#check Nat.zero_add      -- 0 + n = n
3#check Nat.add_comm      -- a + b = b + a
4#check Nat.add_assoc     -- (a + b) + c = a + (b + c)
5#check Nat.succ_add      -- (n + 1) + m = (n + m) + 1
6#check Nat.add_succ      -- n + (m + 1) = (n + m) + 1

Multiplication

lean

Try it

1#check Nat.mul_zero      -- n * 0 = 0
2#check Nat.zero_mul      -- 0 * n = 0
3#check Nat.mul_one       -- n * 1 = n
4#check Nat.one_mul       -- 1 * n = n
5#check Nat.mul_comm      -- a * b = b * a
6#check Nat.mul_assoc     -- (a * b) * c = a * (b * c)
7#check Nat.mul_add       -- a * (b + c) = a * b + a * c

Lists

lean

Try it

1#check List.append_nil   -- xs ++ [] = xs
2#check List.nil_append   -- [] ++ xs = xs
3#check List.append_assoc -- (xs ++ ys) ++ zs = xs ++ (ys ++ zs)
4#check List.length_append -- (xs ++ ys).length = xs.length + ys.length

💡

Use #check to see a lemma's type. The type tells you exactly what it can rewrite. You can also use rw? to have Lean suggest rewrites automatically.

rw vs simp

When should you use rw vs simp?

lean

Try it

1-- rw: precise control, one rewrite at a time
2example (n : Nat) : n + 0 = n := by
3  rw [Nat.add_zero]
4
5-- simp: automatic, applies many simplifications
6example (n : Nat) : n + 0 = n := by
7  simp  -- Automatically uses Nat.add_zero
8
9-- simp is more powerful but less predictable
10example (a b : Nat) : a + 0 + b + 0 = b + a := by
11  simp [Nat.add_comm]  -- Handles everything
12
13-- rw gives you step-by-step control
14example (a b : Nat) : a + 0 + b + 0 = b + a := by
15  rw [Nat.add_zero, Nat.add_zero, Nat.add_comm]

	rw	simp
Control	Precise	Automatic
Rewrites	Exactly what you specify	Many at once
Predictability	High	Can be surprising
Use when	You know the exact steps	Goal is "obviously" simplifiable

Deep Dive: How rw Finds Subterms

rw searches the goal for the left-hand side of the equality and replaces the first match. If there are multiple matches, you can control which one using nth_rewrite:

lean

1example (a : Nat) : a + a = a + a := by
2  rw [Nat.add_comm]  -- Rewrites a + a to a + a (no visible change!), then rfl closes it
3
4-- Use nth_rewrite to target specific occurrences
5example (a b : Nat) : a + b + (a + b) = (b + a) + (a + b) := by
6  nth_rewrite 1 [Nat.add_comm]  -- Only rewrite the first a + b (Mathlib)
7
8-- You can also use conv for fine-grained control
9example (a b : Nat) : (a + b) + (a + b) = (a + b) + (b + a) := by
10  conv => rhs; rhs; rw [Nat.add_comm]

Real-World Example: Proving Associativity

lean

Try it

1-- A step-by-step proof using rw
2theorem list_append_assoc (xs ys zs : List α) : 
3    (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by
4  induction xs with
5  | nil => 
6    rw [List.nil_append, List.nil_append]
7    -- ([] ++ ys) ++ zs = [] ++ (ys ++ zs)
8    -- After rewrites: ys ++ zs = ys ++ zs
9  | cons h t ih =>
10    rw [List.cons_append, List.cons_append, List.cons_append]
11    rw [ih]
12    -- Use induction hypothesis

Exercise 1: Chain Rewrites

Use rw with two lemmas to simplify the goal.

lean

Try it

1example (a b : Nat) : 0 + a + b = b + a := by
2  rw [Nat.zero_add, Nat.add_comm]

Exercise 2: Rewrite in Hypothesis

Rewrite in the hypothesis to match the goal.

lean

Try it

1example (a b : Nat) (h1 : a = b) (h2 : a + 5 = 10) : b + 5 = 10 := by
2  rw [h1] at h2
3  exact h2

Exercise 3: Use the Arrow

Use ← to rewrite in the reverse direction.

lean

Try it

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

rfl — Reflexivity Next: simp — Simplification