chore: remove CoeFun instances where FunLike is available

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.

This is the first half of the changes, to see if those work without slowdowns.

Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean

@@ -89,9 +89,6 @@ instance equivLike : EquivLike (P₁ ≃ᵃ[k] P₂) P₁ P₂ where
   right_inv f := f.right_inv
   coe_injective' _ _ h _ := toAffineMap_injective (DFunLike.coe_injective h)
 
-instance : CoeFun (P₁ ≃ᵃ[k] P₂) fun _ => P₁ → P₂ :=
-  DFunLike.hasCoeToFun
-
 instance : CoeOut (P₁ ≃ᵃ[k] P₂) (P₁ ≃ P₂) :=
   ⟨AffineEquiv.toEquiv⟩
 

Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

@@ -67,11 +67,6 @@ instance AffineMap.instFunLike (k : Type*) {V1 : Type*} (P1 : Type*) {V2 : Type*
     apply vadd_right_cancel (f p)
     rw [← f_add, h, ← g_add]
 
-instance AffineMap.hasCoeToFun (k : Type*) {V1 : Type*} (P1 : Type*) {V2 : Type*} (P2 : Type*)
-    [Ring k] [AddCommGroup V1] [Module k V1] [AffineSpace V1 P1] [AddCommGroup V2] [Module k V2]
-    [AffineSpace V2 P2] : CoeFun (P1 →ᵃ[k] P2) fun _ => P1 → P2 :=
-  DFunLike.hasCoeToFun
-
 namespace LinearMap
 
 variable {k : Type*} {V₁ : Type*} {V₂ : Type*} [Ring k] [AddCommGroup V₁] [Module k V₁]

Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

@@ -161,11 +161,6 @@ instance instFunLike : FunLike (QuadraticMap R M N) M N where
   coe := toFun
   coe_injective' x y h := by cases x; cases y; congr
 
-/-- Helper instance for when there's too many metavariables to apply
-`DFunLike.hasCoeToFun` directly. -/
-instance : CoeFun (QuadraticMap R M N) fun _ => M → N :=
-  ⟨DFunLike.coe⟩
-
 variable (Q)
 
 /-- The `simp` normal form for a quadratic map is `DFunLike.coe`, not `toFun`. -/

Mathlib/MeasureTheory/OuterMeasure/Defs.lean

@@ -62,9 +62,6 @@ instance : FunLike (OuterMeasure α) (Set α) ℝ≥0∞ where
   coe m := m.measureOf
   coe_injective' | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, rfl => rfl
 
-instance instCoeFun : CoeFun (OuterMeasure α) (fun _ => Set α → ℝ≥0∞) :=
-  inferInstance
-
 @[simp] theorem measureOf_eq_coe (m : OuterMeasure α) : m.measureOf = m := rfl
 
 instance : OuterMeasureClass (OuterMeasure α) α where

Mathlib/ModelTheory/Basic.lean

@@ -296,9 +296,6 @@ instance homClass : HomClass L (M →[L] N) M N where
 instance [L.IsAlgebraic] : StrongHomClass L (M →[L] N) M N :=
   HomClass.strongHomClassOfIsAlgebraic
 
-instance hasCoeToFun : CoeFun (M →[L] N) fun _ => M → N :=
-  DFunLike.hasCoeToFun
-
 @[simp]
 theorem toFun_eq_coe {f : M →[L] N} : f.toFun = (f : M → N) :=
   rfl
@@ -557,9 +554,6 @@ def symm (f : M ≃[L] N) : N ≃[L] M :=
       refine (f.map_rel' r (f.toEquiv.symm ∘ x)).symm.trans ?_
       rw [← Function.comp_assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.id_comp] }
 
-instance hasCoeToFun : CoeFun (M ≃[L] N) fun _ => M → N :=
-  DFunLike.hasCoeToFun
-
 @[simp]
 theorem symm_symm (f : M ≃[L] N) :
     f.symm.symm = f :=

Mathlib/ModelTheory/ElementaryMaps.lean

@@ -67,9 +67,6 @@ instance instFunLike : FunLike (M ↪ₑ[L] N) M N where
     ext x
     exact funext_iff.1 h x
 
-instance : CoeFun (M ↪ₑ[L] N) fun _ => M → N :=
-  DFunLike.hasCoeToFun
-
 @[simp]
 theorem map_boundedFormula (f : M ↪ₑ[L] N) {α : Type*} {n : ℕ} (φ : L.BoundedFormula α n)
     (v : α → M) (xs : Fin n → M) : φ.Realize (f ∘ v) (f ∘ xs) ↔ φ.Realize v xs := by

Mathlib/Order/OmegaCompletePartialOrder.lean

@@ -72,7 +72,6 @@ variable [Preorder α] [Preorder β] [Preorder γ]
 
 instance : FunLike (Chain α) ℕ α := inferInstanceAs <| FunLike (ℕ →o α) ℕ α
 instance : OrderHomClass (Chain α) ℕ α := inferInstanceAs <| OrderHomClass (ℕ →o α) ℕ α
-instance : CoeFun (Chain α) fun _ => ℕ → α := ⟨DFunLike.coe⟩
 
 instance [Inhabited α] : Inhabited (Chain α) :=
   ⟨⟨default, fun _ _ _ => le_rfl⟩⟩

Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean

@@ -78,9 +78,6 @@ instance continuousMapClass :
     ContinuousMapClass (ContinuousMultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂ where
   map_continuous := ContinuousMultilinearMap.cont
 
-instance : CoeFun (ContinuousMultilinearMap R M₁ M₂) fun _ => (∀ i, M₁ i) → M₂ :=
-  ⟨fun f => f⟩
-
 /-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
   because it is a composition of multiple projections. -/
 def Simps.apply (L₁ : ContinuousMultilinearMap R M₁ M₂) (v : ∀ i, M₁ i) : M₂ :=

Mathlib/Topology/Algebra/Module/WeakDual.lean

@@ -102,11 +102,6 @@ instance instFunLike : FunLike (WeakDual 𝕜 E) E 𝕜 :=
 instance instContinuousLinearMapClass : ContinuousLinearMapClass (WeakDual 𝕜 E) 𝕜 E 𝕜 :=
   ContinuousLinearMap.continuousSemilinearMapClass
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.hasCoeToFun`
-directly. -/
-instance : CoeFun (WeakDual 𝕜 E) fun _ => E → 𝕜 :=
-  DFunLike.hasCoeToFun
-
 /-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with
 multiplication on `𝕜`, then it acts on `WeakDual 𝕜 E`. -/
 instance instMulAction (M) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜]

Mathlib/Topology/Connected/PathConnected.lean

@@ -85,12 +85,6 @@ instance Path.funLike : FunLike (Path x y) I X where
 instance Path.continuousMapClass : ContinuousMapClass (Path x y) I X where
   map_continuous γ := show Continuous γ.toContinuousMap by fun_prop
 
--- Porting note: not necessary in light of the instance above
-/-
-instance : CoeFun (Path x y) fun _ => I → X :=
-  ⟨fun p => p.toFun⟩
--/
-
 @[ext]
 protected theorem Path.ext : ∀ {γ₁ γ₂ : Path x y}, (γ₁ : I → X) = γ₂ → γ₁ = γ₂ := by
   rintro ⟨⟨x, h11⟩, h12, h13⟩ ⟨⟨x, h21⟩, h22, h23⟩ rfl

Mathlib/Topology/Homeomorph.lean

@@ -60,8 +60,6 @@ instance : EquivLike (X ≃ₜ Y) X Y where
   right_inv h := h.right_inv
   coe_injective' _ _ H _ := toEquiv_injective <| DFunLike.ext' H
 
-instance : CoeFun (X ≃ₜ Y) fun _ ↦ X → Y := ⟨DFunLike.coe⟩
-
 @[simp] theorem homeomorph_mk_coe (a : X ≃ Y) (b c) : (Homeomorph.mk a b c : X → Y) = a :=
   rfl
 

Mathlib/Topology/MetricSpace/Dilation.lean

@@ -87,9 +87,6 @@ instance funLike : FunLike (α →ᵈ β) α β where
 instance toDilationClass : DilationClass (α →ᵈ β) α β where
   edist_eq' f := edist_eq' f
 
-instance : CoeFun (α →ᵈ β) fun _ => α → β :=
-  DFunLike.hasCoeToFun
-
 @[simp]
 theorem toFun_eq_coe {f : α →ᵈ β} : f.toFun = (f : α → β) :=
   rfl

Mathlib/Topology/MetricSpace/DilationEquiv.lean

@@ -60,9 +60,6 @@ instance : EquivLike (X ≃ᵈ Y) X Y where
 instance : DilationEquivClass (X ≃ᵈ Y) X Y where
   edist_eq' f := f.edist_eq'
 
-instance : CoeFun (X ≃ᵈ Y) fun _ ↦ (X → Y) where
-  coe f := f
-
 @[simp] theorem coe_toEquiv (e : X ≃ᵈ Y) : ⇑e.toEquiv = e := rfl
 
 @[ext]