Zulip Chat Archive

Stream: new members

Topic: Symmetry of equality applied to a hypothesis


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

view this post on Zulip James Weaver (Dec 26 2019 at 17:03):

Have just realised that what I want is:
have h := eq.symm h,

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

view this post on Zulip Alex J. Best (Dec 26 2019 at 17:28):

You can also use h.symm to refer to the swapped version.

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

view this post on Zulip Chris Hughes (Dec 26 2019 at 21:57):

rw eq_comm also works.


Last updated: May 06 2021 at 22:13 UTC