feat: expose decidable_of_bool

[robertmaxton42]

This PR adds @[expose] to decidable_of_bool so that proofs-by-decide elsewhere that reduce to decidable_of_bool continue to reduce.

[kim-em]

See #lean4 > Missing `@[expose]` @ 💬.

[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 3bd1dd633f29de1dd0ea0e23833da7710bdb1c25 --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-12 02:59:40)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 3bd1dd633f29de1dd0ea0e23833da7710bdb1c25 --onto eee58f4506d28a14c9a171165f999445a0663d93. You can force reference manual CI using the force-manual-ci label. (2025-12-12 02:59:41)