rw both sides of an equation

Stream: new members

[Mujtaba Alam]

(world 8 level 7)
I've got h : t + a = t + b and I'd like to rw add_comm at h on both sides of h to hopefully get h : a + t = b + t. Does anyone know the syntax for this?

[Moritz Doll]

you can use explicit variables to rewrite the second addition: rw [add_comm t a, add_comm t b] at h.

[Mujtaba Alam]

Moritz Doll said:

you can use explicit variables to rewrite the second addition: rw [add_comm t a, add_comm t b] at h.

Thank you! What do I do this case, where h : a + b = a and rw ← add_zero a at h, adds the zero to the first instance of a?
EDIT: nevermind, I found the same question here: https://leanprover-community.github.io/archive/stream/113489-new-members/topic/Rewriting.20specific.20term.html

[Johan Commelin]

You can wrap your code in conv_rhs { code goes here } so that you only work on the RHS = right hand side.

[Mujtaba Alam]

(deleted)

[Mujtaba Alam]

Moritz Doll said:

you can use explicit variables to rewrite the second addition: rw [add_comm t a, add_comm t b] at h.

I have h : n = succ n. Trying rw ← zero_add at h, doesn't work. (zero add is defined as (n : mynat) : 0 + n = n). What's going on here?

[Notification Bot]

Mujtaba Alam has marked this topic as unresolved.

[Johan Commelin]

@Mujtaba Alam What do you mean with "doesnt work"? Do you get an error?

[Mujtaba Alam]

Johan Commelin said:

Mujtaba Alam What do you mean with "doesnt work"? Do you get an error?

I think I did, but I totally forgot the context behind it and ended up solving the level differently

[Mujtaba Alam]

(deleted)