refactor: update and consolidate attribute-related error messages

[jrr6]

This PR consolidates common attribute-related error messages into reusable functions and updates the wording and formatting of relevant error messages.

[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 9d93b10919ba21cbc2855b73d2d2302567bb9fd8 --onto cdab726e3d289b80860ae9f5a7de21d990c8b95f. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-24 01:23:50)
• 💥 Mathlib branch lean-pr-testing-9495 build failed against this PR. (2025-07-24 18:44:18) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bc5526cacbe4fdea27b273517fb364fcd24eb8e0 --onto 73422d52fd61c3d5bce6f5edb53c6bd698b1b7ba. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-25 19:01:24)

[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 9d93b10919ba21cbc2855b73d2d2302567bb9fd8 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-24 01:23:51)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-07-23 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-07-24 18:00:31)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase bc5526cacbe4fdea27b273517fb364fcd24eb8e0 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-25 19:01:26)