rw single instance in goal

Stream: general

[Steven Moreland]

If I have a goal like a + b = a and I have add_zero (a : \N) : a + 0 = a. Is it possible to rewrite this to say a + b = a + 0 instead of a + 0 + b = a + 0 (e.g. from rw \l add_zero a). I have not figured out how to specify this.

[Shing Tak Lam]

Conv mode can do this. You can specify where exactly to rewrite.

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

[Shing Tak Lam]

Also what are you trying to prove here? If it is that b = 0 then there is an existing lemma called add_right_eq_self.

[Steven Moreland]

Thank you for your kind and quick answer, this is what I was looking for. I'm trying to prove existing theorems, yes. As you can see, I am quite new to this tool. Thanks again.

[Shing Tak Lam]

No problem. I'm quite new to this as well, I only really got started a week or two ago. Have you seen the Natural Numbers Game yet? This is one of the levels there.

[Steven Moreland]

Yes, I saw this yesterday :) Although, trying to hide n00bness with s/mynat/\N/ when posting here.