Stream: new members
James Weaver (Dec 26 2019 at 16:57):
This is probably a stupid question, but when I'm in tactics mode and I have an hypothesis of the form
h: a = b and need one of the form
h: b = a is there a simple result I can use with rw to just swap it round? I've tried
rw eq.symm a b at h but that doesn't seem to do what I want here. I'm probably missing something really obvious.
James Weaver (Dec 26 2019 at 17:03):
Have just realised that what I want is:
have h := eq.symm h,
Bryan Gin-ge Chen (Dec 26 2019 at 17:22):
If you're using mathlib,
symmetry' at h will also work (source). Looks like it's not yet in the tactic docs...
Alex J. Best (Dec 26 2019 at 17:28):
You can also use
h.symm to refer to the swapped version.
Kevin Buzzard (Dec 26 2019 at 17:56):
in the natural number game you can just put
symmetry at h because we have the power to change core ;-)
Chris Hughes (Dec 26 2019 at 21:57):
rw eq_comm also works.
Last updated: May 06 2021 at 22:13 UTC