refactor: correct names of quaternion lemmas (#29190)

This renames lemmas of the form `(foo x).re` to be called `re_foo` instead of `foo_re`, and similarly for `imI`, `imJ`, `imK`, and `im`, to match the naming guide.

These are then all deprecated with the deprecation script.
I did not attempt to deprecated the relocated `simps` lemmas.
Some lemmas ended up exchanged and could not be deprecated, listed below:

Moves:
- Quaternion.im_star -> Quaternion.star_im
- Quaternion.star_im-> Quaternion.im_star
- QuaternionAlgebra.im_star -> QuaternionAlgebra.star_im
- QuaternionAlgebra.star_im-> QuaternionAlgebra.im_star

Author: eric-wieser