symmetry tactic for not equals

Stream: Is there code for X?

[Kayla Thomas]

Is there a tactic that will turn x ≠ y and ¬(x = y) into y ≠ x and ¬(y = x) respectively, that can be used on either the goal or a given hypothesis with at?

[Kyle Miller]

How about rw [ne_comm] or rw [ne_comm] at h?

[Kyle Miller]

For the ¬(x = y) form you can rewrite with eq_comm instead if ne_comm doesn't work.

[Kayla Thomas]

Thank you. It would still be nice to have a single tactic I guess, or somehow make symmetry do this, if that is possible maybe.

[Adam Topaz]

I would have expected symmetry to work.

[Adam Topaz]

okay, so symmetry does indeed work on the goal, but not on a hypothesis

[Adam Topaz]

but symmetry at h doesn't seem to be valid at all, even for regular equalities.

[Kayla Thomas]

Hmm, I didn't realize symmetry worked on the goal. Does it for both versions?

[Adam Topaz]

what do you mean "both versions"?

[Adam Topaz]

import tactic

example (a b : ℕ) (h : a ≠ b) : b ≠ a :=
by { symmetry, assumption }


example (a b : ℕ) (h : a = b) : b = a :=
by { symmetry, assumption }

[Adam Topaz]

both of those work

[Adam Topaz]

It even works for fancier things like this:

import category_theory.isomorphism
open category_theory

example (C : Type*) [category C] (X Y : C) (e : X ≅ Y) : Y ≅ X :=
by { symmetry, assumption }

[Kayla Thomas]

Sorry, the ¬(x = y) version. It doesn't seem to work for me there.

[Kayla Thomas]

For example

symmetry tactic failed, target is not a relation application with the expected property.
state:
v t x y : variable_,
h1_left : (t ≠ x),
h1_right : (t ≠ y),
h : (¬(y = v)) → (y = t),
contra : (¬(v = y))
⊢ (¬(y = v))

[Kyle Miller]

Yeah, symmetry shouldn't work in that case because it would try to look for a symm lemma for docs#not

[Adam Topaz]

but a dsimp should change that to $\neq$ I suppose.

[Kayla Thomas]

Sorry, I have something to go to. I'll be back later.