# 4.23 Rewriting in Goals vs Hypotheses

# 4.23 Rewriting in Goals vs Hypotheses

Rewriting can target either the goal or the local context. The choice affects proof shape, automation, and stability. In Lean, both are first-class operations; disciplined use keeps proofs linear and predictable.

## Rewriting the goal

Rewriting the goal transforms the target statement directly:

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

This is appropriate when a single step aligns the goal with a canonical form or with a known lemma. Prefer this when the change is local and obvious.

## Rewriting hypotheses

Rewriting hypotheses normalizes premises before they are used:

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

This is often more effective when multiple uses of a premise are expected. Normalize once, then reuse.

## Rewriting both

Many proofs benefit from normalizing both sides:

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

The context is aligned first, then the goal is adjusted.

## Global normalization

When several hypotheses share the same shape, normalize them together:

```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 avoids repeated rewrites and keeps the context consistent.

For broader normalization, use:

```lean
simp at *
```

This applies simplification to all hypotheses and the goal. Use with care; it can obscure intermediate structure.

## Choosing direction and location

A practical rule:

* If a hypothesis already matches the goal after rewriting, rewrite the hypothesis.
* If the goal should match a canonical form, rewrite the goal.
* If both are far from canonical, normalize the context first, then the goal.

Direction still matters. Choose the orientation that reduces complexity or aligns with available data.

## Avoiding duplication

Repeated rewriting of the same hypothesis is inefficient and brittle:

```lean
-- avoid
rw [h] at H₁
rw [h] at H₂
rw [h]
```

Instead, normalize once:

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

or group rewrites:

```lean
rw [h] at H₁ H₂
```

## Interaction with `simp`

`simp` can handle both goals and hypotheses:

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

Use `simp` when normalization is the main task. Use `rw` for targeted transformations.

## Stability under refactoring

Rewriting in hypotheses often yields more stable proofs. The goal remains close to its original form, while the context is adjusted to fit it. This reduces the risk that small changes in the goal break earlier steps.

## Summary

Rewriting can target the goal, the context, or both. Normalize hypotheses when they are reused, normalize the goal when aiming for a canonical form, and avoid redundant rewrites. Controlled placement of rewriting steps keeps proofs concise and maintainable.