feat: attribute delaborators

[digama0]

This PR enables attributes to be able to specify how they would like to be shown in #print as additional attribute syntax, with AttributeImpl.delab being a rough inverse to AttributeImpl.add. As a result, this now works:

@[reducible, simp] def foo := 1

#print foo
-- @[reducible, simp] def foo :=
-- 1

Additional comments:

• This does not add delaborators for every attribute; some are skipped because they leave no permanent trace, some because they don't support query at all or not efficiently enough. The semantics of the delab function are such that fun _ => pure () is always an okay backup plan.
• In order to find places to add the new field, for now the delab field is not optional. I hope this can be used at least to clean up mathlib as well, but in the final version I expect delab to be optional and defaulted to fun _ => pure () to make it backward compatible.

Closes #6107

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-11-18 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-11-18 09:00:34)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-11-18 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-11-18 12:19:10)
• 💥 Mathlib branch lean-pr-testing-6115 build failed against this PR. (2024-11-19 10:00:50) View Log
• 💥 Mathlib branch lean-pr-testing-6115 build failed against this PR. (2024-11-19 10:48:07) View Log

[kim-em]

There's now an updated nighly-with-mathlib, so if you'd like to rebase onto that we can start looking at Mathlib/Batteries.

[Kha]

Drafting pending acceptance of RFC