mathlib3

a027a37b - feat(tactic/simps): user-provided names for projections (#4663)

feat(tactic/simps): user-provided names for projections (#4663) Adds the functionality to specify custom projection names, like this: ```lean initialize_simps_projections equiv (to_fun → apply, inv_fun → symm_apply) ``` These names will always be used and cannot (yet) be manually overridden. Implement this for embeddings: `initialize_simps_projections embedding (to_fun → apply)`. Rename `fixed_points.to_alg_hom_apply -> fixed_points.to_alg_hom_apply_apply`, since `@[simps]` now generates the name `to_alg_hom_apply` instead of `to_alg_hom_to_fun`.