`nth_rewrite`

tactic #

The tactic `nth_rewrite`

and `nth_rw`

are variants of `rewrite`

and `rw`

that only performs the
`n`

th possible rewrite.

`nth_rewrite`

is a variant of `rewrite`

that only changes the `n₁, ..., nₖ`

ᵗʰ *occurrence* of
the expression to be rewritten. `nth_rewrite n₁ ... nₖ [eq₁, eq₂,..., eqₘ]`

will rewrite the
`n₁, ..., nₖ`

ᵗʰ *occurrence* of each of the `m`

equalities `eqᵢ`

in that order. Occurrences are
counted beginning with `1`

in order of precedence.

For example,

```
example (h : a = 1) : a + a + a + a + a = 5 := by
nth_rewrite 2 3 [h]
/-
a: ℕ
h: a = 1
⊢ a + 1 + 1 + a + a = 5
-/
```

Notice that the second occurrence of `a`

from the left has been rewritten by `nth_rewrite`

.

To understand the importance of order of precedence, consider the example below

```
example (a b c : Nat) : (a + b) + c = (b + a) + c := by
nth_rewrite 2 [Nat.add_comm] -- ⊢ (b + a) + c = (b + a) + c
```

Here, although the occurrence parameter is `2`

, `(a + b)`

is rewritten to `(b + a)`

. This happens
because in order of precedence, the first occurrence of `_ + _`

is the one that adds `a + b`

to `c`

.
The occurrence in `a + b`

counts as the second occurrence.

If a term `t`

is introduced by rewriting with `eqᵢ`

, then this instance of `t`

will be counted as an
*occurrence* of `t`

for all subsequent rewrites of `t`

with `eqⱼ`

for `j > i`

. This behaviour is
illustrated by the example below

```
example (h : a = a + b) : a + a + a + a + a = 0 := by
nth_rewrite 3 [h, h]
/-
a b: ℕ
h: a = a + b
⊢ a + a + (a + b + b) + a + a = 0
-/
```

Here, the first `nth_rewrite`

with `h`

introduces an additional occurrence of `a`

in the goal.
That is, the goal state after the first rewrite looks like below

```
/-
a b: ℕ
h: a = a + b
⊢ a + a + (a + b) + a + a = 0
-/
```

This new instance of `a`

also turns out to be the third *occurrence* of `a`

. Therefore,
the next `nth_rewrite`

with `h`

rewrites this `a`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`nth_rewrite`

is a variant of `rewrite`

that only changes the `n₁, ..., nₖ`

ᵗʰ *occurrence* of
the expression to be rewritten. `nth_rewrite n₁ ... nₖ [eq₁, eq₂,..., eqₘ]`

will rewrite the
`n₁, ..., nₖ`

ᵗʰ *occurrence* of each of the `m`

equalities `eqᵢ`

in that order. Occurrences are
counted beginning with `1`

in order of precedence.

For example,

```
example (h : a = 1) : a + a + a + a + a = 5 := by
nth_rewrite 2 3 [h]
/-
a: ℕ
h: a = 1
⊢ a + 1 + 1 + a + a = 5
-/
```

Notice that the second occurrence of `a`

from the left has been rewritten by `nth_rewrite`

.

To understand the importance of order of precedence, consider the example below

```
example (a b c : Nat) : (a + b) + c = (b + a) + c := by
nth_rewrite 2 [Nat.add_comm] -- ⊢ (b + a) + c = (b + a) + c
```

Here, although the occurrence parameter is `2`

, `(a + b)`

is rewritten to `(b + a)`

. This happens
because in order of precedence, the first occurrence of `_ + _`

is the one that adds `a + b`

to `c`

.
The occurrence in `a + b`

counts as the second occurrence.

If a term `t`

is introduced by rewriting with `eqᵢ`

, then this instance of `t`

will be counted as an
*occurrence* of `t`

for all subsequent rewrites of `t`

with `eqⱼ`

for `j > i`

. This behaviour is
illustrated by the example below

```
example (h : a = a + b) : a + a + a + a + a = 0 := by
nth_rewrite 3 [h, h]
/-
a b: ℕ
h: a = a + b
⊢ a + a + (a + b + b) + a + a = 0
-/
```

Here, the first `nth_rewrite`

with `h`

introduces an additional occurrence of `a`

in the goal.
That is, the goal state after the first rewrite looks like below

```
/-
a b: ℕ
h: a = a + b
⊢ a + a + (a + b) + a + a = 0
-/
```

This new instance of `a`

also turns out to be the third *occurrence* of `a`

. Therefore,
the next `nth_rewrite`

with `h`

rewrites this `a`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`nth_rw`

is a variant of `rw`

that only changes the `n₁, ..., nₖ`

ᵗʰ *occurrence* of the expression
to be rewritten. Like `rw`

, and unlike `nth_rewrite`

, it will try to close the goal by trying `rfl`

afterwards. `nth_rw n₁ ... nₖ [eq₁, eq₂,..., eqₘ]`

will rewrite the `n₁, ..., nₖ`

ᵗʰ *occurrence* of
each of the `m`

equalities `eqᵢ`

in that order. Occurrences are counted beginning with `1`

in
order of precedence. For example,

```
example (h : a = 1) : a + a + a + a + a = 5 := by
nth_rw 2 3 [h]
/-
a: ℕ
h: a = 1
⊢ a + 1 + 1 + a + a = 5
-/
```

Notice that the second occurrence of `a`

from the left has been rewritten by `nth_rewrite`

.

To understand the importance of order of precedence, consider the example below

```
example (a b c : Nat) : (a + b) + c = (b + a) + c := by
nth_rewrite 2 [Nat.add_comm] -- ⊢ (b + a) + c = (b + a) + c
```

Here, although the occurrence parameter is `2`

, `(a + b)`

is rewritten to `(b + a)`

. This happens
because in order of precedence, the first occurrence of `_ + _`

is the one that adds `a + b`

to `c`

.
The occurrence in `a + b`

counts as the second occurrence.

If a term `t`

is introduced by rewriting with `eqᵢ`

, then this instance of `t`

will be counted as an
*occurrence* of `t`

for all subsequent rewrites of `t`

with `eqⱼ`

for `j > i`

. This behaviour is
illustrated by the example below

```
example (h : a = a + b) : a + a + a + a + a = 0 := by
nth_rw 3 [h, h]
/-
a b: ℕ
h: a = a + b
⊢ a + a + (a + b + b) + a + a = 0
-/
```

Here, the first `nth_rw`

with `h`

introduces an additional occurrence of `a`

in the goal. That is,
the goal state after the first rewrite looks like below

```
/-
a b: ℕ
h: a = a + b
⊢ a + a + (a + b) + a + a = 0
-/
```

This new instance of `a`

also turns out to be the third *occurrence* of `a`

. Therefore,
the next `nth_rw`

with `h`

rewrites this `a`

.

Further, `nth_rw`

will close the remaining goal with `rfl`

if possible.

## Equations

- One or more equations did not get rendered due to their size.