chore: remove CoeFun instances where FunLike is available

Vierkantor · Vierkantor · commit 36f0ed359e33 · 2024-10-17T16:09:20.000+02:00
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.
diff --git a/Mathlib/Algebra/MonoidAlgebra/Defs.lean b/Mathlib/Algebra/MonoidAlgebra/Defs.lean
@@ -86,7 +86,7 @@ instance MonoidAlgebra.instIsCancelAdd [IsCancelAdd k] : IsCancelAdd (MonoidAlge
   inferInstanceAs (IsCancelAdd (G →₀ k))
 
 instance MonoidAlgebra.coeFun : CoeFun (MonoidAlgebra k G) fun _ => G → k :=
-  Finsupp.instCoeFun
+  inferInstanceAs (CoeFun (G →₀ k) _)
 
 end
 
@@ -823,7 +823,7 @@ instance instIsCancelAdd [IsCancelAdd k] : IsCancelAdd (AddMonoidAlgebra k G) :=
   inferInstanceAs (IsCancelAdd (G →₀ k))
 
 instance coeFun : CoeFun k[G] fun _ => G → k :=
-  Finsupp.instCoeFun
+  inferInstanceAs (CoeFun (G →₀ k) _)
 
 end AddMonoidAlgebra
 
diff --git a/Mathlib/Algebra/Order/AbsoluteValue.lean b/Mathlib/Algebra/Order/AbsoluteValue.lean
@@ -77,11 +77,6 @@ def Simps.apply (f : AbsoluteValue R S) : R → S :=
 
 initialize_simps_projections AbsoluteValue (toMulHom_toFun → apply)
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.has_coe_to_fun`
-directly. -/
-instance : CoeFun (AbsoluteValue R S) fun _ => R → S :=
-  DFunLike.hasCoeToFun
-
 @[simp]
 theorem coe_toMulHom : ⇑abv.toMulHom = abv :=
   rfl
diff --git a/Mathlib/Algebra/Polynomial/Module/Basic.lean b/Mathlib/Algebra/Polynomial/Module/Basic.lean
@@ -56,9 +56,6 @@ noncomputable instance : Module S (PolynomialModule R M) :=
 instance instFunLike : FunLike (PolynomialModule R M) ℕ M :=
   Finsupp.instFunLike
 
-instance : CoeFun (PolynomialModule R M) fun _ => ℕ → M :=
-  Finsupp.instCoeFun
-
 theorem zero_apply (i : ℕ) : (0 : PolynomialModule R M) i = 0 :=
   Finsupp.zero_apply
 
diff --git a/Mathlib/Algebra/Ring/CentroidHom.lean b/Mathlib/Algebra/Ring/CentroidHom.lean
@@ -102,13 +102,6 @@ instance : CentroidHomClass (CentroidHom α) α where
   map_mul_right f := f.map_mul_right'
 
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.CoeFun`
-directly. -/
-/- Porting note: Lean gave me `unknown constant 'DFunLike.CoeFun'` and says `CoeFun` is a type
-mismatch, so I used `library_search`. -/
-instance : CoeFun (CentroidHom α) fun _ ↦ α → α :=
-  inferInstanceAs (CoeFun (CentroidHom α) fun _ ↦ α → α)
-
 -- Porting note: removed @[simp]; not in normal form. (`toAddMonoidHom_eq_coe` below ensures that
 -- the LHS simplifies to the RHS anyway.)
 theorem toFun_eq_coe {f : CentroidHom α} : f.toFun = f := rfl
diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace.lean b/Mathlib/Analysis/Distribution/SchwartzSpace.lean
@@ -90,10 +90,6 @@ instance instFunLike : FunLike 𝓢(E, F) E F where
   coe f := f.toFun
   coe_injective' f g h := by cases f; cases g; congr
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.hasCoeToFun`. -/
-instance instCoeFun : CoeFun 𝓢(E, F) fun _ => E → F :=
-  DFunLike.hasCoeToFun
-
 /-- All derivatives of a Schwartz function are rapidly decaying. -/
 theorem decay (f : 𝓢(E, F)) (k n : ℕ) :
     ∃ C : ℝ, 0 < C ∧ ∀ x, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C := by
diff --git a/Mathlib/Analysis/Normed/Algebra/Norm.lean b/Mathlib/Analysis/Normed/Algebra/Norm.lean
@@ -70,10 +70,6 @@ instance algebraNormClass : AlgebraNormClass (AlgebraNorm R S) R S where
   eq_zero_of_map_eq_zero f := f.eq_zero_of_map_eq_zero' _
   map_smul_eq_mul f := f.smul'
 
-/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`. -/
-instance : CoeFun (AlgebraNorm R S) fun _ => S → ℝ :=
-  DFunLike.hasCoeToFun
-
 theorem toFun_eq_coe (p : AlgebraNorm R S) : p.toFun = p := rfl
 
 @[ext]
@@ -160,10 +156,6 @@ instance mulAlgebraNormClass : MulAlgebraNormClass (MulAlgebraNorm R S) R S wher
   eq_zero_of_map_eq_zero f := f.eq_zero_of_map_eq_zero' _
   map_smul_eq_mul f := f.smul'
 
-/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`. -/
-instance : CoeFun (MulAlgebraNorm R S) fun _ => S → ℝ :=
-  DFunLike.hasCoeToFun
-
 theorem toFun_eq_coe (p : MulAlgebraNorm R S) : p.toFun = p := rfl
 
 @[ext]
diff --git a/Mathlib/Analysis/Normed/Group/Seminorm.lean b/Mathlib/Analysis/Normed/Group/Seminorm.lean
@@ -181,12 +181,6 @@ instance groupSeminormClass : GroupSeminormClass (GroupSeminorm E) E ℝ where
   map_mul_le_add f := f.mul_le'
   map_inv_eq_map f := f.inv'
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.hasCoeToFun`. -/
-@[to_additive "Helper instance for when there's too many metavariables to apply
-`DFunLike.hasCoeToFun`. "]
-instance : CoeFun (GroupSeminorm E) fun _ => E → ℝ :=
-  ⟨DFunLike.coe⟩
-
 @[to_additive (attr := simp)]
 theorem toFun_eq_coe : p.toFun = p :=
   rfl
@@ -447,10 +441,6 @@ instance nonarchAddGroupSeminormClass :
   map_zero f := f.map_zero'
   map_neg_eq_map' f := f.neg'
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.hasCoeToFun`. -/
-instance : CoeFun (NonarchAddGroupSeminorm E) fun _ => E → ℝ :=
-  ⟨DFunLike.coe⟩
-
 -- Porting note: `simpNF` said the left hand side simplified to this
 @[simp]
 theorem toZeroHom_eq_coe : ⇑p.toZeroHom = p := by
@@ -667,13 +657,6 @@ instance groupNormClass : GroupNormClass (GroupNorm E) E ℝ where
   map_inv_eq_map f := f.inv'
   eq_one_of_map_eq_zero f := f.eq_one_of_map_eq_zero' _
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.hasCoeToFun`
-directly. -/
-@[to_additive "Helper instance for when there's too many metavariables to apply
-`DFunLike.hasCoeToFun` directly. "]
-instance : CoeFun (GroupNorm E) fun _ => E → ℝ :=
-  DFunLike.hasCoeToFun
-
 -- Porting note: `simpNF` told me the left-hand side simplified to this
 @[to_additive (attr := simp)]
 theorem toGroupSeminorm_eq_coe : ⇑p.toGroupSeminorm = p :=
@@ -799,10 +782,6 @@ instance nonarchAddGroupNormClass : NonarchAddGroupNormClass (NonarchAddGroupNor
   map_neg_eq_map' f := f.neg'
   eq_zero_of_map_eq_zero f := f.eq_zero_of_map_eq_zero' _
 
-/-- Helper instance for when there's too many metavariables to apply `DFunLike.hasCoeToFun`. -/
-noncomputable instance : CoeFun (NonarchAddGroupNorm E) fun _ => E → ℝ :=
-  DFunLike.hasCoeToFun
-
 -- Porting note: `simpNF` told me the left-hand side simplified to this
 @[simp]
 theorem toNonarchAddGroupSeminorm_eq_coe : ⇑p.toNonarchAddGroupSeminorm = p :=
diff --git a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
@@ -486,11 +486,6 @@ 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. -/
-instance instCoeFun : CoeFun (E ≃ₛₗᵢ[σ₁₂] E₂) fun _ ↦ E → E₂ := ⟨DFunLike.coe⟩
-
 theorem coe_injective : @Function.Injective (E ≃ₛₗᵢ[σ₁₂] E₂) (E → E₂) (↑) :=
   DFunLike.coe_injective
 
diff --git a/Mathlib/Combinatorics/Young/SemistandardTableau.lean b/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 : ℕ → ℕ → ℕ) :=
diff --git a/Mathlib/Data/DFinsupp/Basic.lean b/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
diff --git a/Mathlib/Data/Finsupp/Defs.lean b/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
diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean b/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₁]
diff --git a/Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean b/Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean
@@ -73,9 +73,6 @@ instance instEquivLike : EquivLike (P₁ ≃ᵃL[k] P₂) P₁ P₂ where
   right_inv f := f.right_inv
   coe_injective' _ _ h _ := toAffineEquiv_injective (DFunLike.coe_injective h)
 
-instance : CoeFun (P₁ ≃ᵃL[k] P₂) fun _ ↦ P₁ → P₂ :=
-  DFunLike.hasCoeToFun
-
 attribute [coe] ContinuousAffineEquiv.toAffineEquiv
 
 /-- Coerce continuous affine equivalences to affine equivalences. -/
diff --git a/Mathlib/LinearAlgebra/Alternating/Basic.lean b/Mathlib/LinearAlgebra/Alternating/Basic.lean
@@ -93,10 +93,6 @@ instance instFunLike : FunLike (M [⋀^ι]→ₗ[R] N) (ι → M) N where
     rcases g with ⟨⟨_, _, _⟩, _⟩
     congr
 
--- shortcut instance
-instance coeFun : CoeFun (M [⋀^ι]→ₗ[R] N) fun _ => (ι → M) → N :=
-  ⟨DFunLike.coe⟩
-
 initialize_simps_projections AlternatingMap (toFun → apply)
 
 @[simp]
diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/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`. -/
diff --git a/Mathlib/MeasureTheory/OuterMeasure/Defs.lean b/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
diff --git a/Mathlib/Order/OmegaCompletePartialOrder.lean b/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⟩⟩
diff --git a/Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean b/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₂ :=
diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/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 𝕜]
diff --git a/Mathlib/Topology/Connected/PathConnected.lean b/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
diff --git a/Mathlib/Topology/Homeomorph.lean b/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
 
diff --git a/Mathlib/Topology/MetricSpace/Dilation.lean b/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
diff --git a/Mathlib/Topology/MetricSpace/DilationEquiv.lean b/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]
