rewrite at a specific variable?

Stream: Is there code for X?

[唐乾]

For example,I want to rw the rhs of"a+b=a" to "a+b=a+0"conveniently,what should I do?
I found that there is an intro. in
https://leanprover.github.io/tutorial/A1_Quick_Reference.html
which said"t at H {i, ...} : apply t only at numbered occurences in H"
but I don't know what is "i" means,and other ref. didn't explain this.

[Patrick Massot]

The first line of this document says: "Note that this quick reference guide describes Lean 2 only. "

[Patrick Massot]

Are you using Lean 2?

[Patrick Massot]

If you don't know then the answer is no.

[唐乾]

oh! I'm using Lean 3,is there anyway in Lean 3?

[Kevin Buzzard]

Yes, you can do targetted rewrites in several ways in Lean 3

[Kevin Buzzard]

https://leanprover-community.github.io/extras/conv.html

[Kyle Miller]

example (a b : ℕ) (h : a+b=a) : true :=
begin
  conv_rhs at h { rw ←nat.add_zero a },
end

(the true there is just a placeholder)

[Patrick Massot]

For the record, you can also do rw ← nat.add_zero a at h {occs := occurrences.pos [2]}, which is closer to what this ancient doc was referring to.

[唐乾]

thx!!It works !!!