improved interaction of to_additive with other attributes

Stream: mathlib4

[Floris van Doorn]

mathlib4#1314 is a big refactor of the to_additive attribute that improves the interaction with other attributes. It fixes issues mathlib4#950, mathlib4#953 and mathlib4#1149.
One major notational change is that when using to_additive with any other attributes (that should be on both the multiplicative and additive declaration) you have to use @[to_additive (attr := ...)] from now on, so e.g.

@[to_additive (attr := simp)]
@[to_additive (attr := simp, norm_cast)]
@[to_additive (attr := simps apply symm_apply)]
@[to_additive (attr := local simp 500)]

Ideally mathport also starts using this syntax (@Mario Carneiro). Note that in Lean 3 most other attributes come before to_additive but simps comes after it. After this PR is merged all of them should be in the attr field.

[Floris van Doorn]

Note: For now, writing something like @[simp, to_additive] will give a warning to change it to the new form, and similar for a few other common attributes, but not for all of them (for example not for simps).

[Floris van Doorn]

Note 2: the instance attribute is still copied, so we can still use @[to_additive] instance. This is one of the few attributes where we can actually read of all the relevant attribute information (priority, scope) from the environment.

[Floris van Doorn]

This just hit master. Every open PR that uses to_additive should merge master.