symmetry at h not working

Stream: new members

[Alena Gusakov]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Alena Gusakov]

symmetry' worked!! Thank you :)

[Alena Gusakov]

And good to know

[Kevin Buzzard]

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

[Alex Zhang]

theorem test (g: (1:ℕ) = (2:ℕ)) : 1 = 1 :=
begin
   symmetry at g,
   --refl,
end

I expected symmetry at g to change g to g : 2=1, but it gives me the error message invalid 'begin-end' expression, ',' expected. Why is that?

[Damiano Testa]

symmetry' at ... might work

[Alex Zhang]

I found the chat history for this problem... I see what I should use (although I can't understand why symmetry and symmetry' are not combined).

[Ruben Van de Velde]

Hmm, why isn't symmetry' listed at https://leanprover-community.github.io/mathlib_docs/tactics.html ?

[Kevin Buzzard]

This is probably my fault -- IIRC I hacked the Lean symmetry tactic so it worked like this in NNG. I would be happy for symmetry' to become symmetry, I think this was the plan.