# Documentation

Mathlib.Tactic.NthRewrite

# nth_rewrite tactic #

The tactic nth_rewrite and nth_rw are variants of rewrite and rw that only performs the nth 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.
def Mathlib.Tactic.rewriteLocalDecl' (stx : Lean.Syntax) (symm : Bool) (fvarId : Lean.FVarId) (config : optParam Lean.Meta.Rewrite.Config { transparency := Lean.Meta.TransparencyMode.reducible, offsetCnstrs := true }) :

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.