nth_rw

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_rw. For example nth_rw 2 [h] will change only the second a into b.

Examples

  1. Faced with

h : x = y
 x * x = a

the tactic nth_rw 1 [h] will turn the goal into y * x = a and nth_rw 2 [h] will turn it into x * y = a. Compare with rw [h] which will turn it into y * y = a.

  1. nth_rw works on hypotheses too. If h : x = y is a hypothesis and h2 : x * x = a then nth_rw 1 [h] at h2 will change h2 to y * x = a.

  2. Just like rw, nth_rw accepts h if you want to change the right hand side of h to the left hand side.