Motivation: `sorry` should have an indeterminate value so that it's harder to make "fake" theorems about stubbed-out definitions. This PR makes each instance of `sorry` be non-defeq to any other. For example, this now fails:
```lean
example : (sorry : Nat) = sorry := rfl -- fails
```
However, this still succeeds:
```lean
def f (n : Nat) : Nat := sorry
example : f 0 = f 1 := rfl -- succeeds
```
One can be more careful by putting variables to the right of the colon:
```lean
def f : (n : Nat) → Nat := sorry
example : f 0 = f 1 := rfl -- fails
```

Details:

Adds `Lean.Meta.mkUniqueSorry`, which creates a sorry that is not defeq to any other sorry. It also encodes the source position into the term.

Makes the `sorry` term and `sorry` tactic create unique sorries.

Adds support to the LSP so that "go to definition" on `sorry` in the Infoview goes to the origin of that particular `sorry`.

Fixes `sorry` pretty printing: no more `sorryAx` in the Infoview.

Removes `Lean.Meta.mkSyntheticSorry` in favor of `Lean.Meta.mkSorry`.

…tion errors can compound the issues. In any case, they can still be labeled.

improves addPPExplicitToExposeDiff when functions are overapplied

fixes mdata bugs in location RPC handler

fixes leanprover#4972