feat: have "motive is not type correct" come with an explanation

[kmill]

This PR extends the "motive is not type correct" error message for the rewrite tactic to explain what it means. It also pretty prints the type-incorrect motive and reports the type error.

Suggested on Zulip.

[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 ea221f3283fef1a883b1e0be78295a4a49a92d23 --onto 72e952eadc6a171310f1d8e9d6e78acf98421494. (2024-11-22 05:24:45)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ea221f3283fef1a883b1e0be78295a4a49a92d23 --onto 6202461a21d2636129cb8950cd9b6549ccf4b185. (2024-11-22 23:58:41)