a*(c*b)=a*(b*c)

Stream: new members

[Kritixi Lithos]

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]

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

[Johan Commelin]

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

[Johan Commelin]

Another option is tactic#nth_rewrite

[Kritixi Lithos]

Johan Commelin said:

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

Thanks! That works perfectly

[Eric Rodriguez]

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