# 2.23 Rewriting Strategies

Rewriting with equality is one of the most frequent operations in Lean. At scale, the challenge is not knowing that `rw` exists, but deciding **what to rewrite, where, and in which direction** so the proof remains stable and readable.

## Problem

You have equalities available, but naive rewriting:

* fails because the shape does not match
* succeeds but makes the goal harder
* applies too broadly and breaks later steps

You need a disciplined approach.

## Core Strategy

Before rewriting, answer three questions:

1. Where is the mismatch between goal and context?
2. Which equality aligns them?
3. In which direction should it be applied?

## Aligning Goal and Hypotheses

A common pattern is aligning a hypothesis to match the goal.

```lean
theorem rewrite_align_goal
    (a b : Nat)
    (hAB : a = b)
    (ha : a + 1 = 5) :
    b + 1 = 5 := by
  rw [hAB] at ha
  exact ha
```

Instead of rewriting the goal, rewrite the hypothesis so it directly solves the goal.

## Rewriting the Goal

When the goal differs by a known equality, rewrite the goal.

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

After rewriting, the goal becomes reflexive.

## Choosing Direction

Direction is often the main decision.

```lean
hAB : a = b
```

* `rw [hAB]` replaces `a` with `b`
* `rw [← hAB]` replaces `b` with `a`

Example:

```lean
theorem rewrite_direction
    (a b : Nat)
    (hAB : a = b)
    (hb : b + 1 = 5) :
    a + 1 = 5 := by
  rw [← hAB]
  exact hb
```

If rewriting fails, try reversing direction first.

## Rewriting to Simplify

Often rewriting is used to reduce expressions to canonical forms.

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

Or:

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

Rewrite until the expression reaches a normal form.

## Combining with `simp`

`simp` applies many rewrite rules automatically.

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

Guideline:

* use `rw` when you want control
* use `simp` when the transformation is standard

You can combine them:

```lean
theorem rewrite_then_simp (a b : Nat)
    (hAB : a = b) :
    a + 0 = b := by
  rw [hAB]
  simp
```

## Rewriting Multiple Equalities

Apply rewrites in sequence.

```lean
theorem rewrite_chain
    (a b c : Nat)
    (hAB : a = b)
    (hBC : b = c) :
    a + 1 = c + 1 := by
  rw [hAB, hBC]
```

Order matters. Each rewrite transforms the goal for the next step.

## Rewriting Inside Hypotheses

Sometimes the goal is already correct, but a hypothesis needs adjustment.

```lean
theorem rewrite_inside_hyp
    (a b : Nat)
    (hAB : a = b)
    (ha : a + 2 = 7) :
    b + 2 = 7 := by
  rw [hAB] at ha
  exact ha
```

This avoids modifying the goal unnecessarily.

## Rewriting Everywhere

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

This rewrites both the goal and all hypotheses.

Use with care. It may introduce unwanted changes.

## Controlling Occurrences

By default, all matching occurrences are rewritten.

```lean
theorem rewrite_all_occurrences
    (a b : Nat)
    (hAB : a = b) :
    a + a = b + b := by
  rw [hAB]
```

To rewrite a single occurrence:

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

This is useful when full rewriting overshoots the target.

## Rewriting Under Functions

Rewriting works inside expressions.

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

Lean propagates the equality through function application.

## Rewriting Predicates

Rewriting also works for propositions.

```lean
theorem rewrite_predicate
    (a b : Nat)
    (P : Nat -> Prop)
    (hAB : a = b)
    (ha : P a) :
    P b := by
  rw [hAB] at ha
  exact ha
```

This is transport of proofs along equality.

## Rewriting to Match a Lemma

A common use is rewriting so a lemma applies.

```lean
theorem rewrite_for_lemma
    (a b : Nat)
    (hAB : a = b) :
    a + 0 = b := by
  rw [hAB]
  apply Nat.add_zero
```

The rewrite aligns the goal with the lemma.

## Rewriting with Definitions

Definitions may need unfolding.

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

theorem rewrite_definition (n : Nat) :
    double n = n + n := by
  rfl
```

If not automatic:

```lean
theorem rewrite_definition_unfold (n : Nat) :
    double n = n + n := by
  unfold double
  rfl
```

## Rewriting vs `calc`

For longer chains, use `calc`.

```lean
theorem rewrite_calc
    (a b c : Nat)
    (hAB : a = b)
    (hBC : b = c) :
    a = c := by
  calc
    a = b := hAB
    _ = c := hBC
```

This is clearer than a long `rw` sequence.

## Debugging Failed Rewrites

If `rw` fails:

* check if the term actually appears
* check direction
* check if the expression is hidden behind a definition
* try `simp` or `unfold`

Example failure:

```lean
-- no occurrence of a
-- rw [hAB]
```

Lean cannot rewrite what is not present.

## Common Patterns

Rewrite goal:

```lean
rw [h]
```

Rewrite backward:

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

Rewrite hypothesis:

```lean
rw [h] at ha
```

Rewrite many:

```lean
rw [h1, h2, h3]
```

Rewrite everywhere:

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

Rewrite one occurrence:

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

## Common Pitfalls

Do not rewrite blindly. Each rewrite should move the goal toward a simpler or more canonical form.

Do not use `rw` when `simp` expresses the intent better.

Do not rewrite in the wrong direction and make the goal more complex.

Do not apply `rw ... at *` in large contexts without checking side effects.

Do not rely on fragile expression shapes. Minor definition changes can break such proofs.

## Takeaway

Rewriting is controlled substitution guided by equality. Effective use depends on choosing the right direction, location, and sequence. The goal is not to rewrite as much as possible, but to rewrite just enough to align the goal with known facts or canonical forms.