# 4.22 Rewriting with `conv`

# 4.22 Rewriting with `conv`

The `conv` tactic provides fine-grained control over rewriting by allowing you to navigate inside an expression and apply transformations at a precise location. In Lean, `conv` is used when `rw` or `simp` either affect too much or fail to reach the intended subterm.

## Basic structure

A `conv` block focuses on a specific part of the goal:

```lean
conv =>
  lhs
  rw [h]
```

This restricts rewriting to the left-hand side of the goal. Similarly:

```lean
conv =>
  rhs
  rw [h]
```

targets the right-hand side.

## Navigating expressions

Inside `conv`, you can descend into subterms using `congr`, which mirrors the structure of the expression:

```lean
example (a b : Nat) (h : a = b) :
  (a + 1) * 2 = (b + 1) * 2 := by
  conv =>
    lhs
    congr
    rw [h]
  rfl
```

The `congr` step moves into the argument of multiplication, exposing `a + 1`.

You can apply multiple navigation steps:

```lean
conv =>
  lhs
  congr
  congr
  rw [h]
```

Each `congr` descends one level deeper.

## Rewriting specific occurrences

When a term appears multiple times, `conv` allows you to rewrite only one occurrence:

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

Only the first `a` is rewritten.

## Combining with simplification

You can use `simp` inside `conv`:

```lean
example (a : Nat) :
  (a + 0) + 1 = a + 1 := by
  conv =>
    lhs
    simp
  rfl
```

This simplifies a subexpression without affecting the rest of the goal.

## Rewriting under binders

`conv` can reach inside binders without introducing variables:

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

This avoids explicit use of `funext` in simple cases, though extensionality is often clearer for function equality.

## Working with nested structures

For deeply nested expressions, `conv` provides a path-based approach:

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

Each `congr` step moves inward.

## Practical guidance

* Use `conv` when `rw` affects too many occurrences.
* Use `conv` when rewriting must target a deeply nested subterm.
* Keep navigation steps explicit and minimal.
* Prefer `rw` or `simp` for simple cases; reserve `conv` for precision work.
* Combine `conv` with `simp` for local normalization.

## Summary

`conv` provides precise control over where rewriting occurs. It allows you to navigate expression structure and apply transformations exactly where needed. This is essential when dealing with complex terms where global rewriting is either too aggressive or insufficient.