alias, deprecated, and to_additive don't get along togther

[kim-em]

Unfortunately,

@[to_additive (attr := deprecated (since := "date"))] alias foo_mul := bar_mul

only attaches the replacement name to foo_mul, not to foo_add, and so we need to add the replacement foo_add -> bar_add in a separate attribute statement.

[kim-em]

(This is a tracking issue: as of #19426, all such occurrences in Mathlib have a link to this issue.)