mathlib

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

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`.