feat(logic/basic): given two different elements, one of the two is different from a third

[adomani]

This lemma is extracted from #15984, as suggested by the code-review.

---

[adomani]

If Ramsey's theorem has been proved in mathlib, this lemma could be an application. 🙃

[adomani]

@eric-wieser, here is an example of the ne.symm issue:

import tactic.alias
example {α} {a b : α} (ab : a ≠ b) : b ≠ a := ab.symm  --works
example {α} {a b : α} (ab : ¬a = b) : ¬b = a := ab.symm  -- there isn't a not.symm

alias ne.symm ← not.symm
example {α} {a b : α} (ab : ¬a = b) : ¬b = a := ab.symm  -- now this works

[adomani]

docs#decidable.exists_ne, L43 is an example where dot-notation cannot be used.

protected lemma decidable.exists_ne [nontrivial α] [decidable_eq α] (x : α) : ∃ y, y ≠ x :=
begin
  rcases exists_pair_ne α with ⟨y, y', h⟩,
  by_cases hx : x = y,
  { rw ← hx at h,
    exact ⟨y', h.symm⟩ },
  { exact ⟨y, ne.symm hx⟩ }
end

In this case again the issue is the ¬ rather than the ≠ generated by by_cases. In this situation, this actually works:

protected lemma decidable.exists_ne {α} [nontrivial α] [decidable_eq α] (x : α) : ∃ y, y ≠ x :=
begin
  rcases exists_pair_ne α with ⟨y, y', h⟩,
  rcases eq_or_ne x y with rfl | hx,
  exacts [⟨y', h.symm⟩, ⟨y, hx.symm⟩]
end

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests