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

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.

  1. 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.

  2. 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 ↔.