feat: make `registerLabelAttr` consistent with `registerTagAttribute`

[thorimur]

This PR modifies the recently-upstreamed LabelAttributes to be consistent with TagAttributes. Specifically, we modify registerLabelAttr to

• allow a validate argument
• allow an AttributeApplicationTime argument
• change the default applicationTime to .afterTypeChecking
• use the same argument order as registerTagAttribute

This also modifies some docstrings to point users to these features.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-3699 build failed against this PR. (2024-03-16 22:12:04) View Log
• 💥 Mathlib branch lean-pr-testing-3699 build failed against this PR. (2024-03-16 22:32:05) View Log
• 💥 Mathlib branch lean-pr-testing-3699 build failed against this PR. (2024-03-16 22:47:45) View Log
• 💥 Mathlib branch lean-pr-testing-3699 build failed against this PR. (2024-03-17 00:38:45) View Log
• 💥 Mathlib branch lean-pr-testing-3699 build failed against this PR. (2024-03-17 16:58:05) View Log
• ✅ Mathlib branch lean-pr-testing-3699 has successfully built against this PR. (2024-03-18 19:08:27) View Log

[kim-em]

Just confirming that this is still a draft. The changes do seem nice to have!

[thorimur]

@semorrison Apologies, I've been inactive for the past few months! :) If this is still desired I'm happy to finalize it and make it a real PR.