Lint for `category` attribute duplicates

[Paul-Lez]

We should lint to make sure we don't have statements of the form

@[category research solved, category research open]
theorem foo : ...

and so on.

Choose either option

• I plan on implementing this
• This issue is up for grabs