Rewrite tactic

Stream: new members

[De Paz]

Hey there!
I'm trying to prove the lemma add_assoc by induction from the natural number game.
In the base case I want to substitute b + 0 with b by using rw add_zero, but lean only substitutes the first b+0 from left to right that it finds , so I have to write it twice. Is there a way to tell lean to substitute all b+0 in the goal?

I would appreciate some advice.

This is my code:

lemma add_assoc (a b c : mynat) : (a + b) + c = a + (b + c) :=
  begin
     induction c with d hd,
     rw [add_zero, add_zero],
     refl,

[Chris Hughes]

The first time it's actually applying the add_zero lemma to a+b, not b. There is no b + 0 on the left hand side.

You can rw twice withsimp [add_zero]. simp will use lots of different rewrite rules to simplify the expression. To only simplify using add_zero, you can use simp only [add_zero]

[De Paz]

Thank you!

[Kevin Buzzard]

I toned down rw in the natural number game so it wouldn't close a refl goal. Just to warn you that simp might just close the goal by itself.