# `nth_rewrite` tactic #

The tactic `nth_rewrite` and `nth_rw` are variants of `rewrite` and `rw` that only performs the `n`th possible rewrite.

source
def Mathlib.Tactic.tacticNth_rewrite_____ :
Lean.ParserDescr

`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 and third occurrences of `a` from the left have 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

source
def Mathlib.Tactic.tacticNth_rw_____ :
Lean.ParserDescr

`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 and third occurrences of `a` from the left have been rewritten by `nth_rw`.

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.

Instances For