How to navigate backwards in conv mode

Stream: general

[dudubao2007]

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]

Using conv multiple times is one option

[Eric Wieser]

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]

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]

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]

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

[Eric Rodriguez]

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

[Jiatong Yang]

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

[Damiano Testa]

...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]