`simps -fullyApplied` should generate `coe_` instead of `_apply`

It is quite often the case that one wants to generate an unapplied simp lemma for a bundled morphism bar of type Foo (implementing FunLike). Unfortunately, one can only give one name to the coercion to function projection, and to switch between the applied and unapplied versions one has to use simps -fullyApplied (whose behavior is clear only on unary functions, btw).

Here is a MWE:

import Mathlib.Data.FunLike.Basic
import Mathlib.Tactic.Common

structure Foo where
  toFun : Nat → Nat

instance : FunLike Foo Nat Nat where
  coe f := f.toFun
  coe_injective' := by rintro ⟨⟩; congr!

initialize_simps_projections Foo (toFun → apply)

-- This is good
/-- trace: [simps.verbose] The projections for this structure have already been initialized by a previous invocation of `initialize_simps_projections` or `@[simps]`.
    Generated projections for Foo:
    Projection apply: DFunLike.coe
[simps.verbose] adding projection bar_apply:
      ∀ (a : ℕ), bar a = id a -/
#guard_msgs in
@[simps?]
def bar : Foo where
  toFun := id

-- This is bad
/-- trace: [simps.verbose] The projections for this structure have already been initialized by a previous invocation of `initialize_simps_projections` or `@[simps]`.
    Generated projections for Foo:
    Projection apply: DFunLike.coe
[simps.verbose] adding projection baz_apply:
      ⇑baz = id -/
#guard_msgs in
@[simps? -fullyApplied]
def baz : Foo where
  toFun := id

The most principled way I see of solving this is to allow users to register arbitrary projections (rather than just structure fields) and let them decide which projection to generate by doing simps name_of_projection. Eg the second bundled morphism above would instead be declared as

@[simps coe]
def baz : Foo where
  toFun := id

Start with the MWE using simps -fullyApplied, initialize_simps_projections, and the @[simps]/@[simps?] declarations. Trace how the applied and unapplied projections are selected, including the unary-function limitation. Done means the unapplied case generates the intended coe_ projection and the MWE's guarded messages reflect the corrected behavior.