How to rewrite parts of a theorem?

Stream: new members

[Philip B.]

I am solving the Natural number game, advanced addition world, level 6 https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=8&level=6. I need to prove theorem add_left_cancel (t a b : mynat) : t + a = t + b → a = b :=. My first proof is

rw add_comm t a,
rw add_comm t b,
exact add_right_cancel a t b,

I am wondering if I can prove this by rewriting parts of add_right_cancel (a t b : mynat) : a + t = b + t → a = b rather than rewriting parts of the goal. How can I do that? rw add_comm at add_right_cancel, doesn't work. have add_right_cancel, produces something I don't understand.

[Kevin Buzzard]

Maybe something like have h := add_right_cancel a t b, rw add_comm at h? Most lean tactics work on the goal though, it's often easiest to go backwards if you can

[Philip B.]

@Kevin Buzzard Oops, I got confused with the syntax of have. Thank you, that works.