Zulip Chat Archive

Stream: new members

Topic: equality manipulation

Michael Beeson (Oct 28 2020 at 08:15):

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 (Oct 28 2020 at 08:45):

rw eq_comm works

Kenny Lau (Oct 28 2020 at 08:46):

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

Kevin Buzzard (Oct 28 2020 at 08:46):

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

Last updated: Dec 20 2023 at 11:08 UTC