rw expression IN expression

Question

Say, I need:

rw ← nat.mul_one (d+d),

But there are multiple (d+d) in the whole goal. Can I do something like:

rw ← nat.mul_one (d+d) in (5+(d+d)),

so that (d+d) is rewritten only where the full expression in parentheses is 5+(d+d) is matched?

Answer 1

You can try mathlib's nth_rewrite, or rw's optional occs argument. For example:

if ⊢ (d + d) + 5 * (d + d) + 2 * (d + d) = 8 * (d + d), then nth_rewrite ←nat.mul_one (d + d) 1 should work, as should rw ←nat.mul_one (d + d) { occs := occurrences.pos [2]} (note that nth_rewrite is zero-indexed whilst rw is 1-indexed).

You can also mess around with conv, but I don't recommend that; something that would work for the above example with conv is conv { congr, congr, congr, skip, rw ←nat.mul_one (d + d) }.

Answer 2

You can either learn about the joys of conv mode here, which enable you to do targetted rewriting, or you can use the nth_rewrite tactic documented here which will let you choose precisely which of the d+ds you want to change.