Second half of the second half of the first half of the changes.

Vierkantor · Vierkantor · commit b0a7beee3e9b · 2024-10-18T17:04:49.000+02:00
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]
