Applying rewrite to the nth match?

Stream: new members

[Christopher Hoskin]

Sometimes I find myself trying to do something like rw ← add_zero a to replace a with a+0 in a goal. But I only want to do this for a particular occurrence of a in the goal, whereas rewrite replaces every occurrence. Is there a way to do this?

Thanks,

Christopher

[Bryan Gin-ge Chen]

In mathlib there's nth_rewrite. There's also conv mode which is more powerful but often more verbose.

[Christopher Hoskin]

Thanks! nth_rewrite is just what I was looking for.