Zulip Chat Archive

Stream: new members

Topic: How to rewrite parts of a theorem?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: May 14 2021 at 06:16 UTC