This PR improves the “expected type mismatch” error message by omitting
the type's types when they are defeq, and putting them into separate
lines when not.
I found it rather tediuos to parse the error message when the expected
type is long, because I had to find the `:` in the middle of a large
expression somewhere. Also, when both are of sort `Prop` or `Type` it
doesn't add much value to print the sort (and it’s only one hover away
anyways).
This PR changes `addPPExplicitToExposeDiff` to show universe differences
and to visit into projections, e.g.:
```
error: tactic 'rfl' failed, the left-hand side
(Test.mk (∀ (x : PUnit.{1}), True)).1
is not definitionally equal to the right-hand side
(Test.mk (∀ (x : PUnit.{2}), True)).1
```
for
```lean
inductive Test where
| mk (x : Prop)
example : (Test.mk (∀ _ : PUnit.{1}, True)).1 = (Test.mk (∀ _ : PUnit.{2}, True)).1 := by
rfl
```
