`nth_rewrite`

tactic #

The tactic `nth_rewrite`

and `nth_rw`

are variants of `rewrite`

and `rw`

that only performs the
`n`

th possible rewrite.

Variant of `rewriteTarget`

that allows to use `Occurrences`

.

This def should be in Core.

## Equations

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

Variant of `rewriteLocalDecl`

that allows to use `Occurrences`

.

This def should be in Core.

## Equations

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

`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.

## Equations

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

`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.

## Equations

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

`nth_rw`

is like `nth_rewrite`

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

afterwards.

## Equations

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