## Stream: new members

### Topic: Sam Estep

#### Sam Estep (Jun 17 2020 at 01:52):

Hi everyone! I've been wanting to learn Lean for a while and now I finally have the time to do so :) I have a noob question: is there a way to do a rw in only part of something? For instance, in Advanced Addition world Level 8/13 of the Natural Number Game, I used this proof:

intro h,
rw ← add_zero a at h,
exact add_left_cancel _ _ _ h,


But I'd like to just write something like this:

intro h,
rw_rhs ← add_zero a at h,
exact add_left_cancel _ _ _ h,


Is there a tactic that I could use for what I'm calling rw_rhs here?

#### Bryan Gin-ge Chen (Jun 17 2020 at 01:53):

There is conv, but I don't know if it works in the NNG: https://leanprover-community.github.io/extras/conv.html

#### Sam Estep (Jun 17 2020 at 01:55):

@Bryan Gin-ge Chen Ah thanks! That seems to be exactly what I was looking for; can I use that from my locally-downloaded Lean installation, or do I need to also install something else?

#### Bryan Gin-ge Chen (Jun 17 2020 at 01:56):

It's part of Lean's core library, so it should work out of the box, I think.

#### Bryan Gin-ge Chen (Jun 17 2020 at 01:59):

OK, this works in the level you're looking at:

intro h,
conv at h { to_rhs, rw ← add_zero a, },
exact add_left_cancel _ _ _ h,


#### Sam Estep (Jun 17 2020 at 02:12):

Oh awesome, thanks @Bryan Gin-ge Chen!

#### Dan Stanescu (Jun 17 2020 at 02:33):

@Sam Estep I don't have that level in front of me right now, but something like this may also help: rw [← add_zero a] {occs := occurrences.pos [1]}

#### Bryan Gin-ge Chen (Jun 17 2020 at 02:42):

Wow, I didn't know about occs / occurrences. We should add this info to the docs somewhere...

#### Johan Commelin (Jun 17 2020 at 04:00):

In theory mathlib's nth_rewrite tactic should also help here. But I recently tried it, and got an error. I haven't yet looked into why...

#### Scott Morrison (Jun 17 2020 at 06:55):

occs has pretty strange behaviour: if a rule can match multiple times, but with different arguments, rw {occs:=...} will not find the alternative matches. nth_rewrite was written to solve this problem.

#### Wojtek Wawrów (Jun 19 2020 at 11:18):

Dan Stanescu said:

Sam Estep I don't have that level in front of me right now, but something like this may also help: rw [← add_zero a] {occs := occurrences.pos [1]}

I've tried using your code but it just gives me an error. Could it be that it just doesn't work in NNG? Same goes for the nth_rewrite thing, it doesn't seem to be recognized in NNG (and I wouldn't know how to use it anyways)

#### Kevin Buzzard (Jun 19 2020 at 11:47):

rofl I think that code has very little chance of working in NNG; I use a hacked rw. Try using rewrite [← add_zero a] {occs := occurrences.pos [1]} in NNG? I didn't hack that, so NNG rewrite should be the same as Lean rw.

#### Kevin Buzzard (Jun 19 2020 at 11:49):

Lean rw closes goals which can be closed by rfl (i.e. it tries refl after every rewrite, and if it works it just closes the goal). I thought this was confusing for NNG beginners so i turned it off (and probably turned off a bunch of other things too).

#### Kevin Buzzard (Jun 19 2020 at 11:50):

Similarly I doubt I am importing enough in NNG to make nth_rewrite work. If you want to play it "properly" you can just download and install the repo -- it would be a much less painful experience!

#### Wojtek Wawrów (Jun 19 2020 at 11:57):

Using rewrite worked! Here's then a short solution which works in NNG:

rewrite [← add_zero a] {occs := occurrences.pos [2]},


I will have to get around to installing the repo, hopefully later this weekend.

#### Kevin Buzzard (Jun 19 2020 at 12:00):

One unfortunate consequence of the hacked rw decision in NNG is that we get people here complaining that rw works differently in real Lean than in NNG. I could have hacked rewrite instead, because then users might expect rw to behave differently, but this would have caused so many extra key presses for my users :-/

#### ROCKY KAMEN-RUBIO (Jun 19 2020 at 19:56):

My (somewhat clunky) approach if rw isn't cooperating is to use a have statement for the thing I wanted rw to give me, and then prove that. I'm forgetting whether NNG has discussed them at this point. This isn't much more concise, but maybe it feels a little less redundant?

intro h,
have h2 : a + b = a + 0,