feat(equiv/basic): use @[simps] (#4652)

Use the `@[simps]` attribute to automatically generate equation lemmas for equivalences.
The names `foo_apply` and `foo_symm_apply` are used for the projection lemmas of `foo`.

Author: fpvandoorn