## Stream: new members

### Topic: symmetry at h not working

#### 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

#### 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...

#### Mario Carneiro (May 30 2020 at 00:37):

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

#### Mario Carneiro (May 30 2020 at 00:38):

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

#### Alena Gusakov (May 30 2020 at 00:42):

symmetry' worked!! Thank you :)

And good to know

#### 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