feat: on "type mismatch" errors, expose differences in functions and pi types

[kmill]

Example: Normally subtype notation pretty prints as { x // x > 0 }, but now the difference in domains is exposed:

example (h : {x : Int // x > 0}) : {x : Nat // x > 0} := h
/-
error: type mismatch
  h
has type
  { x : Int // x > 0 } : Type
but is expected to have type
  { x : Nat // x > 0 } : Type
-/

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c7f5fd9a8351c0b69932a81d8d8010395f5e649b --onto 0973ba3e4260327f69587813d6a67e5fade0c977. (2024-11-01 18:45:40)