.. _tac_nth_rewrite:

nth_rewrite
===========

Summary
-------

If ``h : a = b`` then ``rw h`` turns *all* ``a`` s in the goal to ``b`` s. If you only want to turn one of the ``a`` s into a ``b``, use ``nth_rewrite``. For example ``nth_rewrite 2 h`` will change only the third ``a`` into ``b``, and ``nth_rewrite 0 h`` will turn only the first one.

Examples
--------

1) Faced with

.. code-block::

   h : x = y
   ⊢ x * x = a

the tactic ``nth_rewrite 0 h`` will turn the goal into ``⊢ y * x = a`` and ``nth_rewrite 1 h`` will turn it into ``⊢ x * y = a``. Compare with ``rw h`` which will turn it into ``⊢ y * y = a``.

2) ``nth_rewrite`` works on hypotheses too. If ``h : x = y`` is a hypothesis and ``h2 : x * x = a`` then ``nth_rewrite 0 h at h2`` will change ``h2`` to ``y * x = a``.

3) Just like ``rw``, ``nth_rewrite`` accepts ``← h3`` if you want to change the right hand side of ``h3`` to the left hand side.
   
Further notes
-------------

Variants of ``nth_rewrite`` are ``nth_rewrite_lhs`` and ``nth_rewrite_rhs`` which operate only on the left hand or right hand side of an ``=`` or ``↔``.