feat: improved `calc` error messages

[kmill]

Makes the error messages report on RHSs and LHSs that do not match the expected values when the relations are defeq. If the relations are not defeq, the error message now no longer mentions the value of the whole calc expression.

Note: it was tempting to try to make use of expected types more widely, but I ran into issue #2073, so this PR does not use the expected type as a hint.

Closes #4318

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5719 build failed against this PR. (2024-10-15 07:20:40) View Log
• 💥 Mathlib branch lean-pr-testing-5719 build failed against this PR. (2024-10-15 08:12:00) View Log
• 💥 Mathlib branch lean-pr-testing-5719 build failed against this PR. (2024-10-15 08:56:17) View Log
• ✅ Mathlib branch lean-pr-testing-5719 has successfully built against this PR. (2024-10-15 17:49:38) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7c2425605c4c0eba47604c5132bd7617bea02e61 --onto 0bfe1a8c1a2e2eb6da0dad270d7b2bbdd5b97c3d. (2024-10-17 01:11:35)
• ✅ Mathlib branch lean-pr-testing-5719 has successfully built against this PR. (2024-10-28 19:20:20) View Log
• ✅ Mathlib branch lean-pr-testing-5719 has successfully built against this PR. (2024-10-28 21:22:41) View Log

[kmill]

!bench

[leanprover-bot]

Here are the benchmark results for commit 235ecbc71781e9fd957408c4a2a189470924bbd7. There were significant changes against commit 7c2425605c4c0eba47604c5132bd7617bea02e61:

  Benchmark             Metric                 Change
  =============================================================
+ bv_decide_mul         branch-misses           -2.5% (-11.2 σ)
+ bv_decide_realworld   branch-misses           -1.4% (-10.2 σ)
- import Lean           task-clock               8.4%  (16.1 σ)
- import Lean           wall-clock               8.4%  (15.8 σ)
- stdlib                dsimp                    1.4%  (21.9 σ)
- stdlib                instantiate metavars    17.2%  (26.8 σ)

[kmill]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5a0249e745adcee23861e58f14a1a4ea05f2d34d. There were significant changes against commit 9847923f9be5de968f10ed7c7493e3ca0072abce:

  Benchmark   Metric                 Change
  ===================================================
+ stdlib      instantiate metavars    -5.7% (-10.4 σ)