chore: typeclass for non-dependent FunLike

[FR-vdash-bot]

This eliminates (fun a ↦ β) α in the type when applying a FunLike.

Not sure about the name.

I'd like to see if it's much better than #7905.

---

[eric-wieser]

The problem with this strategy is we now need separate lemmas for NDFunLike.coe and FunLike.coe

[eric-wieser]

Oh, I take back my other comment; this actually does continue to use FunLike.coe` as a head symbol!

[FR-vdash-bot]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1689c16.
There were significant changes against commit bf077b1:

  Benchmark                                                  Metric         Change
  ================================================================================
- build                                                      maxrss           8.0%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings          instructions    -7.4%
+ ~Mathlib.Algebra.Category.Ring.Constructions               instructions   -44.0%
+ ~Mathlib.Algebra.DirectLimit                               instructions   -18.2%
+ ~Mathlib.Algebra.Homology.ModuleCat                        instructions   -31.8%
+ ~Mathlib.Algebra.Jordan.Basic                              instructions    -5.6%
- ~Mathlib.Algebra.Lie.Basic                                 instructions     6.8%
- ~Mathlib.AlgebraicGeometry.AffineScheme                    instructions     7.6%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Point             instructions    -4.0%
- ~Mathlib.AlgebraicGeometry.Gluing                          instructions     8.7%
+ ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated        instructions    -9.4%
- ~Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties     instructions    12.9%
+ ~Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme       instructions    -6.2%
+ ~Mathlib.AlgebraicGeometry.Properties                      instructions    -9.6%
+ ~Mathlib.AlgebraicGeometry.Spec                            instructions   -10.9%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul                      instructions    -6.3%
+ ~Mathlib.CategoryTheory.Abelian.InjectiveResolution        instructions    -1.5%
+ ~Mathlib.CategoryTheory.Monoidal.Internal.Module           instructions    -9.0%
- ~Mathlib.CategoryTheory.Monoidal.Mod_                      instructions     6.7%
+ ~Mathlib.Combinatorics.HalesJewett                         instructions   -82.8%
+ ~Mathlib.FieldTheory.RatFunc                               instructions    -2.2%
- ~Mathlib.Geometry.Manifold.VectorBundle.SmoothSection      instructions   152.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction         instructions    -7.1%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Even                instructions   -12.6%
+ ~Mathlib.LinearAlgebra.Dual                                instructions    -4.5%
- ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading             instructions     9.9%
- ~Mathlib.LinearAlgebra.FinsuppVectorSpace                  instructions     6.1%
+ ~Mathlib.LinearAlgebra.FreeModule.PID                      instructions   -49.9%
- ~Mathlib.LinearAlgebra.TensorAlgebra.Grading               instructions    11.2%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                    instructions    -4.7%
- ~Mathlib.NumberTheory.ArithmeticFunction                   instructions   146.2%
- ~Mathlib.NumberTheory.VonMangoldt                          instructions   207.5%
- ~Mathlib.RepresentationTheory.Action                       instructions    17.8%
+ ~Mathlib.RepresentationTheory.Character                    instructions   -28.9%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution   instructions   -52.5%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation           instructions   -22.6%
+ ~Mathlib.RingTheory.IsTensorProduct                        instructions    -8.9%
+ ~Mathlib.RingTheory.PowerSeries.Basic                      instructions   -11.6%
+ ~Mathlib.RingTheory.RootsOfUnity.Basic                     instructions    -6.7%