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.

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.

      Instances For