mathlib3

565fef65 - refactor(tactic/tidy): use @[user_attribute] (#8630)

refactor(tactic/tidy): use @[user_attribute] (#8630) This is just a minor change to use the `@[user_attribute]` attribute like all other user attrs instead of calling `attribute.register`. (This came up during the census of mathlib user attrs.)