feat: improve error messages and docstring for decide tactic

[kmill]

The decide tactic produces error messages that users find to be obscure. Now:

1. If the Decidable instance reduces to isFalse, it reports that decide failed because the proposition is false.
2. If the Decidable instance fails to reduce, it explains what proposition it failed for, and it shows the reduced Decidable instance rather than the Decidable.decide expression. That expression tends to be less useful since it shows the unreduced Decidable argument (plus it's a lot longer!)

Examples:

example : 1 ≠ 1 := by decide
/-
tactic 'decide' proved that the proposition
  1 ≠ 1
is false
-/

opaque unknownProp : Prop

open scoped Classical in
example : unknownProp := by decide
/-
tactic 'decide' failed for proposition
  unknownProp
since its 'Decidable' instance reduced to
  Classical.choice ⋯
rather than to the 'isTrue' constructor.
-/

When reporting the error, decide only shows the whnf of the Decidable instance. In the future we could consider having it reduce all decidable instances present in the term, which can help with determining the cause of failure (this was explored in 8cede58).

[kmill]

@david-christiansen The decide tactic has had a confusing error message when it fails to prove the goal, and here's an attempt to improve the situation, and the documentation as well while we're here.

There was recent Zulip discussion about decide. There, there was a request to make decide synthesize a reason for the failure, but that doesn't seem to be possible to do in a satisfying amount of generality, unless we had a parallel version of Decidable whose constructors contained a reason for the success or failure. This is an idea I had that made it into LSpec.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std CI can not be attempted yet, as the nightly-testing-2024-02-20 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Std CI should run now. (2024-02-20 19:48:52)
• 💥 Mathlib branch lean-pr-testing-3422 build failed against this PR. (2024-02-21 01:18:34) View Log
• 💥 Mathlib branch lean-pr-testing-3422 build failed against this PR. (2024-02-21 02:40:08) View Log
• 💥 Mathlib branch lean-pr-testing-3422 build failed against this PR. (2024-02-21 04:08:29) View Log
• 💥 Mathlib branch lean-pr-testing-3422 build failed against this PR. (2024-02-21 21:29:44) View Log
• 💥 Mathlib branch lean-pr-testing-3422 build failed against this PR. (2024-02-27 18:25:00) View Log
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9c00a5933944bbc4801079777dd9fcc326e66390 --onto c5fd88f5e118738425dd55b7592de435b7db8483. (2024-02-27 23:11:00)

[david-christiansen]

This looks like a nice improvement!

I think we should look into adding reasons as optional arguments. If we do it right, we might not even break anything :-)

[leodemoura]

Rebased