Zulip Chat Archive

Stream: new members

Topic: symmetry at h not working


view this post on Zulip Alena Gusakov (May 30 2020 at 00:28):

I'm going through the complex number game and, for whatever reason, "symmetry at h" never works for me. I've found workarounds for it but I finally got stuck on a lemma without it and I don't know what's wrong with it. Could I just be on a version that doesn't allow symmetry on a hypothesis? I'm on version 3.13.2

view this post on Zulip Bryan Gin-ge Chen (May 30 2020 at 00:32):

I think you have to write symmetry' at h. Looks like there's a gap in our tactic docs...

view this post on Zulip Mario Carneiro (May 30 2020 at 00:37):

FYI you can always work around it with have h := h.symm

view this post on Zulip Mario Carneiro (May 30 2020 at 00:38):

or generally use h.symm or <- h where you would have used h

view this post on Zulip Alena Gusakov (May 30 2020 at 00:42):

symmetry' worked!! Thank you :)

view this post on Zulip Alena Gusakov (May 30 2020 at 00:42):

And good to know

view this post on Zulip Kevin Buzzard (May 30 2020 at 06:37):

Sorry, I think I made symmetry work in the natural number game by hackery, expecting lean to catch up some day...


Last updated: May 14 2021 at 00:42 UTC