Commit 2020-10-27 14:39 a027a37b

feat(tactic/simps): user-provided names for projections (#4663) Adds the functionality to specify custom projection names, like this:

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.