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:

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:

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:

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:

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:

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:

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:

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:

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.