Stream: new members
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: May 14 2021 at 06:16 UTC