# Zulip Chat Archive

## Stream: new members

### Topic: Rewrite tactic

#### De Paz (Feb 14 2020 at 14:24):

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 (Feb 14 2020 at 14:32):

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 with`simp [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 (Feb 14 2020 at 14:36):

Thank you!

#### Kevin Buzzard (Feb 14 2020 at 16:19):

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.

Last updated: Dec 20 2023 at 11:08 UTC