chore: remove CoeFun instances where FunLike is available (#17870)

During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library.

There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.

There is also a shortcut instance that we need for speed reasons: `SemilinearIsometry.instCoeFun`. I don't know why this is so performance-sensitive but the benchmarks tell us that it is.

See also #17871 for removing porting notes and comments where this change happened earlier on.

Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

@@ -487,9 +487,12 @@ instance instSemilinearIsometryEquivClass :
   map_smulₛₗ e := map_smulₛₗ e.toLinearEquiv
   norm_map e := e.norm_map'
 
--- TODO: Shouldn't these `CoeFun` instances be scrapped?
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.hasCoeToFun`
-directly. -/
+/-- Shortcut instance, saving 8.5% of compilation time in
+`Mathlib.Analysis.InnerProductSpace.Adjoint`.
+
+(This instance was pinpointed by benchmarks; we didn't do an in depth investigation why it is
+specifically needed.)
+-/
 instance instCoeFun : CoeFun (E ≃ₛₗᵢ[σ₁₂] E₂) fun _ ↦ E → E₂ := ⟨DFunLike.coe⟩
 
 theorem coe_injective : @Function.Injective (E ≃ₛₗᵢ[σ₁₂] E₂) (E → E₂) (↑) :=

Mathlib/Combinatorics/Young/SemistandardTableau.lean

@@ -68,10 +68,6 @@ instance instFunLike {μ : YoungDiagram} : FunLike (SemistandardYoungTableau μ)
     cases T'
     congr
 
-/-- Helper instance for when there's too many metavariables to apply `CoeFun.coe` directly. -/
-instance {μ : YoungDiagram} : CoeFun (SemistandardYoungTableau μ) fun _ ↦ ℕ → ℕ → ℕ :=
-  inferInstance
-
 @[simp]
 theorem to_fun_eq_coe {μ : YoungDiagram} {T : SemistandardYoungTableau μ} :
     T.entry = (T : ℕ → ℕ → ℕ) :=

Mathlib/Data/DFinsupp/Basic.lean

@@ -81,11 +81,6 @@ instance instDFunLike : DFunLike (Π₀ i, β i) ι β :=
     congr
     subsingleton ⟩
 
-/-- Helper instance for when there are too many metavariables to apply `DFunLike.coeFunForall`
-directly. -/
-instance : CoeFun (Π₀ i, β i) fun _ => ∀ i, β i :=
-  inferInstance
-
 @[simp]
 theorem toFun_eq_coe (f : Π₀ i, β i) : f.toFun = f :=
   rfl

Mathlib/Data/Finsupp/Defs.lean

@@ -116,11 +116,6 @@ instance instFunLike : FunLike (α →₀ M) α M :=
     ext a
     exact (hf _).trans (hg _).symm⟩
 
-/-- Helper instance for when there are too many metavariables to apply the `DFunLike` instance
-directly. -/
-instance instCoeFun : CoeFun (α →₀ M) fun _ => α → M :=
-  inferInstance
-
 @[ext]
 theorem ext {f g : α →₀ M} (h : ∀ a, f a = g a) : f = g :=
   DFunLike.ext _ _ h