## Stream: general

### Topic: How to navigate backwards in conv mode

#### dudubao2007 (Jul 24 2022 at 13:16):

For example, I wanted to prove (cb)a=(bc)a=b(ca)=b(ac) in the conv mode, but I stuck there. lean_conv.png

#### Eric Wieser (Jul 24 2022 at 13:21):

Using conv multiple times is one option

#### Eric Wieser (Jul 24 2022 at 13:22):

I think you can use conv within conv? Can you paste your code as a #mwe in #backticks so that we can copy it?

#### dudubao2007 (Jul 24 2022 at 13:26):

import data.real.basic
example (a b c : ℝ) : (c * b) * a = b * (a * c) :=
begin
conv {
to_lhs,
congr,
rw mul_comm,
}
end


#### Jiatong Yang (Jul 24 2022 at 13:28):

Conv within conv is a nice option. Thank you very much!

import data.real.basic
example (a b c : ℝ) : (c * b) * a = b * (a * c) :=
begin
conv {
to_lhs,
conv {
congr,
rw mul_comm,
},
rw mul_assoc,
congr,
skip,
rw mul_comm,
},
end


#### Eric Wieser (Jul 24 2022 at 13:30):

Glad to see you were able to work out how to get that working

#### Eric Rodriguez (Jul 24 2022 at 13:34):

(btw, either docs#mul_rotate or docs#mul_rotate' are your lemma)

#### Jiatong Yang (Jul 24 2022 at 13:37):

Thank you. Of course, if I meet such a goal in a long proof, I will directly solve it by "ring". :joy:

#### Damiano Testa (Jul 24 2022 at 14:07):

...or with the not-yet-in-mathlib ( :smile: ) move_mul, you can also do

example (a b c : ℝ) : (c * b) * a = b * (a * c) :=
by move_mul [a, b]


Last updated: Aug 03 2023 at 10:10 UTC