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
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
.
nth_rw
works on hypotheses too. Ifh : x = y
is a hypothesis andh2 : x * x = a
thennth_rw 1 [h] at h2
will changeh2
toy * x = a
.Just like
rw
,nth_rw
accepts← h
if you want to change the right hand side ofh
to the left hand side.