Tactics/methods to do simple algebraic transformations

Stream: new members

[Philogy]

I have a have lemma in my theorem that has a certain shape and I want to convert it to another. Converted here into a #mwe:

theorem can_transform_mod (x y : Int) : (16 * x + -(15 * y)) % 256 = (16 * (x - y) + y) % 256 := by
  sorry

How do I do this (Converting the right side into the left)?

Q2: If have a simple proposition of equality a = b how do I use that to substitute one side or the other in a proposition?

[Luigi Massacci]

I would bet my right hand that by omega should do the trick. You can read more on it in the language reference if you want to

[Luigi Massacci]

For the added question, the answer is rw, but I would suggest reading a more comprehensive tutorial, say #tpil or #mil to get started with the basics

[Luigi Massacci]

See the documentation page more broadly: https://lean-lang.org/documentation/

[Philogy]

Luigi Massacci said:

I would bet my right hand that by omega should do the trick. You can read more on it in the language reference if you want to

Omega does do the trick but my goal here is not to solve that theorem (it's just the #mwe) I specifically want to transform the one for the other because I need it in further proof steps in my larger proof.

Also rw works in the #mwe but not my larger example :thinking:

Here's the full file (down in remco_equiv_naive): https://gist.github.com/Philogy/23932ea05fe450533fe769e3e839cc1e

[Philogy]

Ah it does work, I just have to specifically have the constant (not variables) and the same type, which is quite tedious. But works.

[Alex Mobius]

@Philogy about your equation question, there is subst, which works on variable = expression and deals with those better than rw.