symmetry of a theorem

Stream: new members

[Robert Watson]

I'm wondering if there is an easier way to write this:

have add_one : (a' + 1 = succ a') := add_one_eq_succ a',
have add_one2 : (succ a' = a' + 1) := (add_one),
rw (add_one2) at f,

Like for example:

rw (←add_one_eq_succ a') at f,

So far I haven't been able to get the syntax right for this.

[Kevin Buzzard]

Can you post a #mwe ?

[Robert Watson]

When I try to do lean in VSCode I find that it often produces the following even when there is an error in the code, or even if the code is absurd (see lack of errors below)...so I can't do a proper mwe right now. I have to use the Natural Numbers Game online which works, but that isn't a real mwe, so I'll do it using that:

All Messages (1)
No messages.

[Riccardo Brasca]

There is no error/picture in your message.