Showing two expressions are not equal

Stream: Is there code for X?

[Arend Mellendijk]

I want to show that two terms are not equal by proving some predicate holds on one side but not the other. That is, in my proof I'd like to apply the following theorem and prove the two sub-cases.

theorem ne_of_prop {x y : α} (p : α → Prop) (hx : p x) (hy : ¬ p y) : x ≠ y := by
  intro h; subst h; contradiction

This lemma doesn't seem to exist in mathilb. Is there a better way to do this? The terms x and y are quite ugly, so I'd like to avoid having to write them out in the proof.

[Damiano Testa]

Can you prove it via the contrapositive of congr_arg as well? That might be a way to golf the proof enough that you do not actually need the lemma in the first place.

[Ruben Van de Velde]

Start with apply ne_of_apply_ne p, perhaps

[Eric Wieser]

docs#ne_of_mem_of_not_mem is very close (it's defeq)

[Arend Mellendijk]

Ruben Van de Velde said:

Start with apply ne_of_apply_ne p, perhaps

Annoyingly I looked for that but exact? didn't find it

import Mathlib

example {x y : α} (p : α → Type _) (hxy : p x ≠ p y) : x ≠ y := by
  -- exact? -- fails
  exact ne_of_apply_ne p hxy

But I'm not quite on the latest mathlib so it may not reproduce.

[Arend Mellendijk]

That said getting from p x ≠ p y to what I want is still a little verbose so I'll probably go with Eric's suggestion

[Arend Mellendijk]

Also should there be a propositional version just so I don't get tempted by defeq abuse?

[Eric Wieser]

The problem with the propositional version is that it's hard to name

[Eric Wieser]

ne_of_of_not isn't ideal!