# 4.12 Rewriting Under Binders

# 4.12 Rewriting Under Binders

Rewriting becomes more subtle when the target term appears inside a binder such as a lambda, a universal quantifier, or an existential. In these cases, the occurrence is not directly accessible to `rw` because the term is abstracted over a variable. In Lean, the standard approach is to expose the body of the binder before rewriting.

The simplest example is function equality. Suppose you want to rewrite inside a lambda:

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

The tactic `funext` reduces equality of functions to pointwise equality. After introducing `x`, the goal becomes `x + a = x + b`, where rewriting applies directly.

The same principle applies to universal quantifiers:

```lean
example (a b : Nat) (h : a = b) :
  (∀ x, x + a = x + b) := by
  intro x
  rw [h]
```

The binder is opened with `intro`, exposing the body. Rewriting then proceeds as usual.

For existential statements, rewriting often occurs after destructuring:

```lean
example (a b : Nat) (h : a = b)
  (H : ∃ x, x + a = 5) :
  ∃ x, x + b = 5 := by
  cases H with
  | intro x hx =>
      exists x
      rw [h] at hx
      exact hx
```

Here the existential is unpacked with `cases`, producing a witness `x` and a proof `hx`. The hypothesis is rewritten, and the result is reassembled.

Rewriting under dependent binders requires attention to types. If a term appears in a type, rewriting may change the type of subsequent expressions. Lean handles this through transport, but the user must expose the dependency:

```lean
example (a b : Nat) (h : a = b)
  (P : Nat -> Prop)
  (H : P a) :
  P b := by
  rw [← h]
  exact H
```

The rewrite changes the goal from `P b` to `P a`, which matches the hypothesis. The direction is chosen to align the types.

In some cases, rewriting under binders is not directly possible because the structure is too opaque. The `conv` tactic provides a way to focus on a specific subterm:

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

The `conv` block navigates the expression tree, applies rewriting at a chosen location, and returns to the main goal. This is useful when standard rewriting does not reach the desired occurrence.

Another approach is to refactor the expression to expose the subterm. For example, applying a function or introducing a variable often reveals the structure needed for rewriting.

A practical guideline is:

1. Open binders using `intro`, `cases`, or `funext`.
2. Rewrite in the exposed body.
3. Reassemble the structure if necessary.

Avoid attempting to rewrite deeply nested terms without exposing their structure. This leads to brittle proofs and difficult debugging.

In summary, rewriting under binders requires making the hidden term explicit. Once exposed, the usual rewriting tools apply. The combination of binder elimination and local rewriting provides a systematic approach to these situations.