## Stream: new members

### Topic: a*(c*b)=a*(b*c)

#### Kritixi Lithos (Jul 12 2021 at 11:00):

Hi, how do I rw[mul_comm] on an inner expression? rw[mul_comm] at (b*c) doesn't work (understandably from the docs), and rw[mul_comm] by itself only handles the outer expression. An example lemma would be the following,

lemma testing (a b c:ℕ):a*(c*b)=a*(b*c) := sorry


Of course in the above example I can solve it by cc, but how can rw be used here? I'm stuck on another proof where I want to commute a product which is an inner expression.

#### Johan Commelin (Jul 12 2021 at 11:01):

@Kritixi Lithos You can use rw [mul_comm c b].

#### Johan Commelin (Jul 12 2021 at 11:02):

And you can even replace either of them by _, if it happens that one of them is a longer expression.

#### Johan Commelin (Jul 12 2021 at 11:02):

Another option is tactic#nth_rewrite

#### Kritixi Lithos (Jul 12 2021 at 11:04):

Johan Commelin said:

Kritixi Lithos You can use rw [mul_comm c b].

Thanks! That works perfectly

#### Eric Rodriguez (Jul 12 2021 at 14:38):

doesn't quite work here because of bracketing, but I find that docs#mul_right_comm and docs#mul_left_comm aren't as used as they really should be

Last updated: Dec 20 2023 at 11:08 UTC