feat: detailed feedback on `decide` tactic failure (#4674)

When the `decide` tactic fails, it can try to give hints about the
failure:
- It tells you which `Decidable` instances it unfolded, by making use of
the diagnostics feature.
- If it encounters `Eq.rec`, it gives you a hint that one of these
instances was likely defined using tactics.
- If it encounters `Classical.choice`, it hints that you might have
classical instances in scope.
- During this, it tries to process `Decidable.rec`s and matchers to pin
blame on a particular instance that failed to reduce.

This idea comes from discussion with Heather Macbeth [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Decidable.20with.20structures/near/449409870).