symmApply vs symm_apply

Stream: mathlib4

[Yury G. Kudryashov]

Which name should we use for simp lemmas (and in simps config)?

$ git grep 'init.*symmApply'
Mathlib/Algebra/Hom/Equiv/Basic.lean:initialize_simps_projections AddEquiv (toEquiv_toFun → apply, toEquiv_invFun → symmApply, -toEquiv)
Mathlib/Algebra/Hom/Equiv/Basic.lean:initialize_simps_projections MulEquiv (toEquiv_toFun → apply, toEquiv_invFun → symmApply, -toEquiv)
Mathlib/Algebra/Module/Equiv.lean:initialize_simps_projections LinearEquiv (toLinearMap → apply, invFun → symmApply)
Mathlib/Algebra/Ring/Equiv.lean:initialize_simps_projections RingEquiv (toEquiv_toFun → apply, toEquiv_invFun → symmApply, -toEquiv)
Mathlib/Logic/Equiv/LocalEquiv.lean:initialize_simps_projections LocalEquiv (toFun → apply, invFun → symmApply)
Mathlib/Order/RelIso/Basic.lean:initialize_simps_projections RelIso (toEquiv_toFun → apply, toEquiv_invFun → symmApply, -toEquiv)

$ git grep 'init.*symm_apply'
Mathlib/Data/Finsupp/Defs.lean:  equivFunOnFinite.symm_apply_apply f
Mathlib/Data/Finsupp/Defs.lean:  rw [← equivFunOnFinite_single, Equiv.symm_apply_apply]
Mathlib/Logic/Equiv/Defs.lean:initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)
Mathlib/Tactic/Simps/Basic.lean:  Example: `initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)`.
Mathlib/Tactic/Simps/Basic.lean:  `initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)`.
Mathlib/Tactic/Simps/Basic.lean:    initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)
Mathlib/Topology/Homeomorph.lean:initialize_simps_projections Homeomorph (toEquiv_toFun → apply, toEquiv_invFun → symm_apply,
test/Simps.lean:initialize_simps_projections Equiv (toFun → apply, invFun → symm_apply)
test/Simps.lean:initialize_simps_projections Equiv (toFun → coe as_prefix, invFun → symm_apply)

[Reid Barton]

symm_apply seems more logical to me

[Floris van Doorn]

It was also on my todo-list to replace all occurrences of symmApply with symm_apply, but feel free to do this!

[Floris van Doorn]

Note that the mismatch is likely because mathport automatically camelCases the custom projections for Simps (e.g. Equiv.Simps.symmApply).