mathlib3

1ac8d430 - chore(*): fix `@[to_additive, simp]` to the correct order (#19169)

chore(*): fix `@[to_additive, simp]` to the correct order (#19169) Whilst making some files, I noticed that there is some lemmas that have the wrong order for `to_additive` and `simp`.