equality manipulation

Stream: new members

[Michael Beeson]

Question 1: I have h:t=s and I want to reverse it. If it's in the goal I can do rw symmetry but rw symmetry at h doesn't work.
It's surely silly but have h2:s=t:= begin finish end, does work. But I'm sure it's not the right way.

Question 2. I have h1 : x = single u and h2: y = single u and I want to write have h3:x=y for some reason.
I tried have h3:x=y:= begin ifinish end and got "deep recursion..." Since posting this I realized the obvious
answer is rw\left h2 at h1. Never mind. But I still don't know about question 1.

[Johan Commelin]

rw eq_comm works

[Kenny Lau]

depends on who you're asking, have h2 : s = t := begin finish end might be the right way

[Kevin Buzzard]

You can also use h.symm. I think there's also a symmetry' tactic which might allow at h