Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC