nth_rewrite tactic

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

def Mathlib.Tactic.nthRewriteSeq : Lean.ParserDescr

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.

def Mathlib.Tactic.evalNthRewriteSeq : Lean.Elab.Tactic.Tactic

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.

def Mathlib.Tactic.nthRwSeq : Lean.ParserDescr

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.