Symmetry of equality applied to a hypothesis

Stream: new members

[James Weaver]

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]

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

[Bryan Gin-ge Chen]

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]

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

[Kevin Buzzard]

in the natural number game you can just put symmetry at h because we have the power to change core ;-)

[Chris Hughes]

rw eq_comm also works.