Zulip Chat Archive

Stream: new members

Topic: How to rewrite parts of a theorem?


Philip B. (Sep 15 2020 at 06:23):

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 (Sep 15 2020 at 06:37):

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. (Sep 15 2020 at 06:42):

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


Last updated: Dec 20 2023 at 11:08 UTC