chore: remove Ne.elim (#14345)

<!--
# Read this section before submitting

* Ensure your PR follows the [External Contribution
Guidelines](https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md).
* Please make sure the PR has excellent documentation and tests. If we
label it `missing documentation` or `missing tests` then it needs
fixing!
* Include the link to your `RFC` or `bug` issue in the description.
* If the issue does not already have approval from a developer, submit
the PR as draft.
* The PR title/description will become the commit message. Keep it
up-to-date as the PR evolves.
* For `feat/fix` PRs, the first paragraph starting with "This PR" must
be present and will become a
changelog entry unless the PR is labeled with `no-changelog`. If the PR
does not have this label,
it must instead be categorized with one of the `changelog-*` labels
(which will be done by a
  reviewer for external PRs).
* A toolchain of the form `leanprover/lean4-pr-releases:pr-release-NNNN`
for Linux and M-series Macs will be generated upon build. To generate
binaries for Windows and Intel-based Macs as well, write a comment
containing `release-ci` on its own line.
* If you rebase your PR onto `nightly-with-mathlib` then CI will test
Mathlib against your PR.
* You can manage the `awaiting-review`, `awaiting-author`, and `WIP`
labels yourself, by writing a comment containing one of these labels on
its own line.
* Remove this section, up to and including the `---` before submitting.

---
-->

This PR removes `Ne.elim`, as it is strictly less general than
`Not.elim`. Dot notation will still work, since if we have `h : a ≠ b`
then `h.elim` will elaborate to `Not.elim h` instead of `Ne.elim h`.

Author: plp127

src/Init/Core.lean

@@ -887,8 +887,6 @@ variable {a b : α} {p : Prop}
 
 theorem Ne.intro (h : a = b → False) : a ≠ b := h
 
-theorem Ne.elim (h : a ≠ b) : a = b → False := h
-
 theorem Ne.irrefl (h : a ≠ a) : False := h rfl
 
 @[symm] theorem Ne.symm (h : a ≠ b) : b ≠ a := fun h₁ => h (h₁.symm)

src/Std/Data/Internal/List/Associative.lean

@@ -2243,7 +2243,7 @@ theorem getEntry?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) 
     simp only [getEntry?_cons]
     cases h₂ : k₂ == a <;> cases h₁ : k₁ == a <;> try simp; done
     simp only [distinctKeys_cons_iff, containsKey_cons, Bool.or_eq_false_iff] at hl
-    exact ((Bool.eq_false_iff.1 hl.2.1).elim (BEq.trans h₁ (BEq.symm h₂))).elim
+    exact (Bool.eq_false_iff.1 hl.2.1).elim (BEq.trans h₁ (BEq.symm h₂))
   next l₁ l₂ l₃ hl₁₂ _ ih₁ ih₂ => exact (ih₁ hl).trans (ih₂ (hl.perm (hl₁₂.symm)))
 
 theorem getEntryD_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α} {fallback : (a : α) × β a}