`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 nth occurrence of the expression
to be rewritten.

Note: The occurrences are counted beginning with `1`

and not `0`

, this is different than in
mathlib3. The translation will be handled by mathport.

## Instances For

`nth_rewrite`

is a variant of `rewrite`

that only changes the nth occurrence of the expression
to be rewritten.

Note: The occurrences are counted beginning with `1`

and not `0`

, this is different than in
mathlib3. The translation will be handled by mathport.

## Instances For

`nth_rw`

is like `nth_rewrite`

, but also tries to close the goal by trying `rfl`

afterwards.