# 4.9 Rewriting with Hypotheses

# 4.9 Rewriting with Hypotheses

In most proofs, equalities come from the local context. A hypothesis `h : a = b` is a rewrite rule that you control. The tactic `rw` applies it directly; `simp` can use it as part of normalization. This section focuses on disciplined use of hypotheses to keep proofs local and predictable.

The basic use is direct replacement in the goal:

```lean
example (a b : Nat) (h : a = b) :
  a + 2 = b + 2 := by
  rw [h]
```

Orientation is explicit. If the goal requires the reverse direction, use:

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

Prefer choosing the direction that moves the goal toward a canonical form. This reduces later work and aligns with `simp`.

You can rewrite inside hypotheses. This is often necessary to normalize premises before using them:

```lean
example (a b : Nat) (h : a = b) (H : a + 1 = 5) :
  b + 1 = 5 := by
  rw [h] at H
  exact H
```

The step `rw [h] at H` updates `H` in place. After normalization, the goal can be discharged directly.

Rewriting both goal and context is common:

```lean
example (a b c : Nat)
  (h₁ : a = b) (h₂ : b = c)
  (H : a + 1 = 7) :
  c + 1 = 7 := by
  rw [h₁] at H
  rw [h₂]
  exact H
```

Order matters. Each rewrite changes the shape of the remaining expressions. Apply rewrites so that later steps match structurally.

When a hypothesis should be used repeatedly, it is often better to normalize the context once:

```lean
example (a b : Nat) (h : a = b)
  (H₁ : a + 1 = 3) (H₂ : a + 2 = 4) :
  b + 1 = 3 ∧ b + 2 = 4 := by
  rw [h] at H₁ H₂
  constructor <;> assumption
```

This keeps subsequent steps simple and avoids repeated rewrites.

`simp` can incorporate hypotheses as rewrite rules:

```lean
example (a b : Nat) (h : a = b) :
  a + 0 = b := by
  simp [h]
```

This both applies `h` and normalizes `a + 0`. The bracket form is preferred when the goal is primarily normalization with a few contextual equalities.

A common pattern is to derive a local equality and use it immediately:

```lean
example (a b : Nat) (h : a = b) :
  a + a = b + b := by
  have h' : a + a = b + a := by
    rw [h]
  rw [h']    -- now goal is b + a = b + b
  rw [h]
```

This decomposes a larger rewrite into smaller, verifiable steps. It is useful when direct rewriting does not match the entire goal.

Rewriting can fail when the target is not syntactically present. In such cases, restructure the goal or expose the subterm:

```lean
example (a b : Nat) (h : a = b) :
  (fun x => x + a) 3 = (fun x => x + b) 3 := by
  rw [h]
```

If the occurrence is hidden under a binder, introduce variables or use extensionality before rewriting.

Avoid global, indiscriminate rewriting. Keep changes local to the goal or specific hypotheses. This reduces unintended interactions and makes proofs stable under refactoring.

A useful workflow is:

1. Normalize hypotheses with `rw` or `simp`.
2. Apply the main step of the proof.
3. Normalize the goal to a canonical form.
4. Close with `rfl`, `simp`, or a direct lemma.

In summary, hypotheses act as local rewrite rules. Apply them with explicit direction, normalize the context early, and keep rewrites small and targeted. This keeps proofs linear and reduces backtracking.