symmetry tactic request

Stream: general

[Kevin Buzzard]

I have another tactic request: symmetry. Looks like the Lean 3 version never got ported? But I need it for NNG. The spec is that symmetry should change a goal of x = y to y = x, a goal of x \ne y to y \ne x and a goal of P \iff Q to Q iff P, and symmetry at h should do the same for hypothesis h.

I feel like I could do this one myself in a totally bone-headed way if I knew which book to read (which one goes through examples like this?), not least because it's just apply eq.symm at h etc for me in NNG. But in Lean 3 I think that there was some symmetry tag which you could give to a binary relation once you'd proved a symm lemma for it, and really symmetry should work on all of these. Does this tag still exist?

[Scott Morrison]

It's called symm, not symmetry.

[Kevin Buzzard]

No wonder all my searches failed :-)