mathlib3

[Merged by Bors] - refactor(*): move all `mk_simp_attribute` commands to 1 file

#19223

Closed