diff --git a/Archive/Sensitivity.lean b/Archive/Sensitivity.lean
index 9b7d63d9bc709f..a766a59f8c18fd 100644
--- a/Archive/Sensitivity.lean
+++ b/Archive/Sensitivity.lean
@@ -285,7 +285,7 @@ using only the addition of `V`. -/
 set_option backward.isDefEq.respectTransparency false in
 theorem f_squared (v : V n) : (f n) (f n v) = (n : ℝ) • v := by
   induction n with
-  | zero => simp only [Nat.cast_zero, zero_smul, f_zero, zero_apply]
+  | zero => simp only [Nat.cast_zero, zero_smul, f_zero, LinearMap.zero_apply]
   | succ n IH =>
     cases v; rw [f_succ_apply, f_succ_apply]; simp [IH, add_smul (n : ℝ) 1, add_assoc]; abel
 
diff --git a/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean
index 97dccd4743e6a7..759fa8e157449b 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean
@@ -143,7 +143,7 @@ section
 variable {M₁ M₂ : TopModuleCat R}
 
 @[simp] lemma hom_zero : (0 : M₁ ⟶ M₂).hom = 0 := rfl
-@[simp] lemma hom_zero_apply (m : M₁) : (0 : M₁ ⟶ M₂).hom m = 0 := rfl
+lemma hom_zero_apply (m : M₁) : (0 : M₁ ⟶ M₂).hom m = 0 := rfl
 @[simp] lemma hom_add (φ₁ φ₂ : M₁ ⟶ M₂) : (φ₁ + φ₂).hom = φ₁.hom + φ₂.hom := rfl
 @[simp] lemma hom_neg (φ : M₁ ⟶ M₂) : (-φ).hom = -φ.hom := rfl
 @[simp] lemma hom_sub (φ₁ φ₂ : M₁ ⟶ M₂) : (φ₁ - φ₂).hom = φ₁.hom - φ₂.hom := rfl
diff --git a/Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean b/Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean
index 3c01d51041c96e..11f3a44f94c3cd 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean
@@ -85,7 +85,7 @@ def isColimitCoker : IsColimit (CokernelCofork.ofπ (cokerπ φ) (comp_cokerπ 
   (fun s ↦ ofHom <|
     { toLinearMap := φ.hom.range.liftQ s.π.hom.toLinearMap
         (LinearMap.range_le_ker_iff.mpr <| show (φ ≫ s.π).hom.toLinearMap = 0 by
-          rw [s.condition, hom_zero, ContinuousLinearMap.coe_zero])
+          rw [s.condition, hom_zero, ContinuousLinearMap.toLinearMap_zero])
       cont := Continuous.quotient_lift s.π.hom.2 _ })
   (fun s ↦ rfl)
   (fun s m h ↦ by dsimp at h ⊢; rw [← cancel_epi (cokerπ φ), h]; rfl)
@@ -113,7 +113,7 @@ instance : CategoryWithHomology (TopModuleCat R) := by
       (Submodule.isOpenQuotientMap_mkQ _).isQuotientMap
       (Submodule.isOpenQuotientMap_mkQ _)
       (Subtype.val_injective.comp hF.1) ?_
-    · rw [← ContinuousLinearMap.coe_comp', ← ContinuousLinearMap.coe_comp',
+    · rw [← ContinuousLinearMap.coe_comp, ← ContinuousLinearMap.coe_comp,
         ← hom_comp, ← hom_comp, ShortComplex.π_leftRightHomologyComparison'_ι]
     · suffices ∀ x y, S.g y = 0 → D₂.p y = D₂.p x → S.g x = 0 by
         simpa [Set.subset_def, D₁, kerι_apply S.g] using this
diff --git a/Mathlib/Analysis/Analytic/Binomial.lean b/Mathlib/Analysis/Analytic/Binomial.lean
index b48638486df97f..f155a1e5126456 100644
--- a/Mathlib/Analysis/Analytic/Binomial.lean
+++ b/Mathlib/Analysis/Analytic/Binomial.lean
@@ -183,7 +183,7 @@ theorem one_div_sub_pow_hasFPowerSeriesOnBall_zero (a : ℕ) {z : ℂ} (hz : z 
   rw [← map_zero (z⁻¹ • 1 : ℂ →L[ℂ] ℂ)] at this
   have := this.compContinuousLinearMap
   have H : 1 / ‖(z⁻¹ • 1 : ℂ →L[ℂ] ℂ)‖ₑ = ‖z‖ₑ := by simp [enorm_smul, enorm_inv, hz]
-  simp only [one_div, ContinuousLinearMap.coe_smul', H, Function.comp_def] at this
+  simp only [one_div, FunLike.coe_smul, H, Function.comp_def] at this
   convert! (this.const_smul (c := (z ^ (a + 1))⁻¹)).congr ?_ using 2
   · ext n
     simp only [FormalMultilinearSeries.smul_apply, ContinuousMultilinearMap.smul_apply,
diff --git a/Mathlib/Analysis/Analytic/IteratedFDeriv.lean b/Mathlib/Analysis/Analytic/IteratedFDeriv.lean
index 61168105022f72..2019cd650302ed 100644
--- a/Mathlib/Analysis/Analytic/IteratedFDeriv.lean
+++ b/Mathlib/Analysis/Analytic/IteratedFDeriv.lean
@@ -100,7 +100,7 @@ lemma FormalMultilinearSeries.iteratedFDerivSeries_eq_zero {k n : ℕ}
       ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe,
       LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply,
       continuousMultilinearCurryLeftEquiv_symm_apply, ContinuousMultilinearMap.zero_apply,
-      ContinuousLinearMap.zero_apply,
+      _root_.zero_apply,
       derivSeries_eq_zero _ (ih (p.congr_zero (Nat.succ_add_eq_add_succ _ _).symm h))]
 
 /-- If the `n`-th term in a power series is zero, then the `n`-th derivative of the corresponding
diff --git a/Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean b/Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
index 4db5f19f1e3938..7ed03d6b564b4e 100644
--- a/Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
+++ b/Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
@@ -485,13 +485,13 @@ noncomputable def toCLM : CStarMatrix m n A →ₗ[ℂ] C⋆ᵐᵒᵈ(A, m → A
     ext
     simp only [ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
       WithCStarModule.equivL_apply, WithCStarModule.equivL_symm_apply,
-      WithCStarModule.equiv_symm_pi_apply, ContinuousLinearMap.add_apply, WithCStarModule.add_apply]
+      WithCStarModule.equiv_symm_pi_apply, _root_.add_apply, WithCStarModule.add_apply]
     rw [Matrix.vecMul_add, Pi.add_apply]
   map_smul' c M := by
     ext x i
     simp only [ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
       WithCStarModule.equivL_apply, WithCStarModule.equivL_symm_apply,
-      WithCStarModule.equiv_symm_pi_apply, ContinuousLinearMap.smul_apply,
+      WithCStarModule.equiv_symm_pi_apply, _root_.smul_apply,
       WithCStarModule.smul_apply, RingHom.id_apply]
     rw [Matrix.vecMul_smul, Pi.smul_apply]
 
diff --git a/Mathlib/Analysis/CStarAlgebra/Multiplier.lean b/Mathlib/Analysis/CStarAlgebra/Multiplier.lean
index ab2e3eab4d4bdd..2e7e3627c8e6b8 100644
--- a/Mathlib/Analysis/CStarAlgebra/Multiplier.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Multiplier.lean
@@ -113,7 +113,7 @@ instance instAdd : Add 𝓜(𝕜, A) where
     { toProd := a.toProd + b.toProd
       central := fun x y =>
         show (a.snd + b.snd) x * y = x * (a.fst + b.fst) y by
-          simp only [ContinuousLinearMap.add_apply, mul_add, add_mul, central] }
+          simp only [add_apply, mul_add, add_mul, central] }
 
 instance instZero : Zero 𝓜(𝕜, A) where
   zero :=
@@ -132,7 +132,7 @@ instance instSub : Sub 𝓜(𝕜, A) where
     { toProd := a.toProd - b.toProd
       central := fun x y =>
         show (a.snd - b.snd) x * y = x * (a.fst - b.fst) y by
-          simp only [ContinuousLinearMap.sub_apply, _root_.sub_mul, _root_.mul_sub, central] }
+          simp only [sub_apply, _root_.sub_mul, _root_.mul_sub, central] }
 
 section Scalars
 
@@ -144,7 +144,7 @@ instance instSMul : SMul S 𝓜(𝕜, A) where
     { toProd := s • a.toProd
       central := fun x y =>
         show (s • a.snd) x * y = x * (s • a.fst) y by
-          simp only [ContinuousLinearMap.smul_apply, mul_smul_comm, smul_mul_assoc, central] }
+          simp only [smul_apply, mul_smul_comm, smul_mul_assoc, central] }
 
 @[simp]
 theorem smul_toProd (s : S) (a : 𝓜(𝕜, A)) : (s • a).toProd = s • a.toProd :=
@@ -184,13 +184,15 @@ instance instNatCast : NatCast 𝓜(𝕜, A) where
   natCast n :=
     ⟨n, fun x y => by
       rw [Prod.snd_natCast, Prod.fst_natCast]
-      simp only [← Nat.smul_one_eq_cast, smul_apply, one_apply, mul_smul_comm, smul_mul_assoc]⟩
+      simp only [← Nat.smul_one_eq_cast, smul_apply, one_apply_eq_self, mul_smul_comm,
+        smul_mul_assoc]⟩
 
 instance instIntCast : IntCast 𝓜(𝕜, A) where
   intCast n :=
     ⟨n, fun x y => by
       rw [Prod.snd_intCast, Prod.fst_intCast]
-      simp only [← Int.smul_one_eq_cast, smul_apply, one_apply, mul_smul_comm, smul_mul_assoc]⟩
+      simp only [← Int.smul_one_eq_cast, smul_apply, one_apply_eq_self, mul_smul_comm,
+        smul_mul_assoc]⟩
 
 instance instPow : Pow 𝓜(𝕜, A) ℕ where
   pow a n :=
@@ -199,7 +201,7 @@ instance instPow : Pow 𝓜(𝕜, A) ℕ where
       | zero => rfl
       | succ k hk =>
         rw [Prod.pow_snd, Prod.pow_fst] at hk ⊢
-        rw [pow_succ' a.snd, mul_apply, a.central, hk, pow_succ a.fst, mul_apply]⟩
+        rw [pow_succ' a.snd, mul_apply_eq_comp, a.central, hk, pow_succ a.fst, mul_apply_eq_comp]⟩
 
 instance instInhabited : Inhabited 𝓜(𝕜, A) :=
   ⟨0⟩
@@ -347,8 +349,8 @@ instance instAlgebra : Algebra 𝕜 𝓜(𝕜, A) where
   { toFun k :=
       { toProd := algebraMap 𝕜 ((A →L[𝕜] A) × (A →L[𝕜] A)) k
         central := fun x y => by
-          simp_rw [Prod.algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_apply, one_apply,
-            mul_smul_comm, smul_mul_assoc] }
+          simp_rw [Prod.algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_apply,
+            one_apply_eq_self, mul_smul_comm, smul_mul_assoc] }
     map_one' := ext (𝕜 := 𝕜) (A := A) _ _ <| map_one <| algebraMap 𝕜 ((A →L[𝕜] A) × (A →L[𝕜] A))
     map_mul' _ _ :=
       ext (𝕜 := 𝕜) (A := A) _ _ <|
@@ -611,7 +613,7 @@ instance instCStarRing : CStarRing 𝓜(𝕜, A) where
               (a.fst.le_opNorm_of_le hy))
           _ ≤ ‖a‖₊ * ‖a‖₊ := by simp only [mul_one, nnnorm_fst, le_rfl]
       rw [← nnnorm_snd]
-      simp only [mul_snd, ← sSup_unitClosedBall_eq_nnnorm, star_snd, mul_apply]
+      simp only [mul_snd, ← sSup_unitClosedBall_eq_nnnorm, star_snd, mul_apply_eq_comp]
       simp only [← @opNNNorm_mul_apply 𝕜 _ A]
       simp only [← sSup_unitClosedBall_eq_nnnorm, mul_apply']
       refine csSup_eq_of_forall_le_of_forall_lt_exists_gt (hball.image _) ?_ fun r hr => ?_
diff --git a/Mathlib/Analysis/CStarAlgebra/Unitization.lean b/Mathlib/Analysis/CStarAlgebra/Unitization.lean
index dbf98f1999989f..3e1ef0b0d4f8ca 100644
--- a/Mathlib/Analysis/CStarAlgebra/Unitization.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Unitization.lean
@@ -98,9 +98,9 @@ theorem Unitization.norm_splitMul_snd_sq (x : Unitization 𝕜 E) :
   simp only
   -- rewrite to a more convenient form; this is where we use the C⋆-property
   rw [← Real.sqrt_sq (norm_nonneg _), Real.sqrt_le_sqrt_iff (norm_nonneg _), sq,
-    ← CStarRing.norm_star_mul_self, ContinuousLinearMap.add_apply, star_add, mul_apply',
-    Algebra.algebraMap_eq_smul_one, ContinuousLinearMap.smul_apply,
-    ContinuousLinearMap.one_apply, star_mul, star_smul, add_mul, smul_mul_assoc, ← mul_smul_comm,
+    ← CStarRing.norm_star_mul_self, add_apply, star_add, mul_apply',
+    Algebra.algebraMap_eq_smul_one, smul_apply,
+    one_apply_eq_self, star_mul, star_smul, add_mul, smul_mul_assoc, ← mul_smul_comm,
     mul_assoc, ← mul_add, ← sSup_unitClosedBall_eq_norm]
   refine (norm_mul_le _ _).trans ?_
   calc
@@ -119,9 +119,9 @@ theorem Unitization.norm_splitMul_snd_sq (x : Unitization 𝕜 E) :
       simpa only [mul_one] using!
         mul_le_mul_of_nonneg_left (mem_closedBall_zero_iff.1 hy) (norm_nonneg (star x * x).fst)
     · exact (unit_le_opNorm _ y <| mem_closedBall_zero_iff.1 hy).trans (opNorm_mul_apply_le _ _ _)
-  · simp only [ContinuousLinearMap.add_apply, mul_apply', Unitization.snd_star, Unitization.snd_mul,
+  · simp only [add_apply, mul_apply', Unitization.snd_star, Unitization.snd_mul,
       Unitization.fst_mul, Unitization.fst_star, Algebra.algebraMap_eq_smul_one, smul_apply,
-      one_apply, smul_add, mul_add, add_mul]
+      one_apply_eq_self, smul_add, mul_add, add_mul]
     simp only [smul_smul, smul_mul_assoc, ← add_assoc, ← mul_assoc, mul_smul_comm]
 
 variable {𝕜}
diff --git a/Mathlib/Analysis/Calculus/AbsolutelyMonotone.lean b/Mathlib/Analysis/Calculus/AbsolutelyMonotone.lean
index edd4a6a92a2432..79825130a34cf8 100644
--- a/Mathlib/Analysis/Calculus/AbsolutelyMonotone.lean
+++ b/Mathlib/Analysis/Calculus/AbsolutelyMonotone.lean
@@ -116,7 +116,7 @@ theorem smul {c : ℝ} (hf : AbsolutelyMonotoneOn f s) (hc : 0 ≤ c) :
   have hcomp : (T ∘ f) = c • f := by ext x; simp [hT, smul_eq_mul]
   refine ⟨_, hcomp ▸ hp.continuousLinearMap_comp T, fun n x hx => ?_⟩
   simp only [ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply, hT,
-    ContinuousLinearMap.smul_apply, ContinuousLinearMap.id_apply, smul_eq_mul]
+    smul_apply, ContinuousLinearMap.id_apply, smul_eq_mul]
   exact mul_nonneg hc (hp_nn n hx)
 
 end AbsolutelyMonotoneOn
diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean
index 8782686073b4aa..1b47d10f546325 100644
--- a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean
+++ b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean
@@ -277,10 +277,7 @@ theorem ContinuousLinearEquiv.iteratedFDerivWithin_comp_left (g : F ≃L[𝕜] G
       fderivWithin_congr' (@IH) hx
     simp_rw [Z]
     rw [(g.continuousMultilinearMapCongrRight fun _ : Fin i => E).comp_fderivWithin (hs x hx)]
-    simp only [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, comp_apply,
-      ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply,
-      ContinuousLinearMap.compContinuousMultilinearMap_coe, EmbeddingLike.apply_eq_iff_eq]
-    rw [iteratedFDerivWithin_succ_apply_left]
+    simp [iteratedFDerivWithin_succ_apply_left]
 
 /-- Iterated derivatives commute with left composition by continuous linear equivalences. -/
 theorem ContinuousLinearEquiv.iteratedFDeriv_comp_left {f : E → F} {x : E} (g : F ≃L[𝕜] G) {i : ℕ} :
@@ -452,11 +449,11 @@ theorem ContinuousLinearEquiv.iteratedFDerivWithin_comp_right (g : G ≃L[𝕜]
             (iteratedFDerivWithin 𝕜 i f s ∘ g)) (g ⁻¹' s) x :=
       fderivWithin_congr' (@IH) hx
     rw [this, ContinuousLinearEquiv.comp_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx)]
-    simp only [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, comp_apply,
+    simp only [ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe,
       ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply,
       ContinuousMultilinearMap.compContinuousLinearMap_apply]
     rw [ContinuousLinearEquiv.comp_right_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx),
-      ContinuousLinearMap.coe_comp', coe_coe, comp_apply, tail_def, tail_def]
+      ContinuousLinearMap.comp_apply, coe_coe, tail_def, tail_def]
 
 /-- The iterated derivative of the composition with a linear map on the right is
 obtained by composing the iterated derivative with the linear map. -/
diff --git a/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean b/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
index a4c1b1f6dc7ed3..fa113ea69a5af7 100644
--- a/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
+++ b/Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
@@ -154,9 +154,8 @@ theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear (B : E →L
   have Bu_le : ‖Bu‖ ≤ ‖B‖ := by
     refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg B) fun y => ?_
     refine ContinuousLinearMap.opNorm_le_bound _ (by positivity) fun x => ?_
-    simp only [Eu, Fu, Gu, hBu, Bu₀, compL_apply, coe_comp', Function.comp_apply,
-      ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_coe, flip_apply,
-      LinearIsometryEquiv.norm_map]
+    simp only [Eu, Fu, Gu, hBu, Bu₀, compL_apply, comp_apply, ContinuousLinearEquiv.coe_coe,
+      LinearIsometryEquiv.coe_coe, flip_apply, LinearIsometryEquiv.norm_map]
     calc
       ‖B (isoE y) (isoF x)‖ ≤ ‖B (isoE y)‖ * ‖isoF x‖ := ContinuousLinearMap.le_opNorm _ _
       _ ≤ ‖B‖ * ‖isoE y‖ * ‖isoF x‖ := by gcongr; apply ContinuousLinearMap.le_opNorm
diff --git a/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean b/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
index 23af6e15d7e212..6b24f9ee7aaf84 100644
--- a/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
+++ b/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
@@ -1011,7 +1011,7 @@ private lemma faaDiBruno_aux1 {m : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
   simp only [Nat.succ_eq_add_one, OrderedFinpartition.extend, extendLeft,
     ContinuousMultilinearMap.curryLeft_apply,
     FormalMultilinearSeries.compAlongOrderedFinpartition_apply, applyOrderedFinpartition_apply,
-    ContinuousLinearMap.coe_comp', comp_apply, continuousMultilinearCurryFin1_apply,
+    ContinuousLinearMap.comp_apply, continuousMultilinearCurryFin1_apply,
     Matrix.zero_empty, ContinuousLinearMap.flipMultilinear_apply_apply,
     compAlongOrderedFinpartitionL_apply, compAlongOrderFinpartition_apply]
   congr
@@ -1032,7 +1032,7 @@ private lemma faaDiBruno_aux2 {m : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
   simp? [OrderedFinpartition.extend, extendMiddle, applyOrderedFinpartition_apply] says
     simp only [OrderedFinpartition.extend, extendMiddle, ContinuousMultilinearMap.curryLeft_apply,
       Nat.succ_eq_add_one, FormalMultilinearSeries.compAlongOrderedFinpartition_apply,
-      applyOrderedFinpartition_apply, ContinuousLinearMap.coe_comp', comp_apply,
+      applyOrderedFinpartition_apply, ContinuousLinearMap.comp_apply,
       ContinuousMultilinearMap.toContinuousLinearMap_apply, compAlongOrderedFinpartitionL_apply,
       compAlongOrderFinpartition_apply]
   congr
@@ -1101,8 +1101,7 @@ theorem HasFTaylorSeriesUpToOn.comp {n : WithTop ℕ∞} {g : F → G} {f : E 
       ext v
       simp only [Nat.succ_eq_add_one, Fintype.sum_option, ContinuousMultilinearMap.curryLeft_apply,
         ContinuousMultilinearMap.sum_apply, ContinuousMultilinearMap.add_apply,
-        FormalMultilinearSeries.compAlongOrderedFinpartition_apply, ContinuousLinearMap.coe_sum',
-        Finset.sum_apply, ContinuousLinearMap.add_apply]
+        FormalMultilinearSeries.compAlongOrderedFinpartition_apply, sum_apply, add_apply]
     rw [Finset.sum_sigma']
     exact Fintype.sum_equiv (OrderedFinpartition.extendEquiv m) _ _ (fun p ↦ rfl)
   · intro m hm
diff --git a/Mathlib/Analysis/Calculus/ContDiff/Operations.lean b/Mathlib/Analysis/Calculus/ContDiff/Operations.lean
index 326be2fca3b1ac..7fb93ae9a9881d 100644
--- a/Mathlib/Analysis/Calculus/ContDiff/Operations.lean
+++ b/Mathlib/Analysis/Calculus/ContDiff/Operations.lean
@@ -284,7 +284,7 @@ theorem iteratedFDerivWithin_neg_apply {f : E → F} (hu : UniqueDiffOn 𝕜 s)
       _ = fderivWithin 𝕜 (-iteratedFDerivWithin 𝕜 i f s) s x (h 0) (Fin.tail h) := by
         rw [fderivWithin_congr' (@hi) hx, Pi.neg_def]
       _ = -(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s) x (h 0) (Fin.tail h) := by
-        rw [fderivWithin_neg (hu x hx), ContinuousLinearMap.neg_apply,
+        rw [fderivWithin_neg (hu x hx), neg_apply,
           ContinuousMultilinearMap.neg_apply]
       _ = -(iteratedFDerivWithin 𝕜 (i + 1) f s) x h := by
         rw [iteratedFDerivWithin_succ_apply_left]
diff --git a/Mathlib/Analysis/Calculus/Darboux.lean b/Mathlib/Analysis/Calculus/Darboux.lean
index dac2d10f8337be..87654360ce1e8f 100644
--- a/Mathlib/Analysis/Calculus/Darboux.lean
+++ b/Mathlib/Analysis/Calculus/Darboux.lean
@@ -45,7 +45,7 @@ theorem exists_hasDerivWithinAt_eq_of_gt_of_lt (hab : a ≤ b)
         (not_le_of_gt hma)
       have : b - a ∈ posTangentConeAt (Icc a b) a :=
         sub_mem_posTangentConeAt_of_segment_subset (segment_eq_Icc hab ▸ Subset.rfl)
-      simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply]
+      simpa only [ContinuousLinearMap.smulRight_apply, one_apply_eq_self]
         using! hc.localize.hasFDerivWithinAt_nonneg (hg a (left_mem_Icc.2 hab)) this
     rcases cmem.2.eq_or_lt' with (rfl | hcb)
     -- Show that `c` can't be equal to `b`
@@ -53,7 +53,7 @@ theorem exists_hasDerivWithinAt_eq_of_gt_of_lt (hab : a ≤ b)
         (not_le_of_gt hmb)
       have : a - b ∈ posTangentConeAt (Icc a b) b :=
         sub_mem_posTangentConeAt_of_segment_subset (by rw [segment_symm, segment_eq_Icc hab])
-      simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply]
+      simpa only [ContinuousLinearMap.smulRight_apply, one_apply_eq_self]
         using! hc.localize.hasFDerivWithinAt_nonneg (hg b (right_mem_Icc.2 hab)) this
     exact ⟨hac, hcb⟩
   use c, cmem'
diff --git a/Mathlib/Analysis/Calculus/Deriv/Add.lean b/Mathlib/Analysis/Calculus/Deriv/Add.lean
index 4ab42275c25c4e..abf6222dfea024 100644
--- a/Mathlib/Analysis/Calculus/Deriv/Add.lean
+++ b/Mathlib/Analysis/Calculus/Deriv/Add.lean
@@ -271,12 +271,12 @@ theorem HasStrictDerivAt.neg (h : HasStrictDerivAt f f' x) : HasStrictDerivAt (-
 @[to_fun]
 theorem derivWithin.neg : derivWithin (-f) s x = -derivWithin f s x := by
   by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-  · simp only [derivWithin, fderivWithin_neg hsx, ContinuousLinearMap.neg_apply]
+  · simp only [derivWithin, fderivWithin_neg hsx, neg_apply]
   · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
 
 @[to_fun]
 theorem deriv.neg : deriv (-f) x = -deriv f x := by
-  simp only [deriv, fderiv_neg, ContinuousLinearMap.neg_apply]
+  simp only [deriv, fderiv_neg, neg_apply]
 
 @[to_fun (attr := simp)]
 theorem deriv.neg' : (deriv (-f)) = fun x ↦ -deriv f x :=
diff --git a/Mathlib/Analysis/Calculus/Deriv/Basic.lean b/Mathlib/Analysis/Calculus/Deriv/Basic.lean
index 74f4ba8a3d68de..8158b0abeb227d 100644
--- a/Mathlib/Analysis/Calculus/Deriv/Basic.lean
+++ b/Mathlib/Analysis/Calculus/Deriv/Basic.lean
@@ -238,14 +238,14 @@ variable {s t : Set 𝕜}
 variable {L L₁ L₂ : Filter (𝕜 × 𝕜)}
 
 theorem derivWithin_zero_of_not_accPt (h : ¬AccPt x (𝓟 s)) : derivWithin f s x = 0 := by
-  rw [derivWithin, fderivWithin_zero_of_not_accPt h, ContinuousLinearMap.zero_apply]
+  rw [derivWithin, fderivWithin_zero_of_not_accPt h, zero_apply]
 
 theorem derivWithin_zero_of_not_uniqueDiffWithinAt (h : ¬UniqueDiffWithinAt 𝕜 s x) :
     derivWithin f s x = 0 :=
   derivWithin_zero_of_not_accPt <| mt AccPt.uniqueDiffWithinAt h
 
 theorem derivWithin_zero_of_notMem_closure (h : x ∉ closure s) : derivWithin f s x = 0 := by
-  rw [derivWithin, fderivWithin_zero_of_notMem_closure h, ContinuousLinearMap.zero_apply]
+  rw [derivWithin, fderivWithin_zero_of_notMem_closure h, zero_apply]
 
 theorem deriv_zero_of_not_differentiableAt (h : ¬DifferentiableAt 𝕜 f x) : deriv f x = 0 := by
   unfold deriv
diff --git a/Mathlib/Analysis/Calculus/Deriv/CompMul.lean b/Mathlib/Analysis/Calculus/Deriv/CompMul.lean
index 78bbee7d817f32..34c03da1a2670d 100644
--- a/Mathlib/Analysis/Calculus/Deriv/CompMul.lean
+++ b/Mathlib/Analysis/Calculus/Deriv/CompMul.lean
@@ -41,4 +41,4 @@ theorem derivWithin_comp_mul_left :
 
 variable (c f x) in
 theorem deriv_comp_mul_left : deriv (f <| c * ·) x = c • deriv f (c * x) := by
-  simp only [← smul_eq_mul, deriv, fderiv_comp_smul, ContinuousLinearMap.smul_apply]
+  simp only [← smul_eq_mul, deriv, fderiv_comp_smul, smul_apply]
diff --git a/Mathlib/Analysis/Calculus/Deriv/Mul.lean b/Mathlib/Analysis/Calculus/Deriv/Mul.lean
index 64ab0635d2cedf..f2ee38a74335a6 100644
--- a/Mathlib/Analysis/Calculus/Deriv/Mul.lean
+++ b/Mathlib/Analysis/Calculus/Deriv/Mul.lean
@@ -410,8 +410,7 @@ variable {ι : Type*} [DecidableEq ι] {𝔸' : Type*} [NormedCommRing 𝔸'] [N
 
 theorem HasDerivAt.fun_finsetProd (hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x) :
     HasDerivAt (∏ i ∈ u, f i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x := by
-  simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
-    (HasFDerivAt.finsetProd (fun i hi ↦ (hf i hi).hasFDerivAt)).hasDerivAt
+  simpa using (HasFDerivAt.finsetProd (hf · · |> hasFDerivAt)).hasDerivAt
 
 @[deprecated (since := "2026-04-08")] alias HasDerivAt.fun_finset_prod := HasDerivAt.fun_finsetProd
 
@@ -423,8 +422,7 @@ theorem HasDerivAt.finsetProd (hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x) :
 
 theorem HasDerivWithinAt.fun_finsetProd (hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x) :
     HasDerivWithinAt (∏ i ∈ u, f i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) s x := by
-  simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
-    (HasFDerivWithinAt.finsetProd (fun i hi ↦ (hf i hi).hasFDerivWithinAt)).hasDerivWithinAt
+  simpa using (HasFDerivWithinAt.finsetProd (hf · · |> hasFDerivWithinAt)).hasDerivWithinAt
 
 @[deprecated (since := "2026-04-08")]
 alias HasDerivWithinAt.fun_finset_prod := HasDerivWithinAt.fun_finsetProd
@@ -438,8 +436,7 @@ alias HasDerivWithinAt.finset_prod := HasDerivWithinAt.finsetProd
 
 theorem HasStrictDerivAt.fun_finsetProd (hf : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x) :
     HasStrictDerivAt (∏ i ∈ u, f i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x := by
-  simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
-    (HasStrictFDerivAt.finsetProd (fun i hi ↦ (hf i hi).hasStrictFDerivAt)).hasStrictDerivAt
+  simpa using (HasStrictFDerivAt.finsetProd (hf · · |> hasStrictFDerivAt)).hasStrictDerivAt
 
 @[deprecated (since := "2026-04-08")]
 alias HasStrictDerivAt.fun_finset_prod := HasStrictDerivAt.fun_finsetProd
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Add.lean b/Mathlib/Analysis/Calculus/FDeriv/Add.lean
index 1e2cc503439d5f..3b517d59265c11 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Add.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Add.lean
@@ -192,7 +192,7 @@ section Add
 theorem HasFDerivAtFilter.add (hf : HasFDerivAtFilter f f' L)
     (hg : HasFDerivAtFilter g g' L) : HasFDerivAtFilter (f + g) (f' + g') L :=
   .of_isLittleO <| (hf.isLittleO.add hg.isLittleO).congr_left fun _ => by
-    grind [Pi.add_apply, ContinuousLinearMap.add_apply]
+    grind [Pi.add_apply]
 
 @[to_fun (attr := fun_prop)]
 theorem HasStrictFDerivAt.add (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) :
@@ -403,7 +403,7 @@ theorem HasStrictFDerivAt.fun_sum (h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A'
     HasStrictFDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x := by
   simp only [hasStrictFDerivAt_iff_isLittleO] at *
   convert! IsLittleO.sum h
-  simp [Finset.sum_sub_distrib, ContinuousLinearMap.sum_apply]
+  simp [Finset.sum_sub_distrib]
 
 @[fun_prop]
 theorem HasStrictFDerivAt.sum (h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x) :
@@ -414,7 +414,7 @@ theorem HasFDerivAtFilter.fun_sum (h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A'
     HasFDerivAtFilter (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) L := by
   simp only [hasFDerivAtFilter_iff_isLittleO] at *
   convert! IsLittleO.sum h
-  simp [ContinuousLinearMap.sum_apply]
+  simp
 
 theorem HasFDerivAtFilter.sum (h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) L) :
     HasFDerivAtFilter (∑ i ∈ u, A i) (∑ i ∈ u, A' i) L := by
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
index 73fa63240dea5c..117d0433267872 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
@@ -330,7 +330,7 @@ theorem HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt
   rw [this] at Z
   convert! Z with n
   ext v
-  simp only [FormalMultilinearSeries.derivSeries, ContinuousLinearMap.coe_sum', Finset.sum_apply,
+  simp only [FormalMultilinearSeries.derivSeries, sum_apply,
     ContinuousLinearMap.compFormalMultilinearSeries_apply,
     FormalMultilinearSeries.changeOriginSeries,
     ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe,
@@ -741,8 +741,8 @@ theorem hasFTaylorSeriesUpTo_iteratedFDeriv :
     ext v m
     simp only [ContinuousMultilinearMap.iteratedFDeriv, curryLeft_apply, sum_apply,
       iteratedFDerivComponent_apply, Finset.univ_sigma_univ,
-      Pi.compRightL_apply, ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_comp',
-      Finset.sum_apply, Function.comp_apply, linearDeriv_apply, Finset.sum_sigma']
+      Pi.compRightL_apply, _root_.sum_apply, ContinuousLinearMap.comp_apply, linearDeriv_apply,
+      Finset.sum_sigma']
     rw [← (Equiv.embeddingFinSucc n ι).sum_comp]
     congr with e
     congr with k
@@ -795,7 +795,7 @@ theorem derivSeries_apply_diag (n : ℕ) (x : E) :
     derivSeries p n (fun _ ↦ x) x = (n + 1) • p (n + 1) fun _ ↦ x := by
   simp only [derivSeries, compFormalMultilinearSeries_apply, changeOriginSeries,
     compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_coe,
-    Function.comp_apply, ContinuousMultilinearMap.sum_apply, map_sum, coe_sum', Finset.sum_apply,
+    Function.comp_apply, ContinuousMultilinearMap.sum_apply, map_sum, _root_.sum_apply,
     continuousMultilinearCurryFin1_apply, Matrix.zero_empty]
   convert! Finset.sum_const _
   · rw [Fin.snoc_zero, changeOriginSeriesTerm_apply, Finset.piecewise_same, add_comm]
@@ -830,7 +830,7 @@ private theorem factorial_smul' {n : ℕ} : ∀ {F : Type max u v} [NormedAddCom
   induction n with | zero => _ | succ n ih => _ <;> intro F _ _ _ p f h
   · rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
   · rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag,
-      ← ContinuousLinearMap.smul_apply, ih h.fderiv, iteratedFDeriv_succ_apply_right]
+      ← _root_.smul_apply, ih h.fderiv, iteratedFDeriv_succ_apply_right]
     rfl
 
 variable [CompleteSpace F]
@@ -845,7 +845,7 @@ theorem factorial_smul (n : ℕ) :
   cases n
   · rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
   · rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag,
-      ← ContinuousLinearMap.smul_apply, factorial_smul' _ h.fderiv, iteratedFDeriv_succ_apply_right]
+      ← _root_.smul_apply, factorial_smul' _ h.fderiv, iteratedFDeriv_succ_apply_right]
     rfl
 
 theorem hasSum_iteratedFDeriv [CharZero 𝕜] {y : E} (hy : y ∈ Metric.eball 0 r) :
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Comp.lean b/Mathlib/Analysis/Calculus/FDeriv/Comp.lean
index eb3c8375b23f03..b569401f8f2ceb 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Comp.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Comp.lean
@@ -159,7 +159,7 @@ theorem fderivWithin_fderivWithin {g : F → G} {f : E → F} {x : E} {y : F} {s
     (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) (v : E) :
     fderivWithin 𝕜 g t y (fderivWithin 𝕜 f s x v) = fderivWithin 𝕜 (g ∘ f) s x v := by
   subst y
-  rw [fderivWithin_comp x hg hf h hxs, coe_comp', Function.comp_apply]
+  rw [fderivWithin_comp x hg hf h hxs, comp_apply]
 
 /-- Ternary version of `fderivWithin_comp`, with equality assumptions of basepoints added, in
   order to apply more easily as a rewrite from right-to-left. -/
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Norm.lean b/Mathlib/Analysis/Calculus/FDeriv/Norm.lean
index e2d0003e6a7904..f768fd12622ee4 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Norm.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Norm.lean
@@ -98,8 +98,7 @@ theorem HasStrictFDerivAt.hasStrictFDerivAt_norm_smul
   convert! h2.comp (t • x) h1 with y
   · rw [norm_smul, ← mul_assoc, norm_eq_abs, ← abs_mul, mul_inv_cancel₀ ht, abs_one, one_mul]
   ext y
-  simp only [coe_smul', Pi.smul_apply, smul_eq_mul, comp_smulₛₗ, map_inv₀, RingHom.id_apply,
-    comp_id]
+  simp only [smul_apply, smul_eq_mul, comp_smulₛₗ, map_inv₀, RingHom.id_apply, comp_id]
   rw [eq_inv_mul_iff_mul_eq₀ ht, ← mul_assoc, self_mul_sign]
 
 theorem HasStrictFDerivAt.hasStrictDerivAt_norm_smul_neg
@@ -123,8 +122,7 @@ theorem HasFDerivAt.hasFDerivAt_norm_smul
   · simp only [Function.comp_apply]
     rw [norm_smul, ← mul_assoc, norm_eq_abs, ← abs_mul, mul_inv_cancel₀ ht, abs_one, one_mul]
   · ext y
-    simp only [coe_smul', Pi.smul_apply, smul_eq_mul, comp_smulₛₗ, map_inv₀, RingHom.id_apply,
-      comp_id]
+    simp only [smul_apply, smul_eq_mul, comp_smulₛₗ, map_inv₀, RingHom.id_apply, comp_id]
     rw [eq_inv_mul_iff_mul_eq₀ ht, ← mul_assoc, self_mul_sign]
 
 theorem HasFDerivAt.hasFDerivAt_norm_smul_neg
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean b/Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
index 97ce608ae1fb7e..581c3531bff0ca 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
@@ -292,8 +292,7 @@ theorem Convex.taylor_approx_two_segment {v w : E} (hv : x + v ∈ interior s)
       ‖g' t‖ = ‖(f' (x + h • v + (t * h) • w) - f' x - f'' (h • v + (t * h) • w)) (h • w)‖ := by
         rw [hg']
         congrm ‖?_‖
-        simp only [ContinuousLinearMap.sub_apply, ContinuousLinearMap.add_apply,
-          ContinuousLinearMap.smul_apply, map_add, map_smul]
+        simp only [sub_apply, add_apply, smul_apply, map_add, map_smul]
         module
       _ ≤ ‖f' (x + h • v + (t * h) • w) - f' x - f'' (h • v + (t * h) • w)‖ * ‖h • w‖ :=
         (ContinuousLinearMap.le_opNorm _ _)
@@ -361,7 +360,7 @@ theorem Convex.isLittleO_alternate_sum_square {v w : E} (h4v : x + (4 : ℝ) •
   convert! TA1.sub TA2 using 1
   ext h
   simp only [two_smul, smul_add, ← add_assoc, map_add,
-    ContinuousLinearMap.add_apply]
+    add_apply]
   abel
 
 /-- Assume that `f` is differentiable inside a convex set `s`, and that its derivative `f'` is
@@ -424,16 +423,14 @@ theorem Convex.second_derivative_within_at_symmetric {s : Set E} (s_conv : Conve
     intro m
     have : f'' (z + t m • m) (z + t 0 • (0 : E)) = f'' (z + t 0 • (0 : E)) (z + t m • m) :=
       s_conv.second_derivative_within_at_symmetric_of_mem_interior hf xs hx (ts 0) (ts m)
-    simp only [map_add, map_smul, add_right_inj, ContinuousLinearMap.add_apply, Pi.smul_apply,
-      ContinuousLinearMap.coe_smul', add_zero, smul_zero] at this
+    simp only [map_add, map_smul, add_right_inj, add_apply, smul_apply, add_zero, smul_zero] at this
     exact smul_right_injective F (tpos m).ne' this
   -- applying `second_derivative_within_at_symmetric_of_mem_interior` to the vectors `z + (t v) v`
   -- and `z + (t w) w`, we deduce that `f'' v w = f'' w v`. Cross terms involving `z` can be
   -- eliminated thanks to the fact proved above that `f'' m z = f'' z m`.
   have : f'' (z + t v • v) (z + t w • w) = f'' (z + t w • w) (z + t v • v) :=
     s_conv.second_derivative_within_at_symmetric_of_mem_interior hf xs hx (ts w) (ts v)
-  simp only [map_add, map_smul, ContinuousLinearMap.add_apply, Pi.smul_apply,
-    ContinuousLinearMap.coe_smul', C] at this
+  simp only [map_add, map_smul, add_apply, smul_apply, C] at this
   have : (t v * t w) • (f'' v) w = (t v * t w) • (f'' w) v := by
     linear_combination (norm := module) this
   apply smul_right_injective F _ this
diff --git a/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean b/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
index 81585528d62260..487a58b2cdcfc9 100644
--- a/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
+++ b/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
@@ -415,7 +415,7 @@ lemma compContinuousLinearMap_zero [NontriviallyNormedField 𝕜]
     congr
     apply Subsingleton.allEq
   | succ =>
-    simp [ContinuousLinearMap.coe_zero']
+    simp [FunLike.coe_zero]
 
 end Const
 
diff --git a/Mathlib/Analysis/Calculus/Implicit.lean b/Mathlib/Analysis/Calculus/Implicit.lean
index dce376ac9d4997..c0f66598909a91 100644
--- a/Mathlib/Analysis/Calculus/Implicit.lean
+++ b/Mathlib/Analysis/Calculus/Implicit.lean
@@ -434,7 +434,7 @@ theorem to_implicitFunctionOfComplemented (hf : HasStrictFDerivAt f f' a) (hf' :
   swap
   · ext
     simp only [ContinuousLinearMap.comp_apply, Submodule.coe_subtypeL, Submodule.coe_subtype,
-      ContinuousLinearMap.apply_val_ker, ContinuousLinearMap.zero_apply]
+      ContinuousLinearMap.apply_val_ker, zero_apply]
   simp only [implicitFunctionDataOfComplemented, map_sub, sub_self]
 
 end Complemented
diff --git a/Mathlib/Analysis/Calculus/ImplicitFunction/ProdDomain.lean b/Mathlib/Analysis/Calculus/ImplicitFunction/ProdDomain.lean
index ccbfdb19584495..0ceeb71d831996 100644
--- a/Mathlib/Analysis/Calculus/ImplicitFunction/ProdDomain.lean
+++ b/Mathlib/Analysis/Calculus/ImplicitFunction/ProdDomain.lean
@@ -113,7 +113,7 @@ theorem hasStrictFDerivAt_implicitFunctionOfProdDomain
       (ContinuousLinearMap.fst_comp_prod _ _) this).snd
   ext
   rw [f'u.comp_apply, ← f'u.comp_inl_add_comp_inr]
-  simp [map_neg, if₂u]
+  simp [-ContinuousLinearMap.comp_apply, ContinuousLinearMap.coe_comp, map_neg, if₂u]
 
 theorem tendsto_implicitFunctionOfProdDomain
     (dfu : HasStrictFDerivAt f f'u u) (if₂u : (f'u ∘L .inr 𝕜 E₁ E₂).IsInvertible) :
diff --git a/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean b/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
index 2e008f60735e90..894bf7351a290e 100644
--- a/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
+++ b/Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
@@ -347,7 +347,7 @@ theorem hasFDerivAt_of_tendstoUniformlyOnFilter [NeBot l]
           (‖a.2 - x‖⁻¹ : 𝕜) • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
         fun a : ι × E => (‖a.2 - x‖⁻¹ : 𝕜) • (f' a.1 x - g' x) (a.2 - x) := by
     ext; simp only [Pi.add_apply]; rw [← smul_add, ← smul_add]; congr
-    simp only [map_sub, sub_add_sub_cancel, ContinuousLinearMap.coe_sub', Pi.sub_apply]
+    simp only [map_sub, sub_add_sub_cancel, FunLike.coe_sub, Pi.sub_apply]
     abel
   simp_rw [this]
   have : 𝓝 (0 : G) = 𝓝 (0 + 0 + 0) := by simp only [add_zero]
diff --git a/Mathlib/Analysis/Calculus/VectorField.lean b/Mathlib/Analysis/Calculus/VectorField.lean
index be9e933bd82f80..59828087fde36f 100644
--- a/Mathlib/Analysis/Calculus/VectorField.lean
+++ b/Mathlib/Analysis/Calculus/VectorField.lean
@@ -169,14 +169,14 @@ lemma lieBracketWithin_add_left (hV : DifferentiableWithinAt 𝕜 V s x)
     lieBracketWithin 𝕜 (V + V₁) W s x =
       lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V₁ W s x := by
   simp only [lieBracketWithin, Pi.add_apply, map_add]
-  rw [fderivWithin_add hs hV hV₁, ContinuousLinearMap.add_apply]
+  rw [fderivWithin_add hs hV hV₁, add_apply]
   abel
 
 lemma lieBracket_add_left (hV : DifferentiableAt 𝕜 V x) (hV₁ : DifferentiableAt 𝕜 V₁ x) :
     lieBracket 𝕜 (V + V₁) W x =
       lieBracket 𝕜 V W x + lieBracket 𝕜 V₁ W x := by
   simp only [lieBracket, Pi.add_apply, map_add]
-  rw [fderiv_add hV hV₁, ContinuousLinearMap.add_apply]
+  rw [fderiv_add hV hV₁, add_apply]
   abel
 
 /-- We have `[0, W] = 0` for all vector fields `W`: this depends on the junk value 0
@@ -204,14 +204,14 @@ lemma lieBracketWithin_add_right (hW : DifferentiableWithinAt 𝕜 W s x)
     lieBracketWithin 𝕜 V (W + W₁) s x =
       lieBracketWithin 𝕜 V W s x + lieBracketWithin 𝕜 V W₁ s x := by
   simp only [lieBracketWithin, Pi.add_apply, map_add]
-  rw [fderivWithin_add hs hW hW₁, ContinuousLinearMap.add_apply]
+  rw [fderivWithin_add hs hW hW₁, add_apply]
   abel
 
 lemma lieBracket_add_right (hW : DifferentiableAt 𝕜 W x) (hW₁ : DifferentiableAt 𝕜 W₁ x) :
     lieBracket 𝕜 V (W + W₁) x =
       lieBracket 𝕜 V W x + lieBracket 𝕜 V W₁ x := by
   simp only [lieBracket, Pi.add_apply, map_add]
-  rw [fderiv_add hW hW₁, ContinuousLinearMap.add_apply]
+  rw [fderiv_add hW hW₁, add_apply]
   abel
 
 /-- The differentiation operator along `[W, V]`
@@ -434,9 +434,8 @@ lemma leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt
   rw [fderivWithin_fun_sub (hs x hx) (aux₁ hU hV) (aux₁ hV hU)]
   rw [fderivWithin_fun_sub (hs x hx) (aux₁ hU hW) (aux₁ hW hU)]
   rw [aux₂ hW hV, aux₂ hV hW, aux₂ hV hU, aux₂ hU hV, aux₂ hW hU, aux₂ hU hW]
-  simp only [ContinuousLinearMap.coe_sub', Pi.sub_apply, ContinuousLinearMap.add_apply,
-    ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.flip_apply, h'V.eq,
-    h'U.eq, h'W.eq]
+  simp only [FunLike.coe_sub, Pi.sub_apply, add_apply, ContinuousLinearMap.comp_apply,
+    ContinuousLinearMap.flip_apply, h'V.eq, h'U.eq, h'W.eq]
   abel
 
 /-- The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity
diff --git a/Mathlib/Analysis/Complex/CauchyIntegral.lean b/Mathlib/Analysis/Complex/CauchyIntegral.lean
index 91ecc61b3126d4..02615453ba3763 100644
--- a/Mathlib/Analysis/Complex/CauchyIntegral.lean
+++ b/Mathlib/Analysis/Complex/CauchyIntegral.lean
@@ -201,9 +201,8 @@ theorem integral_boundary_rect_of_hasFDerivAt_real_off_countable (f : ℂ → E)
   set F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p => (f' (e p)).comp (e : ℝ × ℝ →L[ℝ] ℂ)
   have hF' : ∀ p : ℝ × ℝ, (-(I • F' p)) (1, 0) + F' p (0, 1) = -(I • f' (e p) 1 - f' (e p) I) := by
     rintro ⟨x, y⟩
-    simp only [F', ContinuousLinearMap.neg_apply, ContinuousLinearMap.smul_apply,
-      ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe, he₁, he₂, neg_add_eq_sub,
-      neg_sub]
+    simp only [F', neg_apply, smul_apply, ContinuousLinearMap.comp_apply,
+      ContinuousLinearEquiv.coe_coe, he₁, he₂, neg_add_eq_sub, neg_sub]
   set R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
   set t : Set (ℝ × ℝ) := e ⁻¹' s
   rw [uIcc_comm z.im] at Hc Hi; rw [min_comm z.im, max_comm z.im] at Hd
diff --git a/Mathlib/Analysis/Complex/Conformal.lean b/Mathlib/Analysis/Complex/Conformal.lean
index 17170b77922f4a..564f08a7f985ce 100644
--- a/Mathlib/Analysis/Complex/Conformal.lean
+++ b/Mathlib/Analysis/Complex/Conformal.lean
@@ -125,8 +125,8 @@ theorem isConformalMap_iff_is_complex_or_conj_linear :
       simp only [w, restrictScalars_zero]
     · have minor₁ : g = map.restrictScalars ℝ ∘L ↑conjCLE := by
         ext1
-        simp only [hmap, coe_comp', ContinuousLinearEquiv.coe_coe, Function.comp_apply,
-          conjCLE_apply, starRingEnd_self_apply]
+        simp only [hmap, ContinuousLinearEquiv.coe_coe, comp_apply, conjCLE_apply,
+          starRingEnd_self_apply]
       rw [minor₁] at h₂ ⊢
       refine isConformalMap_complex_linear_conj ?_
       contrapose h₂ with w
diff --git a/Mathlib/Analysis/Complex/Harmonic/Analytic.lean b/Mathlib/Analysis/Complex/Harmonic/Analytic.lean
index 1f3c33700dff6e..d7bf86de72edee 100644
--- a/Mathlib/Analysis/Complex/Harmonic/Analytic.lean
+++ b/Mathlib/Analysis/Complex/Harmonic/Analytic.lean
@@ -38,9 +38,8 @@ theorem HarmonicAt.differentiableAt_complex_partial (hf : HarmonicAt f x) :
   refine differentiableAt_complex_iff_differentiableAt_real.2 ⟨by fun_prop, ?_⟩
   rw [fderiv_sub (by fun_prop) (by fun_prop), fderiv_const_smul (by fun_prop)]
   repeat rw [fderiv_comp]; all_goals try fun_prop
-  simp only [ContinuousLinearMap.fderiv, ContinuousLinearMap.coe_sub',
-    ContinuousLinearMap.coe_comp', ContinuousLinearMap.coe_smul', Pi.sub_apply,
-    Function.comp_apply, ofRealCLM_apply, Pi.smul_apply, smul_eq_mul, mul_sub]
+  simp only [ContinuousLinearMap.fderiv, sub_apply, ContinuousLinearMap.comp_apply, ofRealCLM_apply,
+    smul_apply, smul_eq_mul]
   ring_nf
   rw [fderiv_clm_apply (by fun_prop) (by fun_prop), fderiv_clm_apply (by fun_prop) (by fun_prop)]
   simp only [fderiv_fun_const, Pi.zero_apply, ContinuousLinearMap.comp_zero, zero_add,
diff --git a/Mathlib/Analysis/Convex/Birkhoff.lean b/Mathlib/Analysis/Convex/Birkhoff.lean
index 2083948fd5b2da..52c52d26adf950 100644
--- a/Mathlib/Analysis/Convex/Birkhoff.lean
+++ b/Mathlib/Analysis/Convex/Birkhoff.lean
@@ -113,8 +113,8 @@ private lemma doublyStochastic_sum_perm_aux (M : Matrix n n R)
     exact single_le_sum (fun j _ => hM.1 i j) (by simp)
   have : ∃ M' ∈ doublyStochastic R n, N = s' • M' := by
     rw [exists_mem_doublyStochastic_eq_smul_iff hs']
-    simp only [sub_apply, smul_apply, PEquiv.toMatrix_apply, Equiv.toPEquiv_apply, Option.mem_def,
-      Option.some.injEq, smul_eq_mul, mul_ite, mul_one, mul_zero, sub_nonneg,
+    simp only [Matrix.sub_apply, Matrix.smul_apply, PEquiv.toMatrix_apply, Equiv.toPEquiv_apply,
+      Option.mem_def, Option.some.injEq, smul_eq_mul, mul_ite, mul_one, mul_zero, sub_nonneg,
       sum_sub_distrib, sum_ite_eq, mem_univ, ↓reduceIte, N]
     refine ⟨fun i' j => ?_, by simp [s', hM.2.1], by simp [s', ← σ.eq_symm_apply, hM]⟩
     split
diff --git a/Mathlib/Analysis/Convex/DoublyStochasticMatrix.lean b/Mathlib/Analysis/Convex/DoublyStochasticMatrix.lean
index b072ee11c4c878..5401ae19c71739 100644
--- a/Mathlib/Analysis/Convex/DoublyStochasticMatrix.lean
+++ b/Mathlib/Analysis/Convex/DoublyStochasticMatrix.lean
@@ -153,7 +153,7 @@ lemma exists_mem_doublyStochastic_eq_smul_iff {M : Matrix n n R} {s : R} (hs : 0
   case mp =>
     rintro ⟨M', hM', rfl⟩
     rw [mem_doublyStochastic_iff_sum] at hM'
-    simp only [smul_apply, smul_eq_mul, ← mul_sum]
+    simp only [Matrix.smul_apply, smul_eq_mul, ← mul_sum]
     exact ⟨fun i j => mul_nonneg hs (hM'.1 _ _), by simp [hM']⟩
   rcases eq_or_lt_of_le hs with rfl | hs
   case inl =>
diff --git a/Mathlib/Analysis/Convex/Exposed.lean b/Mathlib/Analysis/Convex/Exposed.lean
index cd3e115303c64f..e5ed0d20521fc7 100644
--- a/Mathlib/Analysis/Convex/Exposed.lean
+++ b/Mathlib/Analysis/Convex/Exposed.lean
@@ -117,7 +117,7 @@ theorem eq_inter_halfSpace [IsOrderedRing 𝕜] [Nontrivial 𝕜] {A B : Set E}
   · refine ⟨0, 1, ?_⟩
     rw [eq_comm, eq_empty_iff_forall_notMem]
     rintro x ⟨-, h⟩
-    rw [ContinuousLinearMap.zero_apply] at h
+    rw [zero_apply] at h
     have : ¬(1 : 𝕜) ≤ 0 := not_le_of_gt zero_lt_one
     contradiction
   exact hAB.eq_inter_halfSpace' hB
diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean
index e11a45fc803e23..b35fb5ee876b75 100644
--- a/Mathlib/Analysis/Convolution.lean
+++ b/Mathlib/Analysis/Convolution.lean
@@ -961,7 +961,7 @@ theorem posConvolution_eq_convolution_indicator (f : ℝ → E) (g : ℝ → E')
         exacts [Or.inr (Or.inl ⟨h, h'⟩), Or.inr (Or.inr h')]
     rcases this with (ht | ht | ht)
     · rw [indicator_of_notMem (notMem_Ioo_of_le ht), indicator_of_notMem (notMem_Ioi.mpr ht),
-        map_zero, ContinuousLinearMap.zero_apply]
+        map_zero, zero_apply]
     · rw [indicator_of_mem ht, indicator_of_mem (mem_Ioi.mpr ht.1),
           indicator_of_mem (mem_Ioi.mpr <| sub_pos.mpr ht.2)]
     · rw [indicator_of_notMem (notMem_Ioo_of_ge ht),
@@ -971,7 +971,7 @@ theorem posConvolution_eq_convolution_indicator (f : ℝ → E) (g : ℝ → E')
     · rw [indicator_of_notMem (_ : x - t ∉ Ioi 0), map_zero]
       rw [notMem_Ioi] at h ⊢
       exact sub_nonpos.mpr (h.trans ht.le)
-    · rw [indicator_of_notMem (mem_Ioi.not.mpr ht), map_zero, ContinuousLinearMap.zero_apply]
+    · rw [indicator_of_notMem (mem_Ioi.not.mpr ht), map_zero, zero_apply]
 
 theorem integrable_posConvolution {f : ℝ → E} {g : ℝ → E'} {μ ν : Measure ℝ} [SFinite μ]
     [SFinite ν] [IsAddRightInvariant μ] [NoAtoms ν] (hf : IntegrableOn f (Ioi 0) ν)
diff --git a/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean b/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean
index 09677e60a5f7e0..d46a03d077e0d9 100644
--- a/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean
+++ b/Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean
@@ -919,13 +919,12 @@ noncomputable def integralAgainstBilinLM (B : F₁ →L[𝕜] F₂ →L[𝕜] F
     if IntegrableOn φ K μ then ∫ x, B (f x) (φ x) ∂μ else 0
   map_add' f g := by
     split_ifs with hφ
-    · simp_rw [coe_add, Pi.add_apply, map_add, ContinuousLinearMap.add_apply,
+    · simp_rw [coe_add, Pi.add_apply, map_add, add_apply,
         integral_add (f.integrable_bilin B hφ) (g.integrable_bilin B hφ)]
     · simp
   map_smul' c f := by
     split_ifs with hφ
-    · simp_rw [coe_smul, Pi.smul_apply, map_smul, ContinuousLinearMap.smul_apply,
-        integral_smul c, RingHom.id_apply]
+    · simp_rw [coe_smul, Pi.smul_apply, map_smul, smul_apply, integral_smul c, RingHom.id_apply]
     · simp
 
 @[simp]
@@ -945,7 +944,7 @@ lemma integralAgainstBilinLM_eq_setIntegral {B : F₁ →L[𝕜] F₂ →L[𝕜]
     integralAgainstBilinLM B μ φ f = ∫ x in K, B (f x) (φ x) ∂μ := by
   rw [integralAgainstBilinLM_eq_integral hφ, setIntegral_eq_integral_of_forall_compl_eq_zero]
   intro x hx
-  rw [f.zero_on_compl hx, Pi.zero_apply, map_zero, ContinuousLinearMap.zero_apply]
+  rw [f.zero_on_compl hx, Pi.zero_apply, map_zero, zero_apply]
 
 lemma norm_integralAgainstBilinLM_le {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} {μ : Measure E} {φ : E → F₂}
     {f : 𝓓^{n}_{K}(E, F₁)} :
diff --git a/Mathlib/Analysis/Distribution/FourierMultiplier.lean b/Mathlib/Analysis/Distribution/FourierMultiplier.lean
index 0a93b29d8b06d7..3ea0629964633c 100644
--- a/Mathlib/Analysis/Distribution/FourierMultiplier.lean
+++ b/Mathlib/Analysis/Distribution/FourierMultiplier.lean
@@ -111,7 +111,7 @@ theorem laplacian_eq_fourierMultiplierCLM (f : 𝓢(E, F)) :
   have : ∀ i (hi : i ∈ Finset.univ), (inner ℝ · (b i) ^ 2).HasTemperateGrowth := by
     fun_prop
   simp_rw [laplacian_eq_sum b, ← b.sum_sq_inner_left, fourierMultiplierCLM_sum F this,
-    ContinuousLinearMap.coe_sum', Finset.sum_apply, Finset.smul_sum]
+    _root_.sum_apply, Finset.smul_sum]
   congr 1
   ext i x
   simp_rw [smul_apply, lineDeriv_eq_fourierMultiplierCLM]
@@ -213,8 +213,7 @@ theorem laplacian_eq_fourierMultiplierCLM (f : 𝓢'(E, F)) :
       (fun x ↦ Complex.ofReal (inner ℝ x (b i)) ^ 2).HasTemperateGrowth := by
     fun_prop
   simp_rw [laplacian_eq_sum b, ← b.sum_sq_inner_left, Complex.ofReal_sum, Complex.ofReal_pow,
-    fourierMultiplierCLM_sum F this, ContinuousLinearMap.coe_sum', Finset.sum_apply,
-    Finset.smul_sum]
+    fourierMultiplierCLM_sum F this, sum_apply, Finset.smul_sum]
   congr 1
   ext i x
   simp_rw [lineDeriv_eq_fourierMultiplierCLM, map_smul, smul_smul]
diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace/Deriv.lean b/Mathlib/Analysis/Distribution/SchwartzSpace/Deriv.lean
index f39cfa1c5e6e4a..3b24d3f773f237 100644
--- a/Mathlib/Analysis/Distribution/SchwartzSpace/Deriv.lean
+++ b/Mathlib/Analysis/Distribution/SchwartzSpace/Deriv.lean
@@ -347,7 +347,7 @@ theorem integral_bilinear_laplacian_right_eq_left (f : 𝓢(E, F₁)) (g : 𝓢(
     (L : F₁ →L[ℝ] F₂ →L[ℝ] F₃) :
     ∫ x, L (f x) (Δ g x) ∂μ = ∫ x, L (Δ f x) (g x) ∂μ := by
   simp_rw [laplacian_eq_sum (stdOrthonormalBasis ℝ E), sum_apply, map_sum,
-    ContinuousLinearMap.coe_sum', Finset.sum_apply]
+    _root_.sum_apply]
   rw [MeasureTheory.integral_finsetSum, MeasureTheory.integral_finsetSum]
   · simp [integral_bilinear_lineDerivOp_right_eq_neg_left]
   · exact fun _ _ ↦ (pairing L (∂_{_} <| ∂_{_} f) g).integrable
diff --git a/Mathlib/Analysis/Fourier/FourierTransform.lean b/Mathlib/Analysis/Fourier/FourierTransform.lean
index 5b68556816ea00..7023f5af93e170 100644
--- a/Mathlib/Analysis/Fourier/FourierTransform.lean
+++ b/Mathlib/Analysis/Fourier/FourierTransform.lean
@@ -231,7 +231,7 @@ theorem integral_bilin_fourierIntegral_eq_flip
     integral_fourierIntegral_swap M.flip he hL hf hg
   _ = ∫ x, (∫ ξ, M (f x) (e (-L.flip ξ x) • g ξ) ∂ν) ∂μ := by
     simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.map_smul_of_tower,
-      ContinuousLinearMap.coe_smul', Pi.smul_apply, LinearMap.flip_apply]
+      smul_apply, LinearMap.flip_apply]
   _ = ∫ x, M (f x) (∫ ξ, e (-L.flip ξ x) • g ξ ∂ν) ∂μ := by
     congr with x
     apply ContinuousLinearMap.integral_comp_comm
diff --git a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
index 62ac120d267631..69ce46ebc9901f 100644
--- a/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
+++ b/Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
@@ -118,16 +118,15 @@ lemma hasFDerivAt_fourierChar_neg_bilinear_right (v : V) (w : W) :
   have ha : HasFDerivAt (fun w' : W ↦ L v w') (L v) w := ContinuousLinearMap.hasFDerivAt (L v)
   convert! (hasDerivAt_fourierChar (-L v w)).hasFDerivAt.comp w ha.neg using 1
   ext y
-  simp only [neg_mul, ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_comp', Pi.smul_apply,
-    Function.comp_apply, ofRealCLM_apply, smul_eq_mul, ContinuousLinearMap.comp_neg,
-    ContinuousLinearMap.neg_apply, ContinuousLinearMap.toSpanSingleton_apply, real_smul, neg_inj]
+  simp only [neg_mul, neg_smul, neg_apply, smul_apply, ContinuousLinearMap.comp_apply,
+    ofRealCLM_apply, smul_eq_mul, ContinuousLinearMap.comp_neg,
+    ContinuousLinearMap.toSpanSingleton_apply, real_smul, neg_inj]
   ring
 
 lemma fderiv_fourierChar_neg_bilinear_right_apply (v : V) (w y : W) :
     fderiv ℝ (fun w ↦ (𝐞 (-L v w) : ℂ)) w y = -2 * π * I * L v y * 𝐞 (-L v w) := by
-  simp only [(hasFDerivAt_fourierChar_neg_bilinear_right L v w).fderiv, neg_mul,
-    ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_comp', Pi.smul_apply,
-    Function.comp_apply, ofRealCLM_apply, smul_eq_mul, neg_inj]
+  simp only [(hasFDerivAt_fourierChar_neg_bilinear_right L v w).fderiv, neg_mul, neg_smul,
+    neg_apply, smul_apply, ContinuousLinearMap.comp_apply, ofRealCLM_apply, smul_eq_mul, neg_inj]
   ring
 
 lemma differentiable_fourierChar_neg_bilinear_right (v : V) :
@@ -141,9 +140,9 @@ lemma hasFDerivAt_fourierChar_neg_bilinear_left (v : V) (w : W) :
 
 lemma fderiv_fourierChar_neg_bilinear_left_apply (v y : V) (w : W) :
     fderiv ℝ (fun v ↦ (𝐞 (-L v w) : ℂ)) v y = -2 * π * I * L y w * 𝐞 (-L v w) := by
-  simp only [(hasFDerivAt_fourierChar_neg_bilinear_left L v w).fderiv, neg_mul,
-    ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_comp', Pi.smul_apply,
-    Function.comp_apply, ContinuousLinearMap.flip_apply, ofRealCLM_apply, smul_eq_mul, neg_inj]
+  simp only [(hasFDerivAt_fourierChar_neg_bilinear_left L v w).fderiv, neg_mul, neg_smul, neg_apply,
+    smul_apply, ContinuousLinearMap.comp_apply, ContinuousLinearMap.flip_apply, ofRealCLM_apply,
+    smul_eq_mul, neg_inj]
   ring
 
 lemma differentiable_fourierChar_neg_bilinear_left (w : W) :
@@ -174,8 +173,8 @@ lemma hasFDerivAt_fourierChar_smul (v : V) (w : W) :
   have ha : HasFDerivAt (fun w' : W ↦ L v w') (L v) w := ContinuousLinearMap.hasFDerivAt (L v)
   convert! ((hasDerivAt_fourierChar (-L v w)).hasFDerivAt.comp w ha.neg).smul_const (f v)
   ext w' : 1
-  simp_rw [fourierSMulRight, ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply]
-  rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.neg_apply,
+  simp_rw [fourierSMulRight, smul_apply, ContinuousLinearMap.smulRight_apply]
+  rw [ContinuousLinearMap.comp_apply, neg_apply,
     ContinuousLinearMap.toSpanSingleton_apply, ← smul_assoc, smul_comm,
     ← smul_assoc, real_smul, real_smul, Submonoid.smul_def, smul_eq_mul]
   push_cast
@@ -265,7 +264,7 @@ theorem fourierIntegral_fderiv [MeasurableSpace V] [BorelSpace V] [FiniteDimensi
   suffices ∫ x, g x • fderiv ℝ f x y ∂μ = ∫ x, (2 * ↑π * I * L y w * g x) • f x ∂μ by
     rw [fourierIntegral_continuousLinearMap_apply' hf']
     simpa only [fourierIntegral, ContinuousLinearMap.toLinearMap₁₂_apply, fourierSMulRight_apply,
-      ContinuousLinearMap.neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul,
+      neg_apply, ContinuousLinearMap.flip_apply, ← integral_smul, neg_smul,
       smul_neg, ← smul_smul, coe_smul, neg_neg]
   -- Key step: integrate by parts with respect to `y` to switch the derivative from `f` to `g`.
   have A x : fderiv ℝ g x y = - 2 * ↑π * I * L y w * g x :=
@@ -487,7 +486,8 @@ lemma hasFTaylorSeriesUpTo_fourierIntegral {N : ℕ∞ω}
         fourierIntegral_continuousMultilinearMap_apply' (I₄.apply_continuousLinearMap _)]
       congr with v
       simp only [fourierPowSMulRight_apply, mul_comm, pow_succ, neg_mul, Fin.prod_univ_succ,
-        Fin.cons_zero, Fin.cons_succ, neg_smul, fourierSMulRight_apply, neg_apply, smul_apply,
+        Fin.cons_zero, Fin.cons_succ, neg_smul, fourierSMulRight_apply,
+        ContinuousMultilinearMap.neg_apply, ContinuousMultilinearMap.smul_apply,
         smul_comm (M := ℝ) (N := ℂ) (α := E), smul_smul]
     exact E ▸ hasFDerivAt_fourierIntegral L I₁ I₂ w
   · intro n hn
@@ -539,7 +539,7 @@ theorem fourierIntegral_iteratedFDeriv [FiniteDimensional ℝ V]
   | zero =>
     ext w m
     simp only [iteratedFDeriv_zero_apply, fourierPowSMulRight_apply, pow_zero,
-      Finset.univ_eq_empty, ContinuousLinearMap.neg_apply, ContinuousLinearMap.flip_apply,
+      Finset.univ_eq_empty, _root_.neg_apply, ContinuousLinearMap.flip_apply,
       Finset.prod_empty, one_smul, fourierIntegral_continuousMultilinearMap_apply' ((h'f 0 bot_le))]
   | succ n ih =>
     ext w m
@@ -553,16 +553,17 @@ theorem fourierIntegral_iteratedFDeriv [FiniteDimensional ℝ V]
         (-(2 * π * I)) ^ (n + 1) • (∏ x : Fin (n + 1), -L (m x) w) • ∫ v, 𝐞 (-L v w) • f v ∂μ by
       rw [fourierIntegral_continuousMultilinearMap_apply' (h'f _ hn)]
       simp only [iteratedFDeriv_succ_apply_left, fourierPowSMulRight_apply,
-        ContinuousLinearMap.neg_apply, ContinuousLinearMap.flip_apply]
+        _root_.neg_apply, ContinuousLinearMap.flip_apply]
       rw [← fourierIntegral_continuousMultilinearMap_apply' ((J.apply_continuousLinearMap _)),
           ← fourierIntegral_continuousLinearMap_apply' J]
       exact H
     have h'n : n < N := (Nat.cast_lt.mpr n.lt_succ_self).trans_le hn
     rw [fourierIntegral_fderiv _ (h'f n h'n.le)
       (hf.differentiable_iteratedFDeriv (mod_cast h'n)) J]
-    simp only [ih h'n.le, fourierSMulRight_apply, ContinuousLinearMap.neg_apply,
-      ContinuousLinearMap.flip_apply, neg_smul, smul_neg, neg_neg, smul_apply,
-      fourierPowSMulRight_apply, ← coe_smul (E := E), smul_smul]
+    simp only [ih h'n.le, fourierSMulRight_apply, _root_.neg_apply,
+      ContinuousLinearMap.flip_apply, neg_smul, smul_neg, neg_neg,
+      ContinuousMultilinearMap.smul_apply, fourierPowSMulRight_apply,
+      ← coe_smul (E := E), smul_smul]
     congr 1
     simp only [ofReal_prod, ofReal_neg, pow_succ, mul_neg, Fin.prod_univ_succ, neg_mul,
       ofReal_mul, neg_neg, Fin.tail_def]
@@ -802,7 +803,7 @@ lemma hasDerivAt_fourier
   convert! (VectorFourier.hasFDerivAt_fourierIntegral L hf hf'' w).hasDerivAt using 1
   rw [fourierIntegral_continuousLinearMap_apply' h_int, VectorFourier.fourierIntegral,
     fourier_real_eq]
-  simp [fourierSMulRight, L, ContinuousLinearMap.smul_apply,
+  simp [fourierSMulRight, L, smul_apply,
     ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.mul_apply', ← neg_mul, mul_smul]
 
 @[deprecated (since := "2025-11-16")]
@@ -830,7 +831,7 @@ theorem fourier_deriv
   have : 𝓕 (deriv f) x = 𝓕 (fderiv ℝ f) x 1 := by
     simp only [fourier_continuousLinearMap_apply I, fderiv_apply_one_eq_deriv]
   rw [this, fourier_fderiv hf h'f I]
-  simp only [fourierSMulRight_apply, ContinuousLinearMap.neg_apply, innerSL_apply_apply, smul_smul,
+  simp only [fourierSMulRight_apply, neg_apply, innerSL_apply_apply ℝ, smul_smul,
     RCLike.inner_apply', conj_trivial, mul_one, neg_smul, smul_neg, neg_neg, neg_mul, ← coe_smul]
 
 @[deprecated (since := "2025-11-16")]
@@ -868,7 +869,7 @@ theorem fourier_iteratedDeriv {f : ℝ → E} {N : ℕ∞} {n : ℕ} (hf : ContD
   change 𝓕 (fun x ↦ iteratedDeriv n f x) x = _
   simp_rw [iteratedDeriv, ← fourier_continuousMultilinearMap_apply (A n hn),
     fourier_iteratedFDeriv hf A hn]
-  simp [← coe_smul, smul_smul, ← mul_pow]
+  simp [← coe_smul, smul_smul, ← mul_pow, innerSL_apply_apply ℝ]
 
 @[deprecated (since := "2025-11-16")]
 alias fourierIntegral_iteratedDeriv := fourier_iteratedDeriv
diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
index 48532c4c9e788e..ea679bd5b0edb9 100644
--- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
@@ -83,8 +83,7 @@ theorem adjointAux_apply (A : E →L[𝕜] F) (x : F) :
   rfl
 
 theorem adjointAux_inner_left (A : E →L[𝕜] F) (x : E) (y : F) : ⟪adjointAux A y, x⟫ = ⟪y, A x⟫ := by
-  rw [adjointAux_apply, toDual_symm_apply, toSesqForm_apply_coe, coe_comp', coe_innerSL_apply,
-    Function.comp_apply]
+  simp
 
 theorem adjointAux_inner_right (A : E →L[𝕜] F) (x : E) (y : F) :
     ⟪x, adjointAux A y⟫ = ⟪A x, y⟫ := by
@@ -139,7 +138,7 @@ in reverse order. -/
 theorem adjoint_comp (A : F →L[𝕜] G) (B : E →L[𝕜] F) : (A ∘L B)† = B† ∘L A† := by
   ext v
   refine ext_inner_left 𝕜 fun w => ?_
-  simp only [adjoint_inner_right, ContinuousLinearMap.coe_comp', Function.comp_apply]
+  simp [adjoint_inner_right]
 
 theorem apply_norm_sq_eq_inner_adjoint_left (A : E →L[𝕜] F) (x : E) :
     ‖A x‖ ^ 2 = re ⟪(A† ∘L A) x, x⟫ := by
@@ -224,7 +223,7 @@ You may need to rewrite with `ContinuousLinearMap.coe_comp'` before applying thi
 -/
 lemma adjoint_comp_self_injective_iff (T : E →L[𝕜] F) :
     Function.Injective (T† ∘ T) ↔ Function.Injective T := by
-  rw [← coe_comp', ← coe_coe, ← LinearMap.ker_eq_bot, ← coe_coe, ← LinearMap.ker_eq_bot,
+  rw [← coe_comp, ← coe_coe, ← LinearMap.ker_eq_bot, ← coe_coe, ← LinearMap.ker_eq_bot,
     ker_adjoint_comp_self]
 
 /--
@@ -390,11 +389,12 @@ variable {T : E →L[𝕜] E} [CompleteSpace E]
 theorem isStarNormal_iff_norm_eq_adjoint :
     IsStarNormal T ↔ ∀ v : E, ‖T v‖ = ‖adjoint T v‖ := by
   rw [isStarNormal_iff, Commute, SemiconjBy, ← sub_eq_zero]
-  simp_rw [ContinuousLinearMap.ext_iff, ← coe_coe, coe_sub, ← LinearMap.ext_iff, coe_zero]
-  have := star_eq_adjoint T ▸ coe_sub (star _ * T) _ ▸
+  simp_rw [ContinuousLinearMap.ext_iff, ← coe_coe, toLinearMap_sub, ← LinearMap.ext_iff,
+    toLinearMap_zero]
+  have := star_eq_adjoint T ▸ toLinearMap_sub (star _ * T) _ ▸
     ((IsSelfAdjoint.star_mul_self T).sub (IsSelfAdjoint.mul_star_self T)).isSymmetric
   simp_rw [star_eq_adjoint, ← LinearMap.IsSymmetric.inner_map_self_eq_zero this,
-    LinearMap.sub_apply, inner_sub_left, coe_coe, mul_apply, adjoint_inner_left,
+    LinearMap.sub_apply, inner_sub_left, coe_coe, mul_apply_eq_comp, adjoint_inner_left,
     inner_self_eq_norm_sq_to_K, ← adjoint_inner_right T, inner_self_eq_norm_sq_to_K,
     sub_eq_zero, ← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)]
   norm_cast
@@ -445,7 +445,7 @@ theorem isStarProjection_iff_isIdempotentElem_and_isStarNormal :
 theorem isStarProjection_iff_isSymmetricProjection :
     IsStarProjection T ↔ T.IsSymmetricProjection := by
   simp [isStarProjection_iff, LinearMap.isSymmetricProjection_iff,
-    isSelfAdjoint_iff_isSymmetric, IsIdempotentElem, End.mul_eq_comp, ← coe_comp, mul_def]
+    isSelfAdjoint_iff_isSymmetric, IsIdempotentElem, End.mul_eq_comp, ← toLinearMap_comp, mul_def]
 
 alias ⟨IsStarProjection.isSymmetricProjection, LinearMap.IsSymmetricProjection.isStarProjection⟩ :=
   isStarProjection_iff_isSymmetricProjection
diff --git a/Mathlib/Analysis/InnerProductSpace/ConformalLinearMap.lean b/Mathlib/Analysis/InnerProductSpace/ConformalLinearMap.lean
index 3c9948e75a7c42..4063c25096ba1c 100644
--- a/Mathlib/Analysis/InnerProductSpace/ConformalLinearMap.lean
+++ b/Mathlib/Analysis/InnerProductSpace/ConformalLinearMap.lean
@@ -33,8 +33,8 @@ theorem isConformalMap_iff (f : E →L[ℝ] F) :
   constructor
   · rintro ⟨c₁, hc₁, li, rfl⟩
     refine ⟨c₁ * c₁, mul_self_pos.2 hc₁, fun u v => ?_⟩
-    simp only [real_inner_smul_left, real_inner_smul_right, mul_assoc, coe_smul',
-      coe_toContinuousLinearMap, Pi.smul_apply, inner_map_map]
+    simp only [real_inner_smul_left, real_inner_smul_right, mul_assoc,
+      coe_toContinuousLinearMap, smul_apply, inner_map_map]
   · rintro ⟨c₁, hc₁, huv⟩
     obtain ⟨c, hc, rfl⟩ : ∃ c : ℝ, 0 < c ∧ c₁ = c * c :=
       ⟨√c₁, Real.sqrt_pos.2 hc₁, (Real.mul_self_sqrt hc₁.le).symm⟩
diff --git a/Mathlib/Analysis/InnerProductSpace/Dual.lean b/Mathlib/Analysis/InnerProductSpace/Dual.lean
index 1b5d9ae1b582e4..03916c4cfa434e 100644
--- a/Mathlib/Analysis/InnerProductSpace/Dual.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Dual.lean
@@ -140,9 +140,7 @@ def toDual : E ≃ₗᵢ⋆[𝕜] StrongDual 𝕜 E :=
       by_cases htriv : Y = ⊤
       · have hℓ : ℓ = 0 := by
           have h' := LinearMap.ker_eq_top.mp htriv
-          rw [← coe_zero] at h'
-          apply coe_injective
-          exact h'
+          norm_cast at h'
         exact ⟨0, by simp [hℓ]⟩
       · rw [← Submodule.orthogonal_eq_bot_iff] at htriv
         change Yᗮ ≠ ⊥ at htriv
@@ -204,8 +202,7 @@ theorem continuousLinearMapOfBilin_zero : (0 : E →L⋆[𝕜] E →L[𝕜] 𝕜
 
 @[simp]
 theorem continuousLinearMapOfBilin_apply (v w : E) : ⟪B♯ v, w⟫ = B v w := by
-  rw [continuousLinearMapOfBilin, coe_comp', ContinuousLinearEquiv.coe_coe,
-    LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, toDual_symm_apply]
+  simp [continuousLinearMapOfBilin]
 
 theorem unique_continuousLinearMapOfBilin {v f : E} (is_lax_milgram : ∀ w, ⟪f, w⟫ = B v w) :
     f = B♯ v := by
diff --git a/Mathlib/Analysis/InnerProductSpace/LinearMap.lean b/Mathlib/Analysis/InnerProductSpace/LinearMap.lean
index 1ef51e0d746376..79f8dfa984ef81 100644
--- a/Mathlib/Analysis/InnerProductSpace/LinearMap.lean
+++ b/Mathlib/Analysis/InnerProductSpace/LinearMap.lean
@@ -334,7 +334,8 @@ theorem isIdempotentElem_rankOne_self {x : F} (hx : ‖x‖ = 1) :
 @[simp] theorem rankOne_one_left_eq_innerSL (x : F) : rankOne 𝕜 1 x = innerSL 𝕜 x := by ext; simp
 
 lemma rankOne_comp_rankOne (x : E) (y z : F) (w : G) :
-    rankOne 𝕜 x y ∘L rankOne 𝕜 z w = inner 𝕜 y z • rankOne 𝕜 x w := by simp [comp_rankOne]
+    rankOne 𝕜 x y ∘L rankOne 𝕜 z w = inner 𝕜 y z • rankOne 𝕜 x w := by
+  simp [comp_rankOne]
 
 lemma inner_left_rankOne_apply (x : F) (y z : G) (w : F) :
     inner 𝕜 (rankOne 𝕜 x y z) w = inner 𝕜 z y * inner 𝕜 x w := by
@@ -359,7 +360,7 @@ theorem isIdempotentElem_rankOne_self_iff {x : F} (hx : x ≠ 0) :
     IsIdempotentElem (rankOne 𝕜 x x) ↔ ‖x‖ = 1 := by
   refine ⟨?_, isIdempotentElem_rankOne_self⟩
   simp only [IsIdempotentElem, mul_def, comp_rankOne, rankOne_apply, inner_self_eq_norm_sq_to_K,
-    map_smul, coe_smul', Pi.smul_apply]
+    map_smul, _root_.smul_apply]
   nth_rw 2 [← one_smul 𝕜 (rankOne 𝕜 x x)]
   rw [← sub_eq_zero, ← sub_smul]
   simp only [smul_eq_zero, rankOne_eq_zero, hx, or_self, or_false, sub_eq_zero, sq_eq_one_iff,
diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
index 429cc48151b15d..a8ed2b8a9e530b 100644
--- a/Mathlib/Analysis/InnerProductSpace/PiL2.lean
+++ b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
@@ -1300,7 +1300,7 @@ theorem InnerProductSpace.toMatrix_rankOne {𝕜 E F ι ι' : Type*} [RCLike 
     (b' : OrthonormalBasis ι' 𝕜 F) :
     (rankOne 𝕜 x y).toMatrix b'.toBasis b = .vecMulVec (b.repr x) (star (b'.repr y)) := by
   have := Fintype.ofFinite ι
-  rw [rankOne_def', ContinuousLinearMap.coe_comp, toLinearMap_toSpanSingleton,
+  rw [rankOne_def', ContinuousLinearMap.toLinearMap_comp, toLinearMap_toSpanSingleton,
     toMatrix_comp _ (OrthonormalBasis.singleton Unit 𝕜).toBasis, toMatrix_toSpanSingleton,
     toLinearMap_innerSL_apply, toMatrix_innerₛₗ_apply, OrthonormalBasis.toBasis_singleton,
     Basis.coe_singleton, Matrix.vecMulVec_one, OrthonormalBasis.coe_singleton, star_one,
diff --git a/Mathlib/Analysis/InnerProductSpace/Positive.lean b/Mathlib/Analysis/InnerProductSpace/Positive.lean
index aa2b6607e89991..db2e667423e284 100644
--- a/Mathlib/Analysis/InnerProductSpace/Positive.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Positive.lean
@@ -402,8 +402,8 @@ end LinearMap
 theorem IsPositive.conj_starProjection (U : Submodule 𝕜 E) {T : E →L[𝕜] E} (hT : T.IsPositive)
     [U.HasOrthogonalProjection] :
     (U.starProjection ∘L T ∘L U.starProjection).IsPositive := by
-  simp only [isPositive_iff, IsSymmetric, coe_comp, LinearMap.coe_comp, coe_coe,
-    Function.comp_apply, coe_comp']
+  simp only [isPositive_iff, IsSymmetric, toLinearMap_comp, LinearMap.coe_comp, coe_coe,
+    Function.comp_apply, comp_apply]
   simp_rw [← coe_coe, U.starProjection_isSymmetric _, hT.isSymmetric _,
     U.starProjection_isSymmetric _, ← U.starProjection_isSymmetric _, coe_coe,
     hT.inner_nonneg_right, implies_true, and_self]
@@ -411,8 +411,8 @@ theorem IsPositive.conj_starProjection (U : Submodule 𝕜 E) {T : E →L[𝕜]
 theorem IsPositive.orthogonalProjectionOnto_comp {T : E →L[𝕜] E} (hT : T.IsPositive)
     (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] :
     (U.orthogonalProjectionOnto ∘L T ∘L U.subtypeL).IsPositive := by
-  simp only [isPositive_iff, IsSymmetric, coe_comp, LinearMap.coe_comp, coe_coe,
-    Function.comp_apply, coe_comp']
+  simp only [isPositive_iff, IsSymmetric, toLinearMap_comp, LinearMap.coe_comp, coe_coe,
+    Function.comp_apply, comp_apply]
   simp_rw [U.inner_orthogonalProjectionOnto_eq_of_mem_right, Submodule.subtypeL_apply,
     U.inner_orthogonalProjectionOnto_eq_of_mem_left, ← coe_coe, hT.isSymmetric _, coe_coe,
     hT.inner_nonneg_right, implies_true, and_self]
@@ -547,7 +547,7 @@ theorem ContinuousLinearMap.isPositive_iff_eq_sum_rankOne [FiniteDimensional 
   let a (i : Fin (Module.finrank 𝕜 E)) : E :=
     ((hT.isSymmetric.eigenvalues rfl i).sqrt : 𝕜) • hT.isSymmetric.eigenvectorBasis rfl i
   refine ⟨Module.finrank 𝕜 E, a, ext fun _ ↦ ?_⟩
-  simp_rw [sum_apply, rankOne_apply, a, inner_smul_left, smul_smul, mul_assoc, conj_ofReal,
+  simp_rw [_root_.sum_apply, rankOne_apply, a, inner_smul_left, smul_smul, mul_assoc, conj_ofReal,
     mul_comm (⟪_, _⟫_𝕜), ← mul_assoc, ← ofReal_mul,
     ← Real.sqrt_mul (hT.toLinearMap.nonneg_eigenvalues rfl _),
     Real.sqrt_mul_self (hT.toLinearMap.nonneg_eigenvalues rfl _), mul_comm _ (⟪_, _⟫_𝕜),
@@ -561,6 +561,6 @@ theorem Matrix.posSemidef_iff_eq_sum_vecMulVec {n : Type*} [Finite n] {M : Matri
   rw [← isPositive_toEuclideanLin_iff, ← isPositive_toContinuousLinearMap_iff,
     isPositive_iff_eq_sum_rankOne]
   simp_rw [eq_comm, ← LinearEquiv.symm_apply_eq, coe_toContinuousLinearMap_symm,
-    ContinuousLinearMap.coe_sum, map_sum, symm_toEuclideanLin_rankOne, eq_comm]
+    ContinuousLinearMap.toLinearMap_sum, map_sum, symm_toEuclideanLin_rankOne, eq_comm]
   exact ⟨fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ (u i).ofLp, hu⟩,
     fun ⟨m, u, hu⟩ ↦ ⟨m, fun i ↦ WithLp.toLp 2 (u i), hu⟩⟩
diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean
index 2f61e294b40217..e3d77f07daa77d 100644
--- a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean
@@ -324,7 +324,7 @@ open ContinuousLinearMap in
 lemma ker_starProjection (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] :
     U.starProjection.ker = Uᗮ := by
   rw [LinearMap.IsIdempotentElem.ker_eq_range U.isIdempotentElem_starProjection.toLinearMap,
-    ← range_starProjection Uᗮ, starProjection_orthogonal, coe_sub, coe_id]
+    ← range_starProjection Uᗮ, starProjection_orthogonal, toLinearMap_sub, coe_id]
 
 theorem _root_.LinearIsometry.map_starProjection {E E' : Type*} [NormedAddCommGroup E]
     [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E')
@@ -509,7 +509,7 @@ theorem starProjection_comp_starProjection_eq_zero_iff {U V : Submodule 𝕜 E}
   refine ⟨fun h => ?_, fun h => h.starProjection_comp_starProjection⟩
   rw [← orthogonalProjectionOnto_comp_subtypeL_eq_zero_iff]
   simp only [ContinuousLinearMap.ext_iff, ContinuousLinearMap.comp_apply, subtypeL_apply,
-    starProjection_apply, ContinuousLinearMap.zero_apply, coe_eq_zero] at h ⊢
+    starProjection_apply, zero_apply, coe_eq_zero] at h ⊢
   intro x
   simpa using h (x : E)
 
diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean b/Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean
index 91f6cf9972e6c3..8d239d8f93b8d4 100644
--- a/Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean
@@ -150,7 +150,7 @@ theorem LinearIsometryEquiv.reflections_generate_dim_aux [FiniteDimensional ℝ
     symm
     ext x
     have := LinearMap.congr_fun (LinearMap.ker_eq_top.mp this) x
-    simpa only [sub_eq_zero, ContinuousLinearMap.coe_sub, LinearMap.sub_apply,
+    simpa only [sub_eq_zero, ContinuousLinearMap.toLinearMap_sub, LinearMap.sub_apply,
       LinearMap.zero_apply] using! this
   | succ n IH =>
     -- Inductive step.  Let `W` be the fixed subspace of `φ`.  We suppose its complement to have
diff --git a/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean b/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
index 4b058b7db26694..d1eb401d913e89 100644
--- a/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
@@ -203,7 +203,7 @@ theorem _root_.LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf {T : F 
     HasStrictFDerivAt T.reApplyInnerSelf (2 • (innerSL ℝ (T x₀))) x₀ := by
   convert! T.hasStrictFDerivAt.inner ℝ (hasStrictFDerivAt_id x₀) using 1
   ext y
-  rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.comp_apply, fderivInnerCLM_apply,
+  rw [smul_apply, ContinuousLinearMap.comp_apply, fderivInnerCLM_apply,
     ContinuousLinearMap.prod_apply, innerSL_apply_apply, id, ContinuousLinearMap.id_apply,
     hT.apply_clm x₀ y, real_inner_comm _ x₀, two_smul]
 
diff --git a/Mathlib/Analysis/InnerProductSpace/Reproducing.lean b/Mathlib/Analysis/InnerProductSpace/Reproducing.lean
index bb21216c57c084..7d3d0ed6787d99 100644
--- a/Mathlib/Analysis/InnerProductSpace/Reproducing.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Reproducing.lean
@@ -188,8 +188,8 @@ theorem posSemidef_tfae : List.TFAE [K.PosSemidef, K.IsHermitian ∧ ∀ (f : X
   refine this fun hHerm ↦ ?_
   simp only [nonneg_iff_isPositive, isPositive_def', isSelfAdjoint_finsuppSum hHerm,
     reApplyInnerSelf_apply, true_and]
-  simp only [star_eq_adjoint, zero_apply, add_apply, implies_true, Finsupp.sum_apply'', coe_mul',
-    Function.comp_apply, Finsupp.sum_inner, adjoint_inner_left]
+  simp only [star_eq_adjoint, zero_apply, add_apply, implies_true, Finsupp.sum_apply'',
+    FunLike.coe_mul_eq_comp, Function.comp_apply, Finsupp.sum_inner, adjoint_inner_left]
   -- FIXME: nontriviality should work here
   refine (subsingleton_or_nontrivial V).elim (fun h ↦ ?_) fun _ ↦ ?_
   · have : ∀ v : V, v = 0 := fun v ↦ Subsingleton.elim v 0
diff --git a/Mathlib/Analysis/InnerProductSpace/StarOrder.lean b/Mathlib/Analysis/InnerProductSpace/StarOrder.lean
index 2cce83da0394cd..94f4bd0d837e4e 100644
--- a/Mathlib/Analysis/InnerProductSpace/StarOrder.lean
+++ b/Mathlib/Analysis/InnerProductSpace/StarOrder.lean
@@ -41,9 +41,9 @@ lemma IsPositive.spectrumRestricts {f : H →L[𝕜] H} (hf : f.IsPositive) :
   set c := -c
   exact isUnit_of_forall_le_norm_inner_map _ (c := ⟨c, hc.le⟩) hc fun x ↦ calc
     ‖x‖ ^ 2 * c = re ⟪algebraMap ℝ (H →L[𝕜] H) c x, x⟫_𝕜 := by
-      rw [Algebra.algebraMap_eq_smul_one, ← algebraMap_smul 𝕜 c (1 : (H →L[𝕜] H)), coe_smul',
-        Pi.smul_apply, one_apply, inner_smul_left, RCLike.algebraMap_eq_ofReal, conj_ofReal,
-        re_ofReal_mul, inner_self_eq_norm_sq, mul_comm]
+      rw [Algebra.algebraMap_eq_smul_one, ← algebraMap_smul 𝕜 c (1 : (H →L[𝕜] H)), smul_apply,
+        one_apply_eq_self, inner_smul_left, RCLike.algebraMap_eq_ofReal, conj_ofReal, re_ofReal_mul,
+        inner_self_eq_norm_sq, mul_comm]
     _ ≤ re ⟪(f + (algebraMap ℝ (H →L[𝕜] H)) c) x, x⟫_𝕜 := by
       simpa only [add_apply, inner_add_left, map_add, le_add_iff_nonneg_left]
         using hf.re_inner_nonneg_left x
diff --git a/Mathlib/Analysis/InnerProductSpace/Trace.lean b/Mathlib/Analysis/InnerProductSpace/Trace.lean
index d55c0d61ae319a..4af5d0e42fd3ae 100644
--- a/Mathlib/Analysis/InnerProductSpace/Trace.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Trace.lean
@@ -49,8 +49,8 @@ lemma IsSymmetric.re_trace_eq_sum_eigenvalues {T : E →ₗ[𝕜] E} (hT : T.IsS
 open InnerProductSpace in
 lemma _root_.InnerProductSpace.trace_rankOne (x y : E) :
     (rankOne 𝕜 x y).trace 𝕜 E = inner 𝕜 y x := by
-  rw [rankOne_def', ContinuousLinearMap.coe_comp, trace_comp_comm',
-    ← ContinuousLinearMap.coe_comp, ContinuousLinearMap.comp_toSpanSingleton]
+  rw [rankOne_def', ContinuousLinearMap.toLinearMap_comp, trace_comp_comm',
+    ← ContinuousLinearMap.toLinearMap_comp, ContinuousLinearMap.comp_toSpanSingleton]
   simp [trace_eq_sum_inner _ (OrthonormalBasis.singleton Unit 𝕜)]
 
 end LinearMap
diff --git a/Mathlib/Analysis/LocallyConvex/Separation.lean b/Mathlib/Analysis/LocallyConvex/Separation.lean
index 0b60ee86f7af5c..042f0b08b8fb9c 100644
--- a/Mathlib/Analysis/LocallyConvex/Separation.lean
+++ b/Mathlib/Analysis/LocallyConvex/Separation.lean
@@ -144,7 +144,7 @@ theorem geometric_hahn_banach_open_open (hs₁ : Convex ℝ s) (hs₂ : IsOpen s
   rw [← interior_Ici]
   refine interior_maximal (image_subset_iff.2 hf₂) (f.isOpenMap_of_ne_zero ?_ _ ht₃)
   rintro rfl
-  simp_rw [ContinuousLinearMap.zero_apply] at hf₁ hf₂
+  simp_rw [zero_apply] at hf₁ hf₂
   exact (hf₁ _ ha₀).not_ge (hf₂ _ hb₀)
 
 /-- If `s` and `t` are convex, `interior s` is nonempty and disjoint from `t`, then a nonzero
diff --git a/Mathlib/Analysis/Normed/Group/SeparationQuotient.lean b/Mathlib/Analysis/Normed/Group/SeparationQuotient.lean
index c0c54386dd340f..6db6b0ef4994ca 100644
--- a/Mathlib/Analysis/Normed/Group/SeparationQuotient.lean
+++ b/Mathlib/Analysis/Normed/Group/SeparationQuotient.lean
@@ -133,7 +133,7 @@ theorem normedMk_eq_zero_iff : normedMk (M := M) = 0 ↔ ∀ (x : M), ‖x‖ =
     rw [SeparationQuotient.mk_eq_zero_iff.mp]
     have : normedMk x = 0 := by
       rw [h]
-      simp only [zero_apply]
+      simp only [NormedAddGroupHom.zero_apply]
     rw [← this]
     simp
   · intro h
diff --git a/Mathlib/Analysis/Normed/Module/Bases.lean b/Mathlib/Analysis/Normed/Module/Bases.lean
index bb322bb074a2d0..04f6571614bc88 100644
--- a/Mathlib/Analysis/Normed/Module/Bases.lean
+++ b/Mathlib/Analysis/Normed/Module/Bases.lean
@@ -156,7 +156,7 @@ theorem proj_empty : b.proj ∅ = 0 := by simp [proj]
 /-- The action of the projection on a vector `x`. -/
 @[simp]
 theorem proj_apply (A : Finset β) (x : X) : b.proj A x = ∑ i ∈ A, b.coord i x • b i := by
-  simp [proj, ContinuousLinearMap.sum_apply, ContinuousLinearMap.smulRight_apply]
+  simp [proj, _root_.sum_apply, ContinuousLinearMap.smulRight_apply]
 
 open scoped Classical in
 /-- The action of the projection on a basis element `e i`. -/
@@ -371,7 +371,7 @@ lemma sum_succSub (P : ℕ → X →L[𝕜] X) (h0 : P 0 = 0) (n : ℕ) :
 /-- The operators `succSub P i` satisfy a biorthogonality relation. -/
 lemma succSub_ortho {P : ℕ → X →L[𝕜] X} (hcomp : ∀ n m, ∀ x : X, P n (P m x) = P (min n m) x)
     (i j : ℕ) (x : X) : succSub P i (succSub P j x) = if i = j then succSub P j x else 0 := by
-  simp only [succSub, ContinuousLinearMap.sub_apply, map_sub, hcomp,
+  simp only [succSub, _root_.sub_apply, map_sub, hcomp,
     Nat.add_min_add_right]
   split_ifs with h
   · rw [h, min_self, min_eq_right (Nat.le_succ j), Nat.min_eq_left (Nat.le_succ j)]
@@ -504,14 +504,14 @@ def basis : SchauderBasis 𝕜 X :=
       exact (D.proj_tendsto x).congr fun n ↦ by
         simp only [Function.comp, LinearMap.coe_mk, AddHom.coe_mk,
                    LinearMap.mkContinuous_apply, ← hcoeff]
-        rw [← ContinuousLinearMap.sum_apply, sum_succSub D.P D.proj_zero] }
+        rw [← _root_.sum_apply, sum_succSub D.P D.proj_zero] }
 
 /-- The projections of the constructed basis correspond to the input data `D.P`. -/
 @[simp]
 theorem basis_proj : (basis D).proj = D.P := by
   ext n _
   rw [SchauderBasis.proj_apply, ← sum_succSub D.P D.proj_zero n]
-  simp only [ContinuousLinearMap.coe_sum', Finset.sum_apply]
+  simp only [_root_.sum_apply]
   refine Finset.sum_congr rfl fun i _ ↦ ?_
   dsimp [basis, mkContinuous_apply, IsLinearMap.mk'_apply]
   rw [basisCoeff_spec]
diff --git a/Mathlib/Analysis/Normed/Module/ContinuousInverse.lean b/Mathlib/Analysis/Normed/Module/ContinuousInverse.lean
index 04788b4319f136..ef344f29e422d6 100644
--- a/Mathlib/Analysis/Normed/Module/ContinuousInverse.lean
+++ b/Mathlib/Analysis/Normed/Module/ContinuousInverse.lean
@@ -144,14 +144,14 @@ lemma comp {g : F →L[R] G} (hg : g.HasLeftInverse) (hf : f.HasLeftInverse) :
   obtain ⟨finv, hfinv⟩ := hf
   obtain ⟨ginv, hginv⟩ := hg
   refine ⟨finv.comp ginv, fun x ↦ ?_⟩
-  simp only [coe_comp', Function.comp_apply]
+  simp only [comp_apply]
   rw [hginv, hfinv]
 
 lemma of_comp {g : F →L[R] G} (hfg : (g.comp f).HasLeftInverse) :
     f.HasLeftInverse := by
   obtain ⟨fginv, hfginv⟩ := hfg
   refine ⟨fginv.comp g, fun y ↦ ?_⟩
-  simp only [coe_comp', Function.comp_apply]
+  simp only [comp_apply]
   exact hfginv y
 
 lemma comp_continuousLinearEquivalence {f₀ : F' ≃L[R] E} (hf : f.HasLeftInverse) :
@@ -212,7 +212,7 @@ lemma closedComplemented_range (hf : f.HasLeftInverse) : Submodule.ClosedComplem
   use (f.comp hf.leftInverse).codRestrict f.range (by intro y; simp)
   rintro ⟨y, x, rfl⟩
   ext
-  simp only [coe_coe, coe_codRestrict_apply, coe_comp', Function.comp_apply]
+  simp only [coe_coe, coe_codRestrict_apply, comp_apply]
   rw [hf.leftInverse_leftInverse]
 
 section
@@ -310,7 +310,7 @@ lemma comp {g : F →L[R] G} (hg : g.HasRightInverse) (hf : f.HasRightInverse) :
   obtain ⟨finv, hfinv⟩ := hf
   obtain ⟨ginv, hginv⟩ := hg
   refine ⟨finv.comp ginv, fun x ↦ ?_⟩
-  simp only [coe_comp', Function.comp_apply]
+  simp only [comp_apply]
   rw [hfinv, hginv]
 
 lemma of_comp {g : F →L[R] G} (hfg : (g.comp f).HasRightInverse) :
diff --git a/Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean b/Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean
index 6ee1cf8378902f..e5501a08ca9ad5 100644
--- a/Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean
+++ b/Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean
@@ -941,11 +941,11 @@ def flipMultilinear (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') :
           exact (f x).le_of_opNorm_le (f.le_opNorm x) _
       map_update_add' := fun m i x y => by
         ext1
-        simp only [add_apply, ContinuousMultilinearMap.map_update_add, LinearMap.coe_mk,
+        simp only [_root_.add_apply, ContinuousMultilinearMap.map_update_add, LinearMap.coe_mk,
           LinearMap.mkContinuous_apply, AddHom.coe_mk]
       map_update_smul' := fun m i c x => by
         ext1
-        simp only [coe_smul', ContinuousMultilinearMap.map_update_smul, LinearMap.coe_mk,
+        simp only [FunLike.coe_smul, ContinuousMultilinearMap.map_update_smul, LinearMap.coe_mk,
           LinearMap.mkContinuous_apply, Pi.smul_apply, AddHom.coe_mk] }
     ‖f‖ fun m => by
       dsimp only [MultilinearMap.coe_mk]
diff --git a/Mathlib/Analysis/Normed/Operator/Bilinear.lean b/Mathlib/Analysis/Normed/Operator/Bilinear.lean
index ebd617afa71905..187148928cc83d 100644
--- a/Mathlib/Analysis/Normed/Operator/Bilinear.lean
+++ b/Mathlib/Analysis/Normed/Operator/Bilinear.lean
@@ -263,7 +263,7 @@ def compSL : (F →SL[σ₂₃] G) →L[𝕜₃] (E →SL[σ₁₂] F) →SL[σ
   LinearMap.mkContinuous₂
     (LinearMap.mk₂'ₛₗ (RingHom.id 𝕜₃) σ₂₃ comp add_comp smul_comp comp_add fun c f g => by
       ext
-      simp only [map_smulₛₗ, coe_smul', coe_comp', Function.comp_apply, Pi.smul_apply])
+      simp only [map_smulₛₗ, comp_apply, smul_apply])
     1 fun f g => by simpa only [one_mul] using! opNorm_comp_le f g
 
 theorem norm_compSL_le : ‖compSL E F G σ₁₂ σ₂₃‖ ≤ 1 :=
@@ -423,8 +423,7 @@ def smulRightL : StrongDual 𝕜 E →L[𝕜] Fₗ →L[𝕜] E →L[𝕜] Fₗ
         simp only [add_smul, coe_smulRightₗ, add_apply, smulRight_apply, LinearMap.add_apply]
       map_smul' := fun m c => by
         ext x
-        dsimp
-        rw [smul_smul] }
+        simp [smul_smul] }
     1 fun c x => by
       simp only [coe_smulRightₗ, one_mul, norm_smulRight_apply, LinearMap.coe_mk, AddHom.coe_mk,
         le_refl]
diff --git a/Mathlib/Analysis/Normed/Operator/Compact/Basic.lean b/Mathlib/Analysis/Normed/Operator/Compact/Basic.lean
index 5d56fbdd627983..7a8e40734c48b4 100644
--- a/Mathlib/Analysis/Normed/Operator/Compact/Basic.lean
+++ b/Mathlib/Analysis/Normed/Operator/Compact/Basic.lean
@@ -446,7 +446,7 @@ theorem isClosed_setOf_isCompactOperator {𝕜₁ 𝕜₂ : Type*} [Nontrivially
   refine ⟨t, ht, ?_⟩
   rw [mem_preimage, mem_vadd_set_iff_neg_vadd_mem, vadd_eq_add, neg_add_eq_sub] at htx ⊢
   convert! hVU _ htx _ (huv x hx) using 1
-  rw [ContinuousLinearMap.sub_apply]
+  rw [sub_apply]
   abel
 
 theorem compactOperator_topologicalClosure {𝕜₁ 𝕜₂ : Type*} [NontriviallyNormedField 𝕜₁]
diff --git a/Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean b/Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean
index 9fd02a5ae5b174..a91bff2098caad 100644
--- a/Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean
+++ b/Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean
@@ -68,7 +68,7 @@ public theorem ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv
   set T := apply' _ (.id 𝕜) z ∘L f.toContinuousAlgHom.toContinuousLinearMap ∘L smulRightL 𝕜 _ _ v
   have hT x : T x = f (smulRight v x) z := rfl
   have this A x : T (A x) = f A (T x) := by
-    simp only [hT, ← mul_apply, ← map_mul]
+    simp only [hT, ← mul_apply_eq_comp, ← map_mul]
     congr; ext; simp
   have ⟨d, hd⟩ := SeparatingDual.exists_eq_one (R := 𝕜) hz
   have surj : Function.Surjective T := fun w ↦ ⟨f.symm (smulRight d w) u, by simp [T, this, hd]⟩
diff --git a/Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean b/Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean
index 25ddf12a0d5810..1236db2da757f6 100644
--- a/Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean
+++ b/Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean
@@ -123,8 +123,8 @@ theorem norm_mul_le_const_mul_norm {i : ι} (hBi : B i = (1 : L))
       IsNonarchimedean.finset_image_add hna'
         (fun i ↦ (B.repr x i • ∑ i_1 : ι, B.repr y i_1 • B.repr (B i * B i_1)) ixy)
         (univ : Finset ι)
-    simp only [Finsupp.coe_smul, Finsupp.coe_finsetSum, Pi.smul_apply, sum_apply, smul_eq_mul,
-      norm_mul] at hk ⊢
+    simp only [Finsupp.coe_smul, Finsupp.coe_finsetSum, Pi.smul_apply, Finset.sum_apply,
+      smul_eq_mul, norm_mul] at hk ⊢
     apply le_trans hk
     -- We use the above property again.
     obtain ⟨k', hk'⟩ : ∃ (k' : ι),
diff --git a/Mathlib/Analysis/SpecialFunctions/Exponential.lean b/Mathlib/Analysis/SpecialFunctions/Exponential.lean
index 4032b7535520ec..d4285ca6039335 100644
--- a/Mathlib/Analysis/SpecialFunctions/Exponential.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Exponential.lean
@@ -267,7 +267,7 @@ theorem hasFDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : 𝕊)
     rw [← hasFDerivAt_iff_isLittleO_nhds_zero (f := fun u => exp (u • x))
       (f' := (1 : 𝕊 →L[𝕂] 𝕊).smulRight x) (x := 0)]
     have : HasFDerivAt exp (1 : 𝔸 →L[𝕂] 𝔸) ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x 0) := by
-      rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, zero_smul]
+      rw [ContinuousLinearMap.smulRight_apply, one_apply_eq_self, zero_smul]
       exact hasFDerivAt_exp_zero_of_radius_pos htx.pos
     exact this.comp 0 ((1 : 𝕊 →L[𝕂] 𝕊).smulRight x).hasFDerivAt
   have : Tendsto (fun h : 𝕊 => h • x) (𝓝 0) (𝓝 0) := by
@@ -278,9 +278,9 @@ theorem hasFDerivAt_exp_smul_const_of_mem_ball (x : 𝔸) (t : 𝕊)
   filter_upwards [this] with h hh
   have : Commute (t • x) (h • x) := ((Commute.refl x).smul_left t).smul_right h
   rw [add_smul t h, exp_add_of_commute_of_mem_ball this htx hh, zero_add, zero_smul, exp_zero,
-    ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply,
-    ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply,
-    ContinuousLinearMap.one_apply, smul_eq_mul, mul_sub_left_distrib, mul_sub_left_distrib, mul_one]
+    ContinuousLinearMap.smulRight_apply, one_apply_eq_self,
+    _root_.smul_apply, ContinuousLinearMap.smulRight_apply,
+    one_apply_eq_self, smul_eq_mul, mul_sub_left_distrib, mul_sub_left_distrib, mul_one]
 
 theorem hasFDerivAt_exp_smul_const_of_mem_ball' (x : 𝔸) (t : 𝕊)
     (htx : t • x ∈ Metric.eball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
index ef84fd20d7005d..6c642b86a86689 100644
--- a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
@@ -183,9 +183,9 @@ expected by lemmas like `HasDerivAt.cpow`. -/
 private theorem aux : ((g x * f x ^ (g x - 1)) • (1 : ℂ →L[ℂ] ℂ).smulRight f' +
     (f x ^ g x * log (f x)) • (1 : ℂ →L[ℂ] ℂ).smulRight g') 1 =
       g x * f x ^ (g x - 1) * f' + f x ^ g x * log (f x) * g' := by
-  simp only [smul_eq_mul, one_mul, ContinuousLinearMap.one_apply,
-    ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.add_apply, Pi.smul_apply,
-    ContinuousLinearMap.coe_smul']
+  simp only [smul_eq_mul, one_mul, one_apply_eq_self,
+    ContinuousLinearMap.smulRight_apply, add_apply, Pi.smul_apply,
+    FunLike.coe_smul']
 
 nonrec theorem HasStrictDerivAt.cpow (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x)
     (h0 : f x ∈ slitPlane) : HasStrictDerivAt (fun x => f x ^ g x)
@@ -672,7 +672,7 @@ theorem HasDerivWithinAt.rpow (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWit
     (h : 0 < f x) : HasDerivWithinAt (fun x => f x ^ g x)
       (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) s x := by
   convert! (hf.hasFDerivWithinAt.rpow hg.hasFDerivWithinAt h).hasDerivWithinAt using 1
-  dsimp; ring
+  simp; ring
 
 theorem HasDerivAt.rpow (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) (h : 0 < f x) :
     HasDerivAt (fun x => f x ^ g x)
diff --git a/Mathlib/Geometry/Euclidean/Volume/Measure.lean b/Mathlib/Geometry/Euclidean/Volume/Measure.lean
index 24222a8a6f8976..e3a22b453f5dc1 100644
--- a/Mathlib/Geometry/Euclidean/Volume/Measure.lean
+++ b/Mathlib/Geometry/Euclidean/Volume/Measure.lean
@@ -134,12 +134,12 @@ theorem IsometryEquiv.measurePreserving_euclideanHausdorffMeasure (e : X ≃ᵢ
 
 theorem Isometry.euclideanHausdorffMeasure_image {f : X → Y} {d : ℕ} (hf : Isometry f) (s : Set X) :
     μHE[d] (f '' s) = μHE[d] s := by
-  simp_rw [euclideanHausdorffMeasure_def, smul_apply]
+  simp_rw [euclideanHausdorffMeasure_def, Measure.smul_apply]
   rw [Isometry.hausdorffMeasure_image hf (by simp)]
 
 theorem Isometry.euclideanHausdorffMeasure_preimage {f : X → Y} {d : ℕ} (hf : Isometry f)
     (s : Set Y) : μHE[d] (f ⁻¹' s) = μHE[d] (s ∩ Set.range f) := by
-  simp_rw [euclideanHausdorffMeasure_def, smul_apply]
+  simp_rw [euclideanHausdorffMeasure_def, Measure.smul_apply]
   rw [Isometry.hausdorffMeasure_preimage hf (by simp)]
 
 theorem Isometry.map_euclideanHausdorffMeasure {f : X → Y} {d : ℕ} (hf : Isometry f) :
@@ -167,13 +167,13 @@ variable {𝕜 V P : Type*} [NormedField 𝕜] [NormedAddCommGroup V] [NormedSpa
 theorem MeasureTheory.euclideanHausdorffMeasure_homothety_image (d : ℕ) (x : P) {c : 𝕜}
     (hc : c ≠ 0) (s : Set P) :
     μHE[d] (AffineMap.homothety x c '' s) = ‖c‖₊ ^ d • μHE[d] s := by
-  simp_rw [euclideanHausdorffMeasure_def, smul_apply]
+  simp_rw [euclideanHausdorffMeasure_def, Measure.smul_apply]
   rw [hausdorffMeasure_homothety_image (by simp) x hc, smul_comm, NNReal.rpow_natCast]
 
 theorem MeasureTheory.euclideanHausdorffMeasure_homothety_preimage (d : ℕ) (x : P) {c : 𝕜}
     (hc : c ≠ 0) (s : Set P) :
     μHE[d] (AffineMap.homothety x c ⁻¹' s) = ‖c‖₊⁻¹ ^ d • μHE[d] s := by
-  simp_rw [euclideanHausdorffMeasure_def, smul_apply]
+  simp_rw [euclideanHausdorffMeasure_def, Measure.smul_apply]
   rw [hausdorffMeasure_homothety_preimage (by simp) x hc, smul_comm, NNReal.rpow_natCast]
 
 end Homothety
diff --git a/Mathlib/Geometry/Manifold/Instances/Icc.lean b/Mathlib/Geometry/Manifold/Instances/Icc.lean
index 6711077b3caad1..1db01c146b7d21 100644
--- a/Mathlib/Geometry/Manifold/Instances/Icc.lean
+++ b/Mathlib/Geometry/Manifold/Instances/Icc.lean
@@ -186,7 +186,7 @@ lemma mfderivWithin_comp_projIcc_one {f : Icc x y → M} {w : Icc x y} :
   · simp [hw]
   · exact (contMDiffOn_projIcc _ w.2).mdifferentiableWithinAt one_ne_zero
   · exact (uniqueDiffOn_Icc h.out _ w.2).uniqueMDiffWithinAt
-  simp only [Function.comp_apply, ContinuousLinearMap.coe_comp']
+  simp only [Function.comp_apply, ContinuousLinearMap.comp_apply]
   have : w = projIcc x y h.out.le (w : ℝ) := by rw [projIcc_of_mem]
   rw [projIcc_of_mem _ w.2]
   congr 1
diff --git a/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/Mathlib/Geometry/Manifold/Instances/Sphere.lean
index 5cc776dca65562..bd2d69431eba6d 100644
--- a/Mathlib/Geometry/Manifold/Instances/Sphere.lean
+++ b/Mathlib/Geometry/Manifold/Instances/Sphere.lean
@@ -538,7 +538,7 @@ theorem mfderiv_coe_sphere_injective {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v
     simp
   have := congr_arg DFunLike.coe <| (this.comp 0 U.symm.toContinuousLinearEquiv.hasFDerivAt).fderiv
   refine Eq.subst this.symm ?_
-  rw [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe]
+  rw [ContinuousLinearMap.coe_comp, ContinuousLinearEquiv.coe_coe]
   simpa [-Subtype.val_injective] using Subtype.val_injective
 
 end ContMDiffManifold
diff --git a/Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean b/Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
index 08d2b07d5a7e90..39836315da45e3 100644
--- a/Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
+++ b/Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
@@ -178,7 +178,8 @@ lemma IsMIntegralCurveOn.hasDerivWithinAt (hγ : IsMIntegralCurveOn γ v s) {t :
   rw [ContinuousLinearMap.ext_iff]
   intro a
   rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.smulRight_apply, map_smul,
-    ← ContinuousLinearMap.one_apply (R₁ := ℝ) a, ← ContinuousLinearMap.smulRight_apply,
+    ← one_apply_eq_self (F := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, ℝ) t) a,
+    ← ContinuousLinearMap.smulRight_apply,
     mfderiv_chartAt_eq_tangentCoordChange hsrc]
   rfl
 
@@ -196,6 +197,7 @@ lemma IsMIntegralCurveAt.eventually_hasDerivAt (hγ : IsMIntegralCurveAt γ v t
   rw [ContinuousLinearMap.ext_iff]
   intro a
   rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.smulRight_apply, map_smul,
-    ← ContinuousLinearMap.one_apply (R₁ := ℝ) a, ← ContinuousLinearMap.smulRight_apply,
+    ← one_apply_eq_self (F := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, ℝ) t) a,
+    ← ContinuousLinearMap.smulRight_apply,
     mfderiv_chartAt_eq_tangentCoordChange hsrc]
   rfl
diff --git a/Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean b/Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
index 59215c2d3c81e5..ceed7bccd5e562 100644
--- a/Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
+++ b/Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
@@ -102,11 +102,15 @@ end Translation
 
 section Scaling
 
+open Manifold
+
 lemma IsMIntegralCurveOn.comp_mul (hγ : IsMIntegralCurveOn γ v s) (a : ℝ) :
     IsMIntegralCurveOn (γ ∘ (· * a)) (a • v) { t | t * a ∈ s } := by
   intro t ht
-  rw [comp_apply, Pi.smul_apply, ← ContinuousLinearMap.one_apply (R₁ := ℝ) a,
-    ← ContinuousLinearMap.smulRight_comp_smulRight]
+  have : (1 : ℝ →L[ℝ] ℝ).smulRight (a • v (γ (t * a))) =
+      (1 : ℝ →L[ℝ] ℝ).smulRight (v (γ (t * a))) ∘SL (1 : ℝ →L[ℝ] ℝ).smulRight a := by
+    simp [ContinuousLinearMap.smulRight_comp_smulRight]
+  rw [comp_apply, Pi.smul_apply, this]
   refine HasMFDerivWithinAt.comp t (hγ (t * a) ht)
     ⟨(continuous_mul_const _).continuousWithinAt, ?_⟩ subset_rfl
   simp only [mfld_simps]
diff --git a/Mathlib/Geometry/Manifold/Riemannian/PathELength.lean b/Mathlib/Geometry/Manifold/Riemannian/PathELength.lean
index 1ff68e688548e2..bc1507a2f8fa13 100644
--- a/Mathlib/Geometry/Manifold/Riemannian/PathELength.lean
+++ b/Mathlib/Geometry/Manifold/Riemannian/PathELength.lean
@@ -157,7 +157,7 @@ lemma pathELength_comp_of_monotoneOn {f : ℝ → ℝ} (h : a ≤ b) (hf : Monot
     · rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
       exact uniqueDiffOn_Icc h _ ht
   rw [this]
-  simp only [Function.comp_apply, ContinuousLinearMap.coe_comp']
+  simp only [Function.comp_apply, ContinuousLinearMap.comp_apply]
   have : mfderiv[Icc a b] f t 1 = derivWithin f (Icc a b) t • (1 : TangentSpace 𝓘(ℝ) (f t)) := by
     simp only [mfderivWithin_eq_fderivWithin, ← fderivWithin_derivWithin, smul_eq_mul, mul_one]
     rfl
@@ -189,7 +189,7 @@ lemma pathELength_comp_of_antitoneOn {f : ℝ → ℝ} (h : a ≤ b) (hf : Antit
     · rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
       exact uniqueDiffOn_Icc h _ ht
   rw [this]
-  simp only [Function.comp_apply, ContinuousLinearMap.coe_comp']
+  simp only [Function.comp_apply, ContinuousLinearMap.comp_apply]
   have : mfderiv[Icc a b] f t 1
       = derivWithin f (Icc a b) t • (1 : TangentSpace 𝓘(ℝ) (f t)) := by
     simp only [mfderivWithin_eq_fderivWithin, ← fderivWithin_derivWithin, smul_eq_mul, mul_one]
diff --git a/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean b/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean
index d2804d77f3fa36..d107d81b0c2720 100644
--- a/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean
+++ b/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean
@@ -661,7 +661,7 @@ lemma mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt
   have A : (extChartAt I x₀).symm (extChartAt I x₀ x₀) = x₀ := by simp
   by_cases hfi : (mfderiv[s] f x₀).IsInvertible; swap
   · simp only [mlieBracketWithin_apply, mpullbackWithin_apply,
-      ContinuousLinearMap.inverse_of_not_isInvertible hfi, ContinuousLinearMap.zero_apply]
+      ContinuousLinearMap.inverse_of_not_isInvertible hfi, zero_apply]
     rw [lieBracketWithin_eq_zero_of_eq_zero]
     · simp [-extChartAt]
     · simp only [mpullbackWithin_apply]
diff --git a/Mathlib/Geometry/Manifold/WhitneyEmbedding.lean b/Mathlib/Geometry/Manifold/WhitneyEmbedding.lean
index 9928619fe1d333..84b12fa4431b1b 100644
--- a/Mathlib/Geometry/Manifold/WhitneyEmbedding.lean
+++ b/Mathlib/Geometry/Manifold/WhitneyEmbedding.lean
@@ -89,7 +89,7 @@ theorem comp_embeddingPiTangent_mfderiv (x : M) (hx : x ∈ s) :
   convert! hasMFDerivAt_unique this _
   refine (hasMFDerivAt_extChartAt (f.mem_chartAt_ind_source x hx)).congr_of_eventuallyEq ?_
   refine (f.eventuallyEq_one x hx).mono fun y hy => ?_
-  simp only [L, embeddingPiTangent_coe, ContinuousLinearMap.coe_comp', (· ∘ ·),
+  simp only [L, embeddingPiTangent_coe, ContinuousLinearMap.coe_comp, (· ∘ ·),
     ContinuousLinearMap.coe_fst', ContinuousLinearMap.proj_apply]
   rw [hy, Pi.one_apply, one_smul]
 
diff --git a/Mathlib/LinearAlgebra/Eigenspace/ContinuousLinearMap.lean b/Mathlib/LinearAlgebra/Eigenspace/ContinuousLinearMap.lean
index c04d7e8e20d63b..cd95994b29a597 100644
--- a/Mathlib/LinearAlgebra/Eigenspace/ContinuousLinearMap.lean
+++ b/Mathlib/LinearAlgebra/Eigenspace/ContinuousLinearMap.lean
@@ -26,7 +26,7 @@ variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] [TopologicalSp
 open Module End
 
 instance isClosed_genEigenspace : IsClosed (genEigenspace (f : End R M) μ n : Set M) := by
-  rw [genEigenspace_nat, one_eq_id, ← coe_id, ← coe_smul, ← coe_sub, ← coe_pow]
+  rw [genEigenspace_nat, one_eq_id, ← coe_id, ← toLinearMap_smul, ← toLinearMap_sub, ← coe_pow]
   apply isClosed_ker
 
 instance isClosed_eigenspace : IsClosed (eigenspace (f : End R M) μ : Set M) :=
diff --git a/Mathlib/MeasureTheory/Function/Jacobian.lean b/Mathlib/MeasureTheory/Function/Jacobian.lean
index 61c028c472bcaf..3332b2a233cf83 100644
--- a/Mathlib/MeasureTheory/Function/Jacobian.lean
+++ b/Mathlib/MeasureTheory/Function/Jacobian.lean
@@ -168,7 +168,7 @@ theorem exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt [SecondCou
     calc
       ‖f y - f x - (f' z) (y - x)‖ = ‖f y - f x - (f' x) (y - x) + (f' x - f' z) (y - x)‖ := by
         congr 1
-        simp only [ContinuousLinearMap.coe_sub', map_sub, Pi.sub_apply]
+        simp only [FunLike.coe_sub, map_sub, Pi.sub_apply]
         abel
       _ ≤ ‖f y - f x - (f' x) (y - x)‖ + ‖(f' x - f' z) (y - x)‖ := norm_add_le _ _
       _ ≤ ε * ‖y - x‖ + ‖f' x - f' z‖ * ‖y - x‖ := by
@@ -524,7 +524,7 @@ theorem _root_.ApproximatesLinearOn.norm_fderiv_sub_le {A : E →L[ℝ] E} {δ :
       r * ‖(f' x - A) a‖ = ‖(f' x - A) (r • a)‖ := by
         simp only [map_smul, norm_smul, Real.norm_eq_abs, abs_of_nonneg rpos.le]
       _ = ‖f y - f x - A (y - x) - (f y - f x - (f' x) (y - x))‖ := by
-        simp only [ya, add_sub_cancel_left, sub_sub_sub_cancel_left, ContinuousLinearMap.coe_sub',
+        simp only [ya, add_sub_cancel_left, sub_sub_sub_cancel_left, FunLike.coe_sub,
           Pi.sub_apply, map_smul, smul_sub]
       _ ≤ ‖f y - f x - A (y - x)‖ + ‖f y - f x - (f' x) (y - x)‖ := norm_sub_le _ _
       _ ≤ δ * ‖y - x‖ + ε * ‖y - x‖ := (add_le_add (hf _ ys _ xs) (hρ ⟨rρ hy, ys⟩))
@@ -535,7 +535,7 @@ theorem _root_.ApproximatesLinearOn.norm_fderiv_sub_le {A : E →L[ℝ] E} {δ :
   calc
     ‖(f' x - A) z‖ = ‖(f' x - A) a + (f' x - A) (z - a)‖ := by
       congr 1
-      simp only [ContinuousLinearMap.coe_sub', map_sub, Pi.sub_apply]
+      simp only [FunLike.coe_sub, map_sub, Pi.sub_apply]
       abel
     _ ≤ ‖(f' x - A) a‖ + ‖(f' x - A) (z - a)‖ := norm_add_le _ _
     _ ≤ (δ + ε) * (‖z‖ + ε) + ‖f' x - A‖ * ‖z - a‖ := by
diff --git a/Mathlib/MeasureTheory/Function/JacobianOneDim.lean b/Mathlib/MeasureTheory/Function/JacobianOneDim.lean
index 78c262f6f051bb..bf5c520217f58f 100644
--- a/Mathlib/MeasureTheory/Function/JacobianOneDim.lean
+++ b/Mathlib/MeasureTheory/Function/JacobianOneDim.lean
@@ -210,7 +210,7 @@ theorem lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn (hs : MeasurableSet
       = ∫⁻ x in c, ENNReal.ofReal (|(F' x).det|) * u (f x) := by
     apply setLIntegral_congr_fun hc (fun x hx ↦ ?_)
     simp only [LinearMap.det_ring, ContinuousLinearMap.coe_coe, ContinuousLinearMap.smulRight_apply,
-      ContinuousLinearMap.one_apply, smul_eq_mul, one_mul, F']
+      one_apply_eq_self, smul_eq_mul, one_mul, F']
     rw [abs_of_nonneg (deriv_c x hx)]
   rw [this]
   exact lintegral_image_eq_lintegral_abs_det_fderiv_mul _ hc hf' inj_c _
@@ -257,7 +257,7 @@ theorem integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn (hs : Measu
   rw [integrableOn_image_iff_integrableOn_abs_det_fderiv_smul _ hc hF' inj_c]
   apply integrableOn_congr_fun (fun x hx ↦ ?_) hc
   simp only [LinearMap.det_ring, ContinuousLinearMap.coe_coe, ContinuousLinearMap.smulRight_apply,
-    ContinuousLinearMap.one_apply, smul_eq_mul, one_mul, F']
+    one_apply_eq_self, smul_eq_mul, one_mul, F']
   rw [abs_of_nonneg (deriv_c x hx)]
 
 /-- Change of variable formula for differentiable functions: if a real function `f` is
@@ -301,7 +301,7 @@ theorem integral_image_eq_integral_deriv_smul_of_monotoneOn (hs : MeasurableSet
   have : ∫ x in c, f' x • g (f x) = ∫ x in c, |(F' x).det| • g (f x) := by
     apply setIntegral_congr_fun hc (fun x hx ↦ ?_)
     simp only [LinearMap.det_ring, ContinuousLinearMap.coe_coe, ContinuousLinearMap.smulRight_apply,
-      ContinuousLinearMap.one_apply, smul_eq_mul, one_mul, F']
+      one_apply_eq_self, smul_eq_mul, one_mul, F']
     rw [abs_of_nonneg (deriv_c x hx)]
   rw [this]
   exact integral_image_eq_integral_abs_det_fderiv_smul _ hc hF' inj_c _
diff --git a/Mathlib/MeasureTheory/Group/Prod.lean b/Mathlib/MeasureTheory/Group/Prod.lean
index beebced4fd664b..50a52b5efd9f88 100644
--- a/Mathlib/MeasureTheory/Group/Prod.lean
+++ b/Mathlib/MeasureTheory/Group/Prod.lean
@@ -331,7 +331,7 @@ theorem measure_mul_measure_eq (s t : Set G) (h2s : ν' s ≠ 0) (h3s : ν' s 
 theorem measure_eq_div_smul (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ∞) :
     μ' = (μ' s / ν' s) • ν' := by
   ext1 t -
-  rw [smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm,
+  rw [Measure.smul_apply, smul_eq_mul, mul_comm, ← mul_div_assoc, mul_comm,
     measure_mul_measure_eq μ' ν' s t h2s h3s, mul_div_assoc, ENNReal.mul_div_cancel h2s h3s]
 
 end SigmaFinite
diff --git a/Mathlib/MeasureTheory/Integral/Bochner/L1.lean b/Mathlib/MeasureTheory/Integral/Bochner/L1.lean
index ae5a6642e25426..f11b2590553452 100644
--- a/Mathlib/MeasureTheory/Integral/Bochner/L1.lean
+++ b/Mathlib/MeasureTheory/Integral/Bochner/L1.lean
@@ -139,7 +139,7 @@ theorem dominatedFinMeasAdditive_weightedSMul {_ : MeasurableSpace α} (μ : Mea
 
 theorem weightedSMul_nonneg [PartialOrder F] [IsOrderedModule ℝ F]
     (s : Set α) (x : F) (hx : 0 ≤ x) : 0 ≤ weightedSMul μ s x := by
-  simp only [weightedSMul, coe_smul', _root_.id, coe_id', Pi.smul_apply]
+  simp only [weightedSMul, _root_.id, coe_id', smul_apply]
   exact smul_nonneg toReal_nonneg hx
 
 end WeightedSMul
diff --git a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
index e166b5c4873a81..d6a80a4a9e1495 100644
--- a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
+++ b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
@@ -307,8 +307,7 @@ theorem setToSimpleFunc_zero' {T : Set α → E →L[ℝ] F'}
   by_cases hx0 : x = 0
   · simp [hx0]
   rw [h_zero (f ⁻¹' ({x} : Set E)) (measurableSet_fiber _ _)
-      (measure_preimage_lt_top_of_integrable f hf hx0),
-    ContinuousLinearMap.zero_apply]
+      (measure_preimage_lt_top_of_integrable f hf hx0), zero_apply]
 
 @[simp]
 theorem setToSimpleFunc_zero_apply {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') :
@@ -349,7 +348,7 @@ theorem map_setToSimpleFunc (T : Set α → F →L[ℝ] F') (h_add : FinMeasAddi
     rw [← Finset.set_biUnion_preimage_singleton]
   rw [h_left_eq']
   rw [h_add.map_iUnion_fin_meas_set_eq_sum T T_empty]
-  · simp only [sum_apply, ContinuousLinearMap.coe_sum']
+  · simp only [_root_.sum_apply]
     refine Finset.sum_congr rfl fun x hx => ?_
     rw [mem_filter] at hx
     rw [hx.2]
@@ -374,7 +373,7 @@ theorem setToSimpleFunc_congr' (T : Set α → E →L[ℝ] F) (h_add : FinMeasAd
           congr; rw [pair_preimage_singleton f g]
         rw [h_eq]
         exact h eq
-      simp only [this, ContinuousLinearMap.zero_apply, pair_apply]
+      simp only [this, zero_apply, pair_apply]
 
 theorem setToSimpleFunc_congr (T : Set α → E →L[ℝ] F)
     (h_zero : ∀ s, MeasurableSet s → μ s = 0 → T s = 0) (h_add : FinMeasAdditive μ T) {f g : α →ₛ E}
@@ -422,7 +421,7 @@ theorem setToSimpleFunc_add_left' (T T' T'' : Set α → E →L[ℝ] F)
 
 theorem setToSimpleFunc_smul_left {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') (c : ℝ)
     (f : α →ₛ F) : setToSimpleFunc (fun s => c • T s) f = c • setToSimpleFunc T f := by
-  simp_rw [setToSimpleFunc, ContinuousLinearMap.smul_apply, smul_sum]
+  simp_rw [setToSimpleFunc, _root_.smul_apply, smul_sum]
 
 theorem setToSimpleFunc_smul_left' (T T' : Set α → E →L[ℝ] F') (c : ℝ)
     (h_smul : ∀ s, MeasurableSet s → μ s < ∞ → T' s = c • T s) {f : α →ₛ E} (hf : Integrable f μ) :
@@ -432,7 +431,7 @@ theorem setToSimpleFunc_smul_left' (T T' : Set α → E →L[ℝ] F') (c : ℝ)
   suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T' (f ⁻¹' {x}) = c • T (f ⁻¹' {x}) by
     rw [smul_sum]
     refine Finset.sum_congr rfl fun x hx => ?_
-    rw [this x hx, ContinuousLinearMap.smul_apply]
+    rw [this x hx, _root_.smul_apply]
   intro x hx
   refine
     h_smul (f ⁻¹' {x}) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)
@@ -591,7 +590,7 @@ theorem setToSimpleFunc_indicator (T : Set α → F →L[ℝ] F') (hT_empty : T
       T s x := by
   classical
   obtain rfl | hs_empty := s.eq_empty_or_nonempty
-  · simp only [hT_empty, ContinuousLinearMap.zero_apply, piecewise_empty, const_zero,
+  · simp only [hT_empty, zero_apply, piecewise_empty, const_zero,
       setToSimpleFunc_zero_apply]
   simp_rw [setToSimpleFunc]
   obtain rfl | hs_univ := eq_or_ne s univ
@@ -622,7 +621,7 @@ theorem setToSimpleFunc_const (T : Set α → F →L[ℝ] F') (hT_empty : T ∅
   cases isEmpty_or_nonempty α
   · have h_univ_empty : (univ : Set α) = ∅ := Subsingleton.elim _ _
     rw [h_univ_empty, hT_empty]
-    simp only [setToSimpleFunc, ContinuousLinearMap.zero_apply, sum_empty,
+    simp only [setToSimpleFunc, zero_apply, sum_empty,
       range_eq_empty_of_isEmpty]
   · exact setToSimpleFunc_const' T x
 
diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
index f722f7437a7020..0457eae6354324 100644
--- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
+++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean
@@ -863,7 +863,7 @@ open ContinuousLinearMap
 theorem _root_.ContinuousLinearMap.intervalIntegral_apply {a b : ℝ} {φ : ℝ → F →L[𝕜] E}
     (hφ : IntervalIntegrable φ μ a b) (v : F) :
     (∫ x in a..b, φ x ∂μ) v = ∫ x in a..b, φ x v ∂μ := by
-  simp_rw [intervalIntegral_eq_integral_uIoc, ← integral_apply hφ.def' v, coe_smul', Pi.smul_apply]
+  simp_rw [intervalIntegral_eq_integral_uIoc, ← integral_apply hφ.def' v, smul_apply]
 
 variable [NormedSpace ℝ F] [CompleteSpace F]
 
diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean b/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean
index 78c54ce1ae3810..c8c636f300febd 100644
--- a/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean
+++ b/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean
@@ -191,7 +191,7 @@ theorem exists_simpleFunc_forall_lintegral_sub_lt_of_pos {f : α → ℝ≥0∞}
   have : (map (↑) φ).lintegral μ ≠ ∞ := ne_top_of_le_ne_top h (by exact le_iSup₂ (α := ℝ≥0∞) φ hle)
   rw [← ENNReal.add_lt_add_iff_left this, ← add_lintegral, ← SimpleFunc.map_add @ENNReal.coe_add]
   refine (hb _ fun x => le_trans ?_ (max_le (hle x) (hψ x))).trans_lt hbφ
-  simp only [add_apply, sub_apply, add_tsub_eq_max]
+  simp only [SimpleFunc.add_apply, SimpleFunc.sub_apply, add_tsub_eq_max]
   rfl
 
 theorem iSup_lintegral_le {ι : Sort*} (f : ι → α → ℝ≥0∞) :
diff --git a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/Basic.lean b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/Basic.lean
index eadd8784b638d6..82478cadf73698 100644
--- a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/Basic.lean
+++ b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/Basic.lean
@@ -373,8 +373,7 @@ lemma charFun_toDual_symm_eq_charFunDual {E : Type*} [NormedAddCommGroup E] [Com
 lemma charFunDual_map [OpensMeasurableSpace E] [BorelSpace F] (L : E →L[ℝ] F)
     (L' : StrongDual ℝ F) : charFunDual (μ.map L) L' = charFunDual μ (L'.comp L) := by
   rw [charFunDual_eq_charFun_map_one, charFunDual_eq_charFun_map_one,
-    Measure.map_map (by fun_prop) (by fun_prop)]
-  simp
+    Measure.map_map (by fun_prop) (by fun_prop), ContinuousLinearMap.coe_comp]
 
 @[simp]
 lemma charFunDual_dirac [OpensMeasurableSpace E] {x : E} (L : StrongDual ℝ E) :
diff --git a/Mathlib/MeasureTheory/Measure/Haar/DistribChar.lean b/Mathlib/MeasureTheory/Measure/Haar/DistribChar.lean
index 72b1cb362675d5..643a8c3d7fbc2e 100644
--- a/Mathlib/MeasureTheory/Measure/Haar/DistribChar.lean
+++ b/Mathlib/MeasureTheory/Measure/Haar/DistribChar.lean
@@ -83,7 +83,7 @@ variable (μ) in
 lemma distribHaarChar_mul (g : G) (s : Set A) : distribHaarChar A g * μ s = μ (g • s) := by
   have : (DomMulAct.mk g • μ) s = μ (g • s) := by simp [domSMul_apply]
   rw [eq_comm, ← nnreal_smul_coe_apply, ← addHaarScalarFactor_smul_eq_distribHaarChar μ,
-    ← this, ← smul_apply, ← isAddLeftInvariant_eq_smul_of_regular]
+    ← this, ← Measure.smul_apply, ← isAddLeftInvariant_eq_smul_of_regular]
 
 lemma distribHaarChar_eq_div (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) (g : G) :
     distribHaarChar A g = μ (g • s) / μ s := by
diff --git a/Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.lean b/Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.lean
index a287be8e0de764..64aa4053868516 100644
--- a/Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.lean
+++ b/Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.lean
@@ -105,7 +105,7 @@ lemma mulEquivHaarChar_smul_preimage
     (μ : Measure G) [IsHaarMeasure μ] [Regular μ] {X : Set G} (φ : G ≃ₜ* G) :
     mulEquivHaarChar φ • μ (φ ⁻¹' X) = μ X := by
   nth_rw 2 [← mulEquivHaarChar_smul_map μ φ]
-  simp only [smul_apply, nnreal_smul_coe_apply]
+  simp only [Measure.smul_apply, nnreal_smul_coe_apply]
   exact congr_arg _ <| (MeasurableEquiv.map_apply φ.toMeasurableEquiv X).symm
 
 @[to_additive (attr := simp)]
diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean b/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean
index ffb8f914f33fb9..06d40c8578d4bf 100644
--- a/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean
+++ b/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean
@@ -104,7 +104,7 @@ instance isFiniteMeasureSMulNNReal [IsFiniteMeasure μ] {r : ℝ≥0} : IsFinite
 
 instance IsFiniteMeasure.average : IsFiniteMeasure ((μ univ)⁻¹ • μ) where
   measure_univ_lt_top := by
-    rw [smul_apply, smul_eq_mul, ← ENNReal.div_eq_inv_mul]
+    rw [Measure.smul_apply, smul_eq_mul, ← ENNReal.div_eq_inv_mul]
     exact ENNReal.div_self_le_one.trans_lt ENNReal.one_lt_top
 
 instance isFiniteMeasureSMulOfNNRealTower {R} [SMul R ℝ≥0] [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0 ℝ≥0∞]
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Decomposition/Hahn.lean b/Mathlib/MeasureTheory/VectorMeasure/Decomposition/Hahn.lean
index 892b8e9556e0a2..9f573b85b5ad99 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Decomposition/Hahn.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Decomposition/Hahn.lean
@@ -424,7 +424,7 @@ theorem of_symmDiff_compl_positive_negative {s : SignedMeasure α} {i j : Set α
         (hj'.1 (hi.compl.inter hj) Set.inter_subset_right),
       le_antisymm (hj'.2 (hj.compl.inter hi) Set.inter_subset_left)
         (hi'.1 (hj.compl.inter hi) Set.inter_subset_right),
-      zero_apply, zero_apply, zero_add]
+      VectorMeasure.zero_apply, VectorMeasure.zero_apply, zero_add]
     · exact
         Set.disjoint_of_subset_left Set.inter_subset_left
           (Set.disjoint_of_subset_right Set.inter_subset_right
@@ -437,7 +437,7 @@ theorem of_symmDiff_compl_positive_negative {s : SignedMeasure α} {i j : Set α
         (hj'.1 (hj.inter hi.compl) Set.inter_subset_left),
       le_antisymm (hj'.2 (hi.inter hj.compl) Set.inter_subset_right)
         (hi'.1 (hi.inter hj.compl) Set.inter_subset_left),
-      zero_apply, zero_apply, zero_add]
+      VectorMeasure.zero_apply, VectorMeasure.zero_apply, zero_add]
     · exact
         Set.disjoint_of_subset_left Set.inter_subset_left
           (Set.disjoint_of_subset_right Set.inter_subset_right
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Decomposition/Jordan.lean b/Mathlib/MeasureTheory/VectorMeasure/Decomposition/Jordan.lean
index a6a4b5e16dd34b..fb9ca2d234084b 100644
--- a/Mathlib/MeasureTheory/VectorMeasure/Decomposition/Jordan.lean
+++ b/Mathlib/MeasureTheory/VectorMeasure/Decomposition/Jordan.lean
@@ -156,7 +156,7 @@ theorem toSignedMeasure_zero : (0 : JordanDecomposition α).toSignedMeasure = 0
 
 theorem toSignedMeasure_neg : (-j).toSignedMeasure = -j.toSignedMeasure := by
   ext1 i hi
-  rw [neg_apply, toSignedMeasure, toSignedMeasure, toSignedMeasure_sub_apply hi,
+  rw [VectorMeasure.neg_apply, toSignedMeasure, toSignedMeasure, toSignedMeasure_sub_apply hi,
     toSignedMeasure_sub_apply hi, neg_sub, neg_posPart, neg_negPart]
 
 theorem toSignedMeasure_smul (r : ℝ≥0) : (r • j).toSignedMeasure = r • j.toSignedMeasure := by
@@ -177,7 +177,7 @@ theorem exists_compl_positive_negative :
   · refine restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => ?_
     rw [toSignedMeasure, toSignedMeasure_sub_apply hA, measureReal_def,
       show j.posPart A = 0 from nonpos_iff_eq_zero.1 (hS₂ ▸ measure_mono hA₁), ENNReal.toReal_zero,
-      zero_sub, neg_le, zero_apply, neg_zero]
+      zero_sub, neg_le, VectorMeasure.zero_apply, neg_zero]
     exact ENNReal.toReal_nonneg
   · refine restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => ?_
     rw [toSignedMeasure, toSignedMeasure_sub_apply hA, measureReal_def (μ := j.negPart),
@@ -277,7 +277,7 @@ theorem of_diff_eq_zero_of_symmDiff_eq_zero_positive (hu : MeasurableSet u) (hv
     rw [Set.symmDiff_def,
       of_union (v := s) (Set.disjoint_of_subset_left diff_subset disjoint_sdiff_self_right)
         (hu.diff hv) (hv.diff hu)] at hs
-    rw [zero_apply] at a b
+    rw [VectorMeasure.zero_apply] at a b
     constructor
   · linarith
   · linarith
diff --git a/Mathlib/NumberTheory/Modular.lean b/Mathlib/NumberTheory/Modular.lean
index 3c3c0964047d25..dbd0b531c022d9 100644
--- a/Mathlib/NumberTheory/Modular.lean
+++ b/Mathlib/NumberTheory/Modular.lean
@@ -107,7 +107,7 @@ section TendstoLemmas
 
 open Filter ContinuousLinearMap
 
-attribute [local simp] ContinuousLinearMap.coe_smul
+attribute [local simp] FunLike.coe_smul
 
 /-- The function `(c,d) → |cz+d|^2` is proper, that is, preimages of bounded-above sets are finite.
 -/
diff --git a/Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean b/Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
index 5bcc642f1bf5aa..cb84bd48eb6d08 100644
--- a/Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
+++ b/Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
@@ -291,8 +291,8 @@ theorem exists_Gamma_le_conj (g : GL (Fin 2) ℚ) (M : ℕ) [NeZero M] :
   rw [SetLike.mem_coe, CongruenceSubgroup.Gamma_mem', Subtype.ext_iff]
   ext i j
   simp_rw [map_apply_coe, z, map_add, map_one, RingHom.mapMatrix_apply, Int.coe_castRingHom,
-    add_apply, map_apply, coe_one, add_eq_left, Matrix.smul_apply, nsmul_eq_mul, Int.cast_mul,
-    Int.cast_natCast, ZMod.natCast_self M, zero_mul]
+    Matrix.add_apply, map_apply, coe_one, add_eq_left, Matrix.smul_apply, nsmul_eq_mul,
+    Int.cast_mul, Int.cast_natCast, ZMod.natCast_self M, zero_mul]
 
 /-- For any `g ∈ GL(2, ℚ)` and `M ≠ 0`, there exists `N` such that `g Γ(N) g⁻¹ ≤ Γ(M)`. -/
 theorem exists_Gamma_le_conj' (g : GL (Fin 2) ℚ) (M : ℕ) [NeZero M] :
diff --git a/Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean b/Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
index 8954b30ac0ee88..390947d240021d 100644
--- a/Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
+++ b/Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
@@ -182,8 +182,8 @@ lemma norm_jacobiTheta₂_term_fderiv_ge (n : ℤ) (z τ : ℂ) :
     refine (ContinuousLinearMap.le_opNorm _ _).trans ?_
     simp_rw [Prod.norm_def, norm_one, norm_zero, max_eq_right zero_le_one, mul_one, le_refl]
   refine le_trans ?_ this
-  simp_rw [jacobiTheta₂_term_fderiv, jacobiTheta₂_term, ContinuousLinearMap.coe_smul',
-    Pi.smul_apply, ContinuousLinearMap.add_apply, ContinuousLinearMap.coe_smul',
+  simp_rw [jacobiTheta₂_term_fderiv, jacobiTheta₂_term, FunLike.coe_smul',
+    Pi.smul_apply, add_apply, FunLike.coe_smul',
     ContinuousLinearMap.coe_fst', ContinuousLinearMap.coe_snd', Pi.smul_apply, smul_zero, zero_add,
     smul_eq_mul, mul_one, mul_comm _ ‖cexp _‖, norm_mul]
   refine mul_le_mul_of_nonneg_left (le_of_eq ?_) (norm_nonneg _)
@@ -340,14 +340,14 @@ lemma hasDerivAt_jacobiTheta₂_fst (z : ℂ) {τ : ℂ} (hτ : 0 < im τ) :
   -- through infinite sums of continuous linear maps.
   let eval_fst_CLM : (ℂ × ℂ →L[ℂ] ℂ) →L[ℂ] ℂ :=
   { toFun := fun f ↦ f (1, 0)
-    map_add' := by simp only [ContinuousLinearMap.add_apply, forall_const]
+    map_add' := by simp only [add_apply, forall_const]
     map_smul' := by simp }
   have step1 : HasSum (fun n ↦ (jacobiTheta₂_term_fderiv n z τ) (1, 0))
       ((jacobiTheta₂_fderiv z τ) (1, 0)) := by
     apply eval_fst_CLM.hasSum (hasSum_jacobiTheta₂_term_fderiv z hτ)
   have step2 (n : ℤ) : (jacobiTheta₂_term_fderiv n z τ) (1, 0) = jacobiTheta₂'_term n z τ := by
-    simp only [jacobiTheta₂_term_fderiv, smul_add, ContinuousLinearMap.add_apply,
-      ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_fst', Pi.smul_apply, smul_eq_mul,
+    simp only [jacobiTheta₂_term_fderiv, smul_add, add_apply,
+      FunLike.coe_smul', ContinuousLinearMap.coe_fst', Pi.smul_apply, smul_eq_mul,
       mul_one, ContinuousLinearMap.coe_snd', mul_zero, add_zero, jacobiTheta₂'_term,
       jacobiTheta₂_term, mul_comm _ (cexp _)]
   rw [funext step2] at step1
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
index 8f74b6be17d39e..b2a46262a4ce6e 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
@@ -604,15 +604,15 @@ theorem stdBasis_repr_eq_matrixToStdBasis_mul (x : (K →+* ℂ) → ℂ)
     rcases c with ⟨w, j⟩
     fin_cases j
     · simp only [Fin.zero_eta, Fin.isValue, stdBasis_apply_isComplex_fst, re_eq_add_conj,
-        mul_neg, fromBlocks_apply₂₁, zero_apply, zero_mul, sum_const_zero, fromBlocks_apply₂₂,
-        submatrix_apply, Prod.swap_prod_mk, blockDiagonal_apply, of_apply, cons_val', cons_val_zero,
-        empty_val', cons_val_fin_one, ite_mul, cons_val_one, sum_add_distrib, sum_ite_eq,
-        mem_univ, ↓reduceIte, ← hx (embedding w), zero_add]
+        mul_neg, fromBlocks_apply₂₁, Matrix.zero_apply, zero_mul, sum_const_zero,
+        fromBlocks_apply₂₂, submatrix_apply, Prod.swap_prod_mk, blockDiagonal_apply, of_apply,
+        cons_val', cons_val_zero, empty_val', cons_val_fin_one, ite_mul, cons_val_one,
+        sum_add_distrib, sum_ite_eq, mem_univ, ↓reduceIte, ← hx (embedding w), zero_add]
       ring
     · simp only [Fin.mk_one, Fin.isValue, stdBasis_apply_isComplex_snd, im_eq_sub_conj,
-        mul_neg, fromBlocks_apply₂₁, zero_apply, zero_mul, sum_const_zero, fromBlocks_apply₂₂,
-        submatrix_apply, Prod.swap_prod_mk, blockDiagonal_apply, of_apply, cons_val', cons_val_zero,
-        empty_val', cons_val_fin_one, cons_val_one, ite_mul, neg_mul,
+        mul_neg, fromBlocks_apply₂₁, Matrix.zero_apply, zero_mul, sum_const_zero,
+        fromBlocks_apply₂₂, submatrix_apply, Prod.swap_prod_mk, blockDiagonal_apply, of_apply,
+        cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_one, ite_mul, neg_mul,
         sum_add_distrib, sum_ite_eq, mem_univ, ↓reduceIte, ← hx (embedding w), zero_add]
       ring_nf; simp [field]
 
@@ -952,7 +952,7 @@ theorem negAt_symm :
   · by_cases hw : w ∈ s
     · simp_rw [negAt_apply_isReal_and_mem _ hw, negAt, prodCongr_symm,
         prodCongr_apply, piCongrRight_symm_apply, if_pos hw, symm_neg,
-        neg_apply]
+        ContinuousLinearEquiv.neg_apply]
     · simp_rw [negAt_apply_isReal_and_notMem _ hw, negAt, prodCongr_symm,
         prodCongr_apply, piCongrRight_symm_apply, if_neg hw, refl_symm,
         refl_apply]
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean
index c34f33f1728463..9e25017fbdc9b7 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean
@@ -542,10 +542,10 @@ theorem logMap_expMapBasis (x : realSpace K) :
   conv_lhs =>
     enter [2, 1, 2, w, 2, i]
     rw [if_neg i.prop]
-  simp_rw [sum_apply, ← sum_fn, map_sum, Pi.smul_apply, ← Pi.smul_def, map_smul,
+  simp_rw [Finset.sum_apply, ← sum_fn, map_sum, Pi.smul_apply, ← Pi.smul_def, map_smul,
     completeBasis_apply_of_ne, expMap_symm_apply, normAtAllPlaces_mixedEmbedding,
     ← logEmbedding_component, logEmbedding_fundSystem, Finsupp.coe_finsetSum, Finsupp.coe_smul,
-    sum_apply, Pi.smul_apply, Basis.ofZLatticeBasis_repr_apply, Basis.repr_self,
+    Finset.sum_apply, Pi.smul_apply, Basis.ofZLatticeBasis_repr_apply, Basis.repr_self,
     Finsupp.single_apply, EmbeddingLike.apply_eq_iff_eq, Int.cast_ite, Int.cast_one, Int.cast_zero,
     smul_ite, smul_eq_mul, mul_one, mul_zero, Fintype.sum_ite_eq']
 
@@ -588,9 +588,10 @@ theorem abs_det_fderiv_expMapBasis (x : realSpace K) :
       Real.exp (x w₀ * Module.finrank ℚ K) *
       (∏ w : {w // IsComplex w}, expMapBasis x w.1)⁻¹ * 2⁻¹ ^ nrComplexPlaces K *
         (Module.finrank ℚ K) * regulator K := by
-  simp_rw [fderiv_expMapBasis, det, coe_comp, LinearMap.det_comp, fderiv_expMap, coe_pi, coe_comp,
-    coe_proj, LinearMap.det_pi, LinearMap.det_ring, ContinuousLinearMap.coe_coe, smulRight_apply,
-    one_apply, one_smul, abs_mul, abs_det_completeBasis_equivFunL_symm, prod_deriv_expMap_single]
+  simp_rw [fderiv_expMapBasis, det, toLinearMap_comp, LinearMap.det_comp, fderiv_expMap, coe_pi,
+    toLinearMap_comp, coe_proj, LinearMap.det_pi, LinearMap.det_ring, ContinuousLinearMap.coe_coe,
+    smulRight_apply, one_apply_eq_self, one_smul, abs_mul, abs_det_completeBasis_equivFunL_symm,
+    prod_deriv_expMap_single]
   simp_rw [abs_mul, Real.exp_mul, abs_pow, Real.rpow_natCast, abs_of_nonneg (Real.exp_nonneg _),
     abs_inv, abs_prod, abs_of_nonneg (expMapBasis_nonneg _ _), Nat.abs_ofNat]
   ring
diff --git a/Mathlib/NumberTheory/Padics/PadicNumbers.lean b/Mathlib/NumberTheory/Padics/PadicNumbers.lean
index 4180568c0d733b..937a475b3d77ec 100644
--- a/Mathlib/NumberTheory/Padics/PadicNumbers.lean
+++ b/Mathlib/NumberTheory/Padics/PadicNumbers.lean
@@ -688,7 +688,7 @@ theorem rat_dense' (q : ℚ_[p]) {ε : ℚ} (hε : 0 < ε) : ∃ r : ℚ, padicN
         change padicNorm p (q' _ - q' _) < ε
         rcases Decidable.em (stationaryPoint hne' ≤ N) with hle | hle
         · have := (stationaryPoint_spec hne' le_rfl hle).symm
-          simp only [const_apply, sub_apply, padicNorm.zero, sub_self] at this
+          simp only [const_apply, CauSeq.sub_apply, padicNorm.zero, sub_self] at this
           simpa only [this]
         · exact hN _ (lt_of_not_ge hle).le _ le_rfl⟩
 
diff --git a/Mathlib/NumberTheory/SiegelsLemma.lean b/Mathlib/NumberTheory/SiegelsLemma.lean
index 0c8c8bc5b786d4..4e9706dd6411e9 100644
--- a/Mathlib/NumberTheory/SiegelsLemma.lean
+++ b/Mathlib/NumberTheory/SiegelsLemma.lean
@@ -126,7 +126,7 @@ lemma one_le_norm_A_of_ne_zero (hA : A ≠ 0) : 1 ≤ ‖A‖ := by
   by_contra! h
   apply hA
   ext i j
-  simp only [zero_apply]
+  simp only [Matrix.zero_apply]
   rw [norm_lt_iff Real.zero_lt_one] at h
   specialize h i j
   rw [Int.norm_eq_abs] at h
diff --git a/Mathlib/Probability/Distributions/Gaussian/Basic.lean b/Mathlib/Probability/Distributions/Gaussian/Basic.lean
index 19eef22c3763a6..3163c58577d9df 100644
--- a/Mathlib/Probability/Distributions/Gaussian/Basic.lean
+++ b/Mathlib/Probability/Distributions/Gaussian/Basic.lean
@@ -99,7 +99,7 @@ lemma isGaussian_map_of_measurable {E F : Type*} [TopologicalSpace E] [AddCommMo
     [Module ℝ F] {mF : MeasurableSpace F} [OpensMeasurableSpace F] {μ : Measure E}
     {L : E →L[ℝ] F} [IsGaussian μ] (hL : Measurable L) : IsGaussian (μ.map L) := by
   refine isGaussian_of_map_eq_gaussianReal fun L' ↦ ⟨μ[L' ∘L L], Var[L' ∘L L; μ].toNNReal, ?_⟩
-  rw [Measure.map_map (by fun_prop) hL, ← ContinuousLinearMap.coe_comp',
+  rw [Measure.map_map (by fun_prop) hL, ← ContinuousLinearMap.coe_comp,
     IsGaussian.map_eq_gaussianReal]
 
 variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
@@ -171,7 +171,7 @@ theorem isGaussian_iff_charFunDual_eq {μ : Measure E} [IsFiniteMeasure μ] :
   refine ⟨fun h ↦ h.charFunDual_eq, fun h ↦ ⟨fun L ↦ Measure.ext_of_charFun ?_⟩⟩
   ext u
   rw [charFun_map_eq_charFunDual_smul L u, h (u • L), charFun_gaussianReal]
-  simp only [ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_eq_mul, ofReal_mul,
+  simp only [FunLike.coe_smul', Pi.smul_apply, smul_eq_mul, ofReal_mul,
     Real.coe_toNNReal']
   congr
   · rw [integral_const_mul, integral_complex_ofReal]
diff --git a/Mathlib/Probability/Distributions/Gaussian/Fernique.lean b/Mathlib/Probability/Distributions/Gaussian/Fernique.lean
index f14bad7f0a10d5..f8e1985aea8a16 100644
--- a/Mathlib/Probability/Distributions/Gaussian/Fernique.lean
+++ b/Mathlib/Probability/Distributions/Gaussian/Fernique.lean
@@ -69,21 +69,21 @@ lemma map_rotation_eq_self_of_forall_strongDual_eq_zero
   have h1 : (L.comp (.rotation θ)).comp (.inl ℝ E E)
       = Real.cos θ • L.comp (.inl ℝ E E) - Real.sin θ • L.comp (.inr ℝ E E) := by
     ext x
-    simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.inl_apply,
+    simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.inl_apply,
       ContinuousLinearMap.rotation_apply, smul_zero, add_zero]
     rw [← L.comp_inl_add_comp_inr]
     simp [-neg_smul, sub_eq_add_neg]
   have h2 : (L.comp (.rotation θ)).comp (.inr ℝ E E)
       = Real.sin θ • L.comp (.inl ℝ E E) + Real.cos θ • L.comp (.inr ℝ E E) := by
     ext x
-    simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.inr_apply,
-      ContinuousLinearMap.rotation_apply, smul_zero, zero_add, ContinuousLinearMap.add_apply,
-      ContinuousLinearMap.coe_smul', Pi.smul_apply, ContinuousLinearMap.inl_apply, smul_eq_mul]
+    simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply,
+      ContinuousLinearMap.rotation_apply, smul_zero, zero_add, add_apply, smul_apply,
+      ContinuousLinearMap.inl_apply, smul_eq_mul]
     rw [← L.comp_inl_add_comp_inr]
     simp
   rw [h1, h2]
-  simp only [ContinuousLinearMap.coe_sub', ContinuousLinearMap.coe_smul',
-    ContinuousLinearMap.coe_add']
+  simp only [FunLike.coe_sub, FunLike.coe_smul,
+    FunLike.coe_add]
   rw [variance_sub, variance_smul, variance_add, variance_smul, variance_smul, covariance_smul_left,
     covariance_smul_right, variance_smul, covariance_smul_left, covariance_smul_right]
   · have h := Real.cos_sq_add_sin_sq θ
diff --git a/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean b/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean
index 1a72ec30538f0b..b205b06e591f1a 100644
--- a/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean
+++ b/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean
@@ -316,7 +316,7 @@ lemma HasGaussianLaw.indepFun_of_covariance_strongDual [NormedSpace ℝ E] [Norm
   rw [indepFun_iff_charFunDual_prod hXY.fst.aemeasurable hXY.snd.aemeasurable]
   intro L
   have : L ∘ (fun ω ↦ (X ω, Y ω)) = (L ∘L (.inl ℝ E F)) ∘ X + (L ∘L (.inr ℝ E F)) ∘ Y := by
-    ext; simp [-coe_comp', ← comp_inl_add_comp_inr]
+    ext; simp [-comp_apply, ← comp_inl_add_comp_inr]
   rw [hXY.charFunDual_map_eq, hXY.fst.charFunDual_map_eq, hXY.snd.charFunDual_map_eq, ← exp_add,
     sub_add_sub_comm, ← add_mul, ← ofReal_add, ← integral_add, ← add_div, ← ofReal_add, this,
     variance_add, h, mul_zero, add_zero]
diff --git a/Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Independence.lean b/Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Independence.lean
index dc1f3b1faed68a..7626ec184d7223 100644
--- a/Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Independence.lean
+++ b/Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Independence.lean
@@ -78,9 +78,9 @@ lemma iIndepFun_of_covariance_strongDual [NormedSpace ℝ E]
         map_smul' c x := by ext; simp }
     exact (hX.hasGaussianLaw _).map L
   have h1 : L₁ ∘ (fun ω k ↦ X i k ω) = ∑ k : J i, (L₁ ∘L .single ℝ _ k) ∘ X i k := by
-    ext; simp [-ContinuousLinearMap.coe_comp', ← L₁.sum_comp_single]
+    ext; simp [-ContinuousLinearMap.comp_apply, ← L₁.sum_comp_single]
   have h2 : L₂ ∘ (fun ω k ↦ X j k ω) = ∑ k : J j, (L₂ ∘L .single ℝ _ k) ∘ X j k := by
-    ext; simp [-ContinuousLinearMap.coe_comp', ← L₂.sum_comp_single]
+    ext; simp [-ContinuousLinearMap.comp_apply, ← L₂.sum_comp_single]
   rw [h1, h2, covariance_sum_sum]
   · exact sum_eq_zero fun _ _ ↦ sum_eq_zero fun _ _ ↦ h i j (by simpa) ..
   · exact fun k ↦ ((hX.hasGaussianLaw_eval ⟨i, k⟩).map _).memLp_two
@@ -133,9 +133,9 @@ lemma indepFun_of_covariance_strongDual [NormedSpace ℝ E]
     exact (hXY.hasGaussianLaw _).map L
   classical
   have h1 : L₁ ∘ (fun ω i ↦ X i ω) = ∑ i : I, (L₁ ∘L .single ℝ _ i) ∘ X i := by
-    ext; simp [-ContinuousLinearMap.coe_comp', ← L₁.sum_comp_single]
+    ext; simp [-ContinuousLinearMap.comp_apply, ← L₁.sum_comp_single]
   have h2 : L₂ ∘ (fun ω j ↦ Y j ω) = ∑ j : J, (L₂ ∘L .single ℝ _ j) ∘ Y j := by
-    ext; simp [-ContinuousLinearMap.coe_comp', ← L₂.sum_comp_single]
+    ext; simp [-ContinuousLinearMap.comp_apply, ← L₂.sum_comp_single]
   rw [h1, h2, covariance_sum_sum]
   · exact sum_eq_zero fun i _ ↦ sum_eq_zero fun j _ ↦ h ..
   · exact fun s ↦ ((hXY.hasGaussianLaw_eval (.inl s)).map _).memLp_two
diff --git a/Mathlib/Probability/Distributions/Uniform.lean b/Mathlib/Probability/Distributions/Uniform.lean
index 8b7c5c9ba316a5..ba27e336293991 100644
--- a/Mathlib/Probability/Distributions/Uniform.lean
+++ b/Mathlib/Probability/Distributions/Uniform.lean
@@ -73,7 +73,7 @@ theorem aemeasurable {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s 
   apply zero_ne_one' ℝ≥0∞
   calc
     0 = (0 : Measure E) Set.univ := rfl
-    _ = _ := by rw [hu, smul_apply, restrict_apply MeasurableSet.univ,
+    _ = _ := by rw [hu, Measure.smul_apply, restrict_apply MeasurableSet.univ,
       Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel hns hnt]
 
 theorem absolutelyContinuous {X : Ω → E} {s : Set E} (hu : IsUniform X s ℙ μ) : map X ℙ ≪ μ := by
diff --git a/Mathlib/Probability/Moments/Basic.lean b/Mathlib/Probability/Moments/Basic.lean
index 10d0eb984e7b5e..2941afd2786b9c 100644
--- a/Mathlib/Probability/Moments/Basic.lean
+++ b/Mathlib/Probability/Moments/Basic.lean
@@ -327,7 +327,7 @@ theorem aestronglyMeasurable_exp_mul_sum {X : ι → Ω → ℝ} {s : Finset ι}
   classical
   induction s using Finset.induction_on with
   | empty =>
-    simp only [sum_apply, sum_empty, mul_zero, exp_zero]
+    simp only [Finset.sum_apply, sum_empty, mul_zero, exp_zero]
     exact aestronglyMeasurable_const
   | insert i s hi_notin_s h_rec =>
     have : ∀ i : ι, i ∈ s → AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
@@ -350,7 +350,7 @@ theorem iIndepFun.integrable_exp_mul_sum [IsFiniteMeasure μ] {X : ι → Ω →
   classical
   induction s using Finset.induction_on with
   | empty =>
-    simp only [sum_apply, sum_empty, mul_zero, exp_zero]
+    simp only [Finset.sum_apply, sum_empty, mul_zero, exp_zero]
     exact integrable_const _
   | insert i s hi_notin_s h_rec =>
     have : ∀ i : ι, i ∈ s → Integrable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
diff --git a/Mathlib/Probability/Moments/Variance.lean b/Mathlib/Probability/Moments/Variance.lean
index fe52ac300a94a8..790187496a04c3 100644
--- a/Mathlib/Probability/Moments/Variance.lean
+++ b/Mathlib/Probability/Moments/Variance.lean
@@ -431,7 +431,7 @@ nonrec theorem IndepFun.variance_sum {ι : Type*} {X : ι → Ω → ℝ} {s : F
       simp [variance_congr (h'' i hi)]
     · have := fun (i : s) ↦ h'' i.1 i.2
       filter_upwards [ae_all_iff.2 this] with ω hω
-      simp only [sum_apply, Pi.zero_apply]
+      simp only [Finset.sum_apply, Pi.zero_apply]
       exact Finset.sum_eq_zero fun i hi ↦ hω ⟨i, hi⟩
   obtain ⟨j, hj1, hj2⟩ := not_forall₂.1 h''
   obtain rfl | h' := s.eq_singleton_or_nontrivial hj1
diff --git a/Mathlib/Probability/StrongLaw.lean b/Mathlib/Probability/StrongLaw.lean
index 561c5d9a9382c6..bd87fe5c9227cb 100644
--- a/Mathlib/Probability/StrongLaw.lean
+++ b/Mathlib/Probability/StrongLaw.lean
@@ -467,8 +467,8 @@ theorem strong_law_aux1 {c : ℝ} (c_one : 1 < c) {ε : ℝ} (εpos : 0 < ε) :
     (le_of_tendsto_of_tendsto' (ENNReal.tendsto_nat_tsum _) tendsto_const_nhds I3).trans_lt
       ENNReal.ofReal_lt_top
   filter_upwards [ae_eventually_notMem I4.ne] with ω hω
-  simp_rw [S, not_le, mul_comm, sum_apply] at hω
-  convert! hω; simp only [Y, u, sum_apply]
+  simp_rw [S, not_le, mul_comm, Finset.sum_apply] at hω
+  convert! hω; simp only [Y, u, Finset.sum_apply]
 
 include hint hindep hident hnonneg in
 /-- The truncation of `Xᵢ` up to `i` satisfies the strong law of large numbers
@@ -499,7 +499,7 @@ theorem strong_law_aux3 :
     exact (hident i).truncation.integral_eq
   convert! Asymptotics.isLittleO_sum_range_of_tendsto_zero (tendsto_sub_nhds_zero_iff.2 A) using 1
   ext1 n
-  simp only [sum_sub_distrib, sum_const, card_range, nsmul_eq_mul, sum_apply, sub_left_inj]
+  simp only [sum_sub_distrib, sum_const, card_range, nsmul_eq_mul, Finset.sum_apply, sub_left_inj]
   rw [integral_finsetSum _ fun i _ => ?_]
   exact ((hident i).symm.integrable_snd hint).1.integrable_truncation
 
@@ -863,7 +863,7 @@ theorem strong_law_Lp {p : ℝ≥0∞} (hp : 1 ≤ p) (hp' : p ≠ ∞) (X : ℕ
     apply uniformIntegrable_average hp
     exact MemLp.uniformIntegrable_of_identDistrib hp hp' hℒp hident
   · ext n ω
-    simp only [Pi.smul_apply, sum_apply]
+    simp only [Pi.smul_apply, Finset.sum_apply]
 
 end StrongLawLp
 
diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
index 367870bcb7e066..bbe7c8ee90e94e 100644
--- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
+++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
@@ -12,6 +12,8 @@ public import Mathlib.LinearAlgebra.Projection
 public import Mathlib.Topology.Algebra.ContinuousMonoidHom
 public import Mathlib.Topology.Algebra.IsUniformGroup.Defs
 public import Mathlib.Topology.Algebra.Module.Basic
+public import Mathlib.Data.FunLike.Module
+public import Mathlib.Data.FunLike.Ring
 
 /-!
 # Continuous linear maps
@@ -289,25 +291,25 @@ variable [DistribSMul T₂ M₂] [SMulCommClass R₂ T₂ M₂] [ContinuousConst
 instance instSMul : SMul S₂ (M₁ →SL[σ₁₂] M₂) where
   smul c f := ⟨c • (f : M₁ →ₛₗ[σ₁₂] M₂), (f.2.const_smul _ : Continuous fun x => c • f x)⟩
 
-theorem smul_apply (c : S₂) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) : (c • f) x = c • f x :=
-  rfl
+instance : IsSMulApply S₂ (M₁ →SL[σ₁₂] M₂) M₁ M₂ where
+  smul_apply _ _ _ := rfl
 
 @[simp, norm_cast]
-theorem coe_smul (c : S₂) (f : M₁ →SL[σ₁₂] M₂) :
+theorem toLinearMap_smul (c : S₂) (f : M₁ →SL[σ₁₂] M₂) :
     ↑(c • f) = c • (f : M₁ →ₛₗ[σ₁₂] M₂) :=
   rfl
 
-@[simp, norm_cast]
-theorem coe_smul' (c : S₂) (f : M₁ →SL[σ₁₂] M₂) :
-    ↑(c • f) = c • (f : M₁ → M₂) :=
-  rfl
+@[deprecated (since := "2026-05-20")] protected alias smul_apply := _root_.smul_apply
+
+@[deprecated (since := "2026-05-20")] protected alias coe_smul := toLinearMap_smul
+
+@[deprecated (since := "2026-05-20")] alias coe_smul' := FunLike.coe_smul
 
 instance isScalarTower [SMul S₂ T₂] [IsScalarTower S₂ T₂ M₂] :
-    IsScalarTower S₂ T₂ (M₁ →SL[σ₁₂] M₂) :=
-  ⟨fun a b f => ext fun x => smul_assoc a b (f x)⟩
+    IsScalarTower S₂ T₂ (M₁ →SL[σ₁₂] M₂) := FunLike.isScalarTower
 
 instance smulCommClass [SMulCommClass S₂ T₂ M₂] : SMulCommClass S₂ T₂ (M₁ →SL[σ₁₂] M₂) :=
-  ⟨fun a b f => ext fun x => smul_comm a b (f x)⟩
+  FunLike.smulCommClass
 
 end SMul
 
@@ -316,9 +318,7 @@ section SMulMonoid
 variable {S₂ : Type*} [Monoid S₂]
 variable [DistribMulAction S₂ M₂] [SMulCommClass R₂ S₂ M₂] [ContinuousConstSMul S₂ M₂]
 
-instance mulAction : MulAction S₂ (M₁ →SL[σ₁₂] M₂) where
-  one_smul _f := ext fun _x => one_smul _ _
-  mul_smul _a _b _f := ext fun _x => mul_smul _ _ _
+instance mulAction : MulAction S₂ (M₁ →SL[σ₁₂] M₂) := fast_instance% FunLike.mulAction
 
 end SMulMonoid
 
@@ -326,6 +326,9 @@ end SMulMonoid
 instance zero : Zero (M₁ →SL[σ₁₂] M₂) :=
   ⟨⟨0, continuous_zero⟩⟩
 
+instance : IsZeroApply (M₁ →SL[σ₁₂] M₂) M₁ M₂ where
+  zero_apply _ := rfl
+
 instance inhabited : Inhabited (M₁ →SL[σ₁₂] M₂) :=
   ⟨0⟩
 
@@ -333,20 +336,15 @@ instance inhabited : Inhabited (M₁ →SL[σ₁₂] M₂) :=
 theorem default_def : (default : M₁ →SL[σ₁₂] M₂) = 0 :=
   rfl
 
-@[simp]
-theorem zero_apply (x : M₁) : (0 : M₁ →SL[σ₁₂] M₂) x = 0 :=
-  rfl
-
 @[simp, norm_cast]
-theorem coe_zero : ((0 : M₁ →SL[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂) = 0 :=
+theorem toLinearMap_zero : ((0 : M₁ →SL[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂) = 0 :=
   rfl
 
-/- no simp attribute on the next line as simp does not always simplify `0 x` to `0`
-when `0` is the zero function, while it does for the zero continuous linear map,
-and this is the most important property we care about. -/
-@[norm_cast]
-theorem coe_zero' : ⇑(0 : M₁ →SL[σ₁₂] M₂) = 0 :=
-  rfl
+@[deprecated (since := "2026-05-20")] protected alias zero_apply := _root_.zero_apply
+
+@[deprecated (since := "2026-05-20")] protected alias coe_zero := toLinearMap_zero
+
+@[deprecated (since := "2026-05-20")] alias coe_zero' := FunLike.coe_zero
 
 @[simp, norm_cast]
 theorem toContinuousAddMonoidHom_zero :
@@ -377,6 +375,10 @@ instance one : One (M₁ →L[R₁] M₁) :=
 
 theorem one_def : (1 : M₁ →L[R₁] M₁) = .id R₁ M₁ := rfl
 
+instance instIsOneApply : IsOneApplyEqSelf (M₁ →L[R₁] M₁) M₁ where
+  one_apply_eq_self _ := rfl
+
+@[simp]
 theorem id_apply (x : M₁) : ContinuousLinearMap.id R₁ M₁ x = x := rfl
 
 @[simp, norm_cast]
@@ -388,9 +390,11 @@ theorem coe_id' : ⇑(ContinuousLinearMap.id R₁ M₁) = id :=
   rfl
 
 @[simp, norm_cast]
-theorem coe_one : ((1 : M₁ →L[R₁] M₁) : M₁ →ₗ[R₁] M₁) = 1 :=
+theorem toLinearMap_one : ((1 : M₁ →L[R₁] M₁) : M₁ →ₗ[R₁] M₁) = 1 :=
   rfl
 
+@[deprecated (since := "2026-05-20")] protected alias coe_one := toLinearMap_one
+
 @[simp] lemma mk_id : mk (.id : M₁ →ₗ[R₁] M₁) continuous_id = .id _ _ := rfl
 @[simp] lemma mk_one : mk (1 : M₁ →ₗ[R₁] M₁) continuous_id = 1 := rfl
 
@@ -402,7 +406,7 @@ theorem toContinuousAddMonoidHom_id :
 theorem coe_eq_id {f : M₁ →L[R₁] M₁} : (f : M₁ →ₗ[R₁] M₁) = LinearMap.id ↔ f = .id _ _ := by
   rw [← coe_id, coe_inj]
 
-@[simp] theorem one_apply (x : M₁) : (1 : M₁ →L[R₁] M₁) x = x := rfl
+@[deprecated (since := "2026-05-20")] protected alias one_apply := one_apply_eq_self
 
 instance [Nontrivial M₁] : Nontrivial (M₁ →L[R₁] M₁) :=
   ⟨0, 1, fun e ↦
@@ -415,17 +419,18 @@ variable [ContinuousAdd M₂]
 instance add : Add (M₁ →SL[σ₁₂] M₂) :=
   ⟨fun f g => ⟨f + g, f.2.add g.2⟩⟩
 
-@[simp]
-theorem add_apply (f g : M₁ →SL[σ₁₂] M₂) (x : M₁) : (f + g) x = f x + g x :=
-  rfl
+instance instIsAddApply : IsAddApply (M₁ →SL[σ₁₂] M₂) M₁ M₂ where
+  add_apply _ _ _ := rfl
 
 @[simp, norm_cast]
-theorem coe_add (f g : M₁ →SL[σ₁₂] M₂) : (↑(f + g) : M₁ →ₛₗ[σ₁₂] M₂) = f + g :=
+theorem toLinearMap_add (f g : M₁ →SL[σ₁₂] M₂) : (↑(f + g) : M₁ →ₛₗ[σ₁₂] M₂) = f + g :=
   rfl
 
-@[norm_cast]
-theorem coe_add' (f g : M₁ →SL[σ₁₂] M₂) : ⇑(f + g) = f + g :=
-  rfl
+@[deprecated (since := "2026-05-20")] protected alias add_apply := _root_.add_apply
+
+@[deprecated (since := "2026-05-20")] protected alias coe_add := toLinearMap_add
+
+@[deprecated (since := "2026-05-20")] alias coe_add' := FunLike.coe_add
 
 @[simp, norm_cast]
 theorem toContinuousAddMonoidHom_add (f g : M₁ →SL[σ₁₂] M₂) :
@@ -453,23 +458,18 @@ instance : AddMonoid (M₁ →SL[σ₁₂] M₂) where
     ext
     simp [add_smul]
 
-instance addCommMonoid : AddCommMonoid (M₁ →SL[σ₁₂] M₂) where
-  add_comm := by
-    intros
-    ext
-    apply_rules [zero_add, add_assoc, add_zero, neg_add_cancel, add_comm]
+instance addCommMonoid : AddCommMonoid (M₁ →SL[σ₁₂] M₂) := fast_instance% FunLike.addCommMonoid
 
 @[simp, norm_cast]
-theorem coe_sum {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) :
+theorem toLinearMap_sum {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) :
     ↑(∑ d ∈ t, f d) = (∑ d ∈ t, f d : M₁ →ₛₗ[σ₁₂] M₂) :=
   map_sum (AddMonoidHom.mk ⟨((↑) : (M₁ →SL[σ₁₂] M₂) → M₁ →ₛₗ[σ₁₂] M₂), rfl⟩ fun _ _ => rfl) _ _
 
-@[simp, norm_cast]
-theorem coe_sum' {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) :
-    ⇑(∑ d ∈ t, f d) = ∑ d ∈ t, ⇑(f d) := by simp only [← coe_coe, coe_sum, LinearMap.coe_sum]
+@[deprecated (since := "2026-05-20")] protected alias sum_apply := _root_.sum_apply
+
+@[deprecated (since := "2026-05-20")] protected alias coe_sum := toLinearMap_sum
 
-theorem sum_apply {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) (b : M₁) :
-    (∑ d ∈ t, f d) b = ∑ d ∈ t, f d b := by simp only [coe_sum', Finset.sum_apply]
+@[deprecated (since := "2026-05-20")] alias coe_sum' := FunLike.coe_sum
 
 end Add
 
@@ -489,18 +489,21 @@ infixr:90 " ∘SL " =>
   ContinuousLinearMap.comp
 
 @[simp, norm_cast]
-theorem coe_comp (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
+theorem toLinearMap_comp (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
     (h ∘SL f : M₁ →ₛₗ[σ₁₃] M₃) = (h : M₂ →ₛₗ[σ₂₃] M₃) ∘ₛₗ (f : M₁ →ₛₗ[σ₁₂] M₂) :=
   rfl
 
-@[simp, norm_cast]
-theorem coe_comp' (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) : ⇑(h ∘SL f) = h ∘ f :=
+@[norm_cast]
+theorem coe_comp (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) : ⇑(h ∘SL f) = h ∘ f :=
   rfl
 
+@[deprecated (since := "2026-05-20")] alias coe_comp' := coe_comp
+
 @[simp, norm_cast]
 theorem toContinuousAddMonoidHom_comp (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
     (↑(h ∘SL f) : ContinuousAddMonoidHom M₁ M₃) = (h : ContinuousAddMonoidHom M₂ M₃).comp f := rfl
 
+@[simp, grind =]
 theorem comp_apply (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) : (g ∘SL f) x = g (f x) :=
   rfl
 
@@ -521,7 +524,7 @@ variable {R E F : Type*} [Semiring R]
 /-- `g ∘ f = id` as `ContinuousLinearMap`s implies `g ∘ f = id` as functions. -/
 lemma leftInverse_of_comp {f : E →L[R] F} {g : F →L[R] E}
     (hinv : g ∘L f = .id R E) : Function.LeftInverse g f := by
-  simpa [← Function.rightInverse_iff_comp] using! congr(⇑$hinv)
+  simpa [coe_comp, ← Function.leftInverse_iff_comp] using congr(⇑$hinv)
 
 /-- `f ∘ g = id` as `ContinuousLinearMap`s implies `f ∘ g = id` as functions. -/
 lemma rightInverse_of_comp {f : E →L[R] F} {g : F →L[R] E}
@@ -564,7 +567,7 @@ theorem finsetSum_comp {ι : Type*} {s : Finset ι}
     [ContinuousAdd M₃] (g : ι → M₂ →SL[σ₂₃] M₃)
     (f : M₁ →SL[σ₁₂] M₂) : (∑ i ∈ s, g i) ∘SL f = ∑ i ∈ s, (g i) ∘SL f := by
   ext
-  simp only [coe_comp', coe_sum', Function.comp_apply, Finset.sum_apply]
+  simp only [comp_apply, sum_apply]
 
 @[deprecated (since := "2026-04-08")] alias finset_sum_comp := finsetSum_comp
 
@@ -586,26 +589,24 @@ lemma cancel_left' {g : M₂ →SL[σ₂₃] M₃} {f₁ f₂ : M₁ →SL[σ₁
 instance instMul : Mul (M₁ →L[R₁] M₁) :=
   ⟨comp⟩
 
+instance : IsMulApplyEqComp (M₁ →L[R₁] M₁) M₁ where
+  mul_apply_eq_comp _ _ _ := rfl
+
 theorem mul_def (f g : M₁ →L[R₁] M₁) : f * g = f ∘L g :=
   rfl
 
 @[simp, norm_cast]
-theorem coe_mul (f g : M₁ →L[R₁] M₁) : (↑(f * g) : M₁ →ₗ[R₁] M₁) = f * g :=
+theorem toLinearMap_mul (f g : M₁ →L[R₁] M₁) : (↑(f * g) : M₁ →ₗ[R₁] M₁) = f * g :=
   rfl
 
-@[simp, norm_cast]
-theorem coe_mul' (f g : M₁ →L[R₁] M₁) : ⇑(f * g) = f ∘ g :=
-  rfl
+@[deprecated (since := "2026-05-20")] alias coe_mul := toLinearMap_mul
 
-theorem mul_apply (f g : M₁ →L[R₁] M₁) (x : M₁) : (f * g) x = f (g x) :=
-  rfl
+@[deprecated (since := "2026-05-20")] protected alias coe_mul' := FunLike.coe_mul
 
-instance monoidWithZero : MonoidWithZero (M₁ →L[R₁] M₁) where
-  mul_zero f := ext fun _ => map_zero f
-  zero_mul _ := ext fun _ => rfl
-  mul_one _ := ext fun _ => rfl
-  one_mul _ := ext fun _ => rfl
-  mul_assoc _ _ _ := ext fun _ => rfl
+@[deprecated (since := "2026-05-20")] protected alias mul_apply := mul_apply_eq_comp
+
+instance monoidWithZero : MonoidWithZero (M₁ →L[R₁] M₁) :=
+  fast_instance% FunLike.monoidWithZero
 
 @[simp, norm_cast]
 theorem coe_pow' (f : M₁ →L[R₁] M₁) (n : ℕ) : ⇑(f ^ n) = f^[n] :=
@@ -618,14 +619,11 @@ theorem coe_pow (f : M₁ →L[R₁] M₁) (n : ℕ) : (↑(f ^ n) : M₁ →ₗ
 instance instNatCast [ContinuousAdd M₁] : NatCast (M₁ →L[R₁] M₁) where
   natCast n := n • (1 : M₁ →L[R₁] M₁)
 
-instance semiring [ContinuousAdd M₁] : Semiring (M₁ →L[R₁] M₁) where
-  __ := ContinuousLinearMap.monoidWithZero
-  __ := ContinuousLinearMap.addCommMonoid
-  left_distrib f g h := ext fun x => map_add f (g x) (h x)
-  right_distrib _ _ _ := ext fun _ => LinearMap.add_apply _ _ _
-  toNatCast := instNatCast
-  natCast_zero := zero_smul ℕ (1 : M₁ →L[R₁] M₁)
-  natCast_succ n := AddMonoid.nsmul_succ n (1 : M₁ →L[R₁] M₁)
+instance instIsNatCastApply [ContinuousAdd M₁] : IsNatCastApply (M₁ →L[R₁] M₁) M₁ where
+  natCast_apply _ _ := rfl
+
+instance semiring [ContinuousAdd M₁] : Semiring (M₁ →L[R₁] M₁) :=
+  fast_instance% FunLike.semiring
 
 /-- `ContinuousLinearMap.toLinearMap` as a `RingHom`. -/
 @[simps]
@@ -650,8 +648,8 @@ theorem ofNat_apply [ContinuousAdd M₁] (n : ℕ) [n.AtLeastTwo] (m : M₁) :
 def homeomorphOfUnit (T : (M₁ →L[R₁] M₁)ˣ) : M₁ ≃ₜ M₁ where
   toFun := T.1
   invFun := T⁻¹.1
-  left_inv x := by rw [← mul_apply, Units.inv_mul, one_apply]
-  right_inv x := by rw [← mul_apply, Units.mul_inv, one_apply]
+  left_inv x := by rw [← mul_apply_eq_comp, Units.inv_mul, one_apply_eq_self]
+  right_inv x := by rw [← mul_apply_eq_comp, Units.mul_inv, one_apply_eq_self]
 
 theorem isHomeomorph_of_isUnit {T : M₁ →L[R₁] M₁} (hT : IsUnit T) : IsHomeomorph T := by
   obtain ⟨T, rfl⟩ := hT
@@ -743,7 +741,7 @@ theorem smulRight_comp_smulRight {M₃ : Type*} [AddCommMonoid M₃] [Module R
 theorem range_smulRight_apply {R : Type*} [DivisionSemiring R] [Module R M₁] [Module R M₂]
     [TopologicalSpace R] [ContinuousSMul R M₂] {f : M₁ →L[R] R} (hf : f ≠ 0) (x : M₂) :
     range (f.smulRight x : M₁ →ₗ[R] M₂) = Submodule.span R {x} :=
-  LinearMap.range_smulRight_apply (by simpa [coe_inj, ← coe_zero] using hf) x
+  LinearMap.range_smulRight_apply (by simpa [coe_inj, ← toLinearMap_zero] using hf) x
 
 section ToSpanSingleton
 
@@ -850,17 +848,18 @@ variable [IsTopologicalAddGroup M₂]
 instance neg : Neg (M →SL[σ₁₂] M₂) :=
   ⟨fun f => ⟨-f, f.2.neg⟩⟩
 
-@[simp]
-theorem neg_apply (f : M →SL[σ₁₂] M₂) (x : M) : (-f) x = -f x :=
-  rfl
+instance : IsNegApply (M →SL[σ₁₂] M₂) M M₂ where
+  neg_apply _ _ := rfl
 
 @[simp, norm_cast]
-theorem coe_neg (f : M →SL[σ₁₂] M₂) : (↑(-f) : M →ₛₗ[σ₁₂] M₂) = -f :=
+theorem toLinearMap_neg (f : M →SL[σ₁₂] M₂) : (↑(-f) : M →ₛₗ[σ₁₂] M₂) = -f :=
   rfl
 
-@[norm_cast]
-theorem coe_neg' (f : M →SL[σ₁₂] M₂) : ⇑(-f) = -f :=
-  rfl
+@[deprecated (since := "2026-05-20")] protected alias neg_apply := _root_.neg_apply
+
+@[deprecated (since := "2026-05-20")] protected alias coe_neg := toLinearMap_neg
+
+@[deprecated (since := "2026-05-20")] alias coe_neg' := FunLike.coe_neg
 
 @[simp, norm_cast]
 theorem toContinuousAddMonoidHom_neg (f : M →SL[σ₁₂] M₂) :
@@ -869,6 +868,10 @@ theorem toContinuousAddMonoidHom_neg (f : M →SL[σ₁₂] M₂) :
 instance sub : Sub (M →SL[σ₁₂] M₂) :=
   ⟨fun f g => ⟨f - g, f.2.sub g.2⟩⟩
 
+instance : IsSubApply (M →SL[σ₁₂] M₂) M M₂ where
+  sub_apply _ _ _ := rfl
+
+-- Todo: figure out how to use `FunLike.addCommGroup` here
 instance addCommGroup : AddCommGroup (M →SL[σ₁₂] M₂) where
   sub_eq_add_neg _ _ := by ext; apply sub_eq_add_neg
   zsmul := (· • ·)
@@ -877,16 +880,15 @@ instance addCommGroup : AddCommGroup (M →SL[σ₁₂] M₂) where
   zsmul_neg' n f := by ext; simp [add_smul]
   neg_add_cancel _ := by ext; apply neg_add_cancel
 
-theorem sub_apply (f g : M →SL[σ₁₂] M₂) (x : M) : (f - g) x = f x - g x :=
-  rfl
-
 @[simp, norm_cast]
-theorem coe_sub (f g : M →SL[σ₁₂] M₂) : (↑(f - g) : M →ₛₗ[σ₁₂] M₂) = f - g :=
+theorem toLinearMap_sub (f g : M →SL[σ₁₂] M₂) : (↑(f - g) : M →ₛₗ[σ₁₂] M₂) = f - g :=
   rfl
 
-@[simp, norm_cast]
-theorem coe_sub' (f g : M →SL[σ₁₂] M₂) : ⇑(f - g) = f - g :=
-  rfl
+@[deprecated (since := "2026-05-20")] protected alias sub_apply := _root_.sub_apply
+
+@[deprecated (since := "2026-05-20")] protected alias coe_sub := toLinearMap_sub
+
+@[deprecated (since := "2026-05-20")] alias coe_sub' := FunLike.coe_sub
 
 @[simp, norm_cast]
 theorem toContinuousAddMonoidHom_sub (f g : M →SL[σ₁₂] M₂) :
@@ -920,16 +922,15 @@ theorem sub_comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAd
   ext
   simp
 
-instance ring [IsTopologicalAddGroup M] : Ring (M →L[R] M) where
-  __ := ContinuousLinearMap.semiring
-  __ := ContinuousLinearMap.addCommGroup
+instance [IsTopologicalAddGroup M] : IntCast (M →L[R] M) where
   intCast z := z • (1 : M →L[R] M)
-  intCast_ofNat := natCast_zsmul _
-  intCast_negSucc := negSucc_zsmul _
 
-@[simp]
-theorem intCast_apply [IsTopologicalAddGroup M] (z : ℤ) (m : M) : (↑z : M →L[R] M) m = z • m :=
-  rfl
+instance instIsIntCastApply [IsTopologicalAddGroup M] : IsIntCastApply (M →L[R] M) M where
+  intCast_apply _ _ := rfl
+
+@[deprecated (since := "2026-05-20")] alias intCast_apply := _root_.intCast_apply
+
+instance ring [IsTopologicalAddGroup M] : Ring (M →L[R] M) := fast_instance% FunLike.ring
 
 theorem toSpanSingleton_pow [TopologicalSpace R] [IsTopologicalRing R] (c : R) (n : ℕ) :
     toSpanSingleton R c ^ n = toSpanSingleton R (c ^ n) := by
@@ -988,11 +989,10 @@ theorem comp_smulₛₗ [SMulCommClass R₂ R₂ M₂] [SMulCommClass R₃ R₃
     [ContinuousConstSMul R₃ M₃] (h : M₂ →SL[σ₂₃] M₃) (c : R₂) (f : M →SL[σ₁₂] M₂) :
     h ∘SL (c • f) = σ₂₃ c • h ∘SL f := by
   ext x
-  simp only [coe_smul', coe_comp', Function.comp_apply, Pi.smul_apply, map_smulₛₗ]
+  simp
 
-instance distribMulAction [ContinuousAdd M₂] : DistribMulAction S₃ (M →SL[σ₁₂] M₂) where
-  smul_add a f g := ext fun x => smul_add a (f x) (g x)
-  smul_zero a := ext fun _ => smul_zero a
+instance distribMulAction [ContinuousAdd M₂] : DistribMulAction S₃ (M →SL[σ₁₂] M₂) :=
+  fast_instance% FunLike.distribMulAction
 
 end SMulMonoid
 
@@ -1011,13 +1011,10 @@ variable {R R₂ R₃ S S₃ : Type*} [Semiring R] [Semiring R₂] [Semiring R
 
 variable [ContinuousAdd M₂] [ContinuousAdd M₃] [ContinuousAdd N₂]
 
-instance module : Module S₃ (M →SL[σ₁₃] M₃) where
-  zero_smul _ := ext fun _ => zero_smul S₃ _
-  add_smul _ _ _ := ext fun _ => add_smul _ _ _
+instance module : Module S₃ (M →SL[σ₁₃] M₃) := fast_instance% FunLike.module
 
 instance isCentralScalar [Module S₃ᵐᵒᵖ M₃] [IsCentralScalar S₃ M₃] :
-    IsCentralScalar S₃ (M →SL[σ₁₃] M₃) where
-  op_smul_eq_smul _ _ := ext fun _ => op_smul_eq_smul _ _
+    IsCentralScalar S₃ (M →SL[σ₁₃] M₃) := FunLike.isCentralScalar
 
 variable (S) [ContinuousAdd N₃]
 
@@ -1025,8 +1022,8 @@ variable (S) [ContinuousAdd N₃]
 @[simps]
 def coeLM : (M →L[R] N₃) →ₗ[S] M →ₗ[R] N₃ where
   toFun := (↑)
-  map_add' f g := coe_add f g
-  map_smul' c f := coe_smul c f
+  map_add' f g := toLinearMap_add f g
+  map_smul' c f := toLinearMap_smul c f
 
 variable {S} (σ₁₃)
 
@@ -1034,8 +1031,8 @@ variable {S} (σ₁₃)
 @[simps]
 def coeLMₛₗ : (M →SL[σ₁₃] M₃) →ₗ[S₃] M →ₛₗ[σ₁₃] M₃ where
   toFun := (↑)
-  map_add' f g := coe_add f g
-  map_smul' c f := coe_smul c f
+  map_add' f g := toLinearMap_add f g
+  map_smul' c f := toLinearMap_smul c f
 
 end SMul
 
diff --git a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean
index 68b7f98c714583..75747bacd25b97 100644
--- a/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean
+++ b/Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Idempotent.lean
@@ -37,7 +37,7 @@ namespace ContinuousLinearMap
 theorem isIdempotentElem_toLinearMap_iff {R M : Type*} [Semiring R] [TopologicalSpace M]
     [AddCommMonoid M] [Module R M] {f : M →L[R] M} :
     IsIdempotentElem f.toLinearMap ↔ IsIdempotentElem f := by
-  simp only [IsIdempotentElem, Module.End.mul_eq_comp, ← coe_comp, mul_def, coe_inj]
+  simp only [IsIdempotentElem, Module.End.mul_eq_comp, ← toLinearMap_comp, mul_def, coe_inj]
 
 alias ⟨_, IsIdempotentElem.toLinearMap⟩ := isIdempotentElem_toLinearMap_iff
 
@@ -60,7 +60,7 @@ for idempotent `f`. -/
 lemma range_mem_invtSubmodule_iff {f T : M →L[R] M}
     (hf : IsIdempotentElem f) :
     f.range ∈ Module.End.invtSubmodule T ↔ f ∘L T ∘L f = T ∘L f := by
-  simpa [← ContinuousLinearMap.coe_comp] using
+  simpa [← toLinearMap_comp] using
     LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff (T := T) hf.toLinearMap
 
 alias ⟨conj_eq_of_range_mem_invtSubmodule,
@@ -71,7 +71,7 @@ for idempotent `f`. -/
 lemma ker_mem_invtSubmodule_iff {f T : M →L[R] M}
     (hf : IsIdempotentElem f) :
     f.ker ∈ Module.End.invtSubmodule T ↔ f ∘L T ∘L f = f ∘L T := by
-  simpa [← ContinuousLinearMap.coe_comp] using
+  simpa [← toLinearMap_comp] using
     LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff (T := T) hf.toLinearMap
 
 alias ⟨conj_eq_of_ker_mem_invtSubmodule,
@@ -82,7 +82,7 @@ both `range f` and `ker f` are invariant under `T`. -/
 lemma commute_iff {f T : M →L[R] M}
     (hf : IsIdempotentElem f) :
     Commute f T ↔ (f.range ∈ Module.End.invtSubmodule T ∧ f.ker ∈ Module.End.invtSubmodule T) := by
-  simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← coe_comp] using!
+  simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← toLinearMap_comp] using!
     LinearMap.IsIdempotentElem.commute_iff (T := T) hf.toLinearMap
 
 variable [IsTopologicalAddGroup M]
@@ -94,7 +94,7 @@ theorem commute_iff_of_isUnit {f T : M →L[R] M} (hT : IsUnit T)
     Commute f T ↔ f.range.map (T : M →ₗ[R] M) = f.range ∧ f.ker.map (T : M →ₗ[R] M) = f.ker := by
   have := hT.map ContinuousLinearMap.toLinearMapRingHom
   lift T to (M →L[R] M)ˣ using hT
-  simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← ContinuousLinearMap.coe_comp] using!
+  simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← toLinearMap_comp] using!
     LinearMap.IsIdempotentElem.commute_iff_of_isUnit this hf.toLinearMap
 
 @[deprecated (since := "2025-12-27")] alias range_eq_ker :=
diff --git a/Mathlib/Topology/Algebra/Module/Equiv.lean b/Mathlib/Topology/Algebra/Module/Equiv.lean
index 215464405d79ec..afc135bda2246b 100644
--- a/Mathlib/Topology/Algebra/Module/Equiv.lean
+++ b/Mathlib/Topology/Algebra/Module/Equiv.lean
@@ -1163,7 +1163,7 @@ lemma IsInvertible.inverse_comp_of_left {g : M₂ →L[R] M₃} {f : M →L[R] M
 
 lemma IsInvertible.inverse_comp_apply_of_left {g : M₂ →L[R] M₃} {f : M →L[R] M₂} {v : M₃}
     (hg : g.IsInvertible) : (g ∘L f).inverse v = f.inverse (g.inverse v) := by
-  simp only [hg.inverse_comp_of_left, coe_comp', Function.comp_apply]
+  simp only [hg.inverse_comp_of_left, comp_apply]
 
 lemma IsInvertible.inverse_comp_of_right {g : M₂ →L[R] M₃} {f : M →L[R] M₂}
     (hf : f.IsInvertible) : (g ∘L f).inverse = f.inverse ∘L g.inverse := by
@@ -1172,7 +1172,7 @@ lemma IsInvertible.inverse_comp_of_right {g : M₂ →L[R] M₃} {f : M →L[R]
 
 lemma IsInvertible.inverse_comp_apply_of_right {g : M₂ →L[R] M₃} {f : M →L[R] M₂} {v : M₃}
     (hf : f.IsInvertible) : (g ∘L f).inverse v = f.inverse (g.inverse v) := by
-  simp only [hf.inverse_comp_of_right, coe_comp', Function.comp_apply]
+  simp only [hf.inverse_comp_of_right, comp_apply]
 
 @[simp]
 theorem ringInverse_equiv (e : M ≃L[R] M) : (↑e)⁻¹ʳ = inverse (e : M →L[R] M) := by
diff --git a/Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean b/Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean
index 4739fd4c017f8e..0f9c1b4807783e 100644
--- a/Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean
+++ b/Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean
@@ -394,10 +394,7 @@ def linearDeriv : (∀ i, M₁ i) →L[R] M₂ := ∑ i : ι, (f.toContinuousLin
 
 @[simp]
 lemma linearDeriv_apply : f.linearDeriv x y = ∑ i, f (Function.update x i (y i)) := by
-  unfold linearDeriv toContinuousLinearMap
-  simp only [ContinuousLinearMap.coe_sum', ContinuousLinearMap.coe_comp',
-    ContinuousLinearMap.coe_mk', Finset.sum_apply]
-  rfl
+  simp [linearDeriv, toContinuousLinearMap]
 
 end linearDeriv
 
diff --git a/Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean b/Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean
index 2bfc44b9bdce72..a420d94256c384 100644
--- a/Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean
+++ b/Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean
@@ -182,7 +182,7 @@ theorem add_apply [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Se
 theorem sum_apply {ι : Type*} [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E))
     (t : Finset ι) (f : ι → E →SLᵤ[σ, 𝔖] F) (x : E) :
     (∑ d ∈ t, f d) x = ∑ d ∈ t, (f d) x :=
-  ContinuousLinearMap.sum_apply t f x
+  _root_.sum_apply (F := E →SL[σ] F) t f x
 
 @[simp]
 theorem sub_apply [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E))
diff --git a/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean b/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
index b9e40fa240f932..d3a0f9317126f0 100644
--- a/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
+++ b/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
@@ -379,7 +379,7 @@ theorem Subalgebra.SeparatesPoints.rclike_to_real {A : StarSubalgebra 𝕜 C(X,
   have hFA : F ∈ A := by
     refine A.sub_mem hfA (@Eq.subst _ (· ∈ A) _ _ ?_ <| A.smul_mem A.one_mem <| f x₂)
     ext1
-    simp only [smul_apply, one_apply, smul_eq_mul, mul_one,
+    simp only [ContinuousMap.smul_apply, one_apply, smul_eq_mul, mul_one,
       const_apply]
   -- Consider now the function `fun x ↦ |f x - f x₂| ^ 2`
   refine ⟨_, ⟨⟨(‖F ·‖ ^ 2), by fun_prop⟩, ?_, rfl⟩, ?_⟩
diff --git a/Mathlib/Topology/VectorBundle/Basic.lean b/Mathlib/Topology/VectorBundle/Basic.lean
index 2485b82762a164..21c11a5ea2ad57 100644
--- a/Mathlib/Topology/VectorBundle/Basic.lean
+++ b/Mathlib/Topology/VectorBundle/Basic.lean
@@ -951,7 +951,7 @@ theorem inCoordinates_eq {x₀ x : B} {y₀ y : B'} {ϕ : E x →SL[σ] E' y}
         (ϕ.comp <|
           (((trivializationAt F E x₀).continuousLinearEquivAt 𝕜₁ x hx).symm : F →L[𝕜₁] E x)) := by
   ext
-  simp_rw [inCoordinates, ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe,
+  simp_rw [inCoordinates, ContinuousLinearMap.coe_comp, ContinuousLinearEquiv.coe_coe,
     Trivialization.coe_continuousLinearEquivAt_eq, Trivialization.symm_continuousLinearEquivAt_eq]
 
 set_option backward.isDefEq.respectTransparency false in
diff --git a/Mathlib/Topology/VectorBundle/Riemannian.lean b/Mathlib/Topology/VectorBundle/Riemannian.lean
index 084a49871a5ddc..cf108f20289169 100644
--- a/Mathlib/Topology/VectorBundle/Riemannian.lean
+++ b/Mathlib/Topology/VectorBundle/Riemannian.lean
@@ -228,8 +228,8 @@ lemma eventually_norm_trivializationAt_lt (x : B) :
       ((trivializationAt F E x).symmL ℝ x) = ContinuousLinearMap.id _ _ := by
     ext v
     have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x
-    simp only [coe_comp', Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply,
-      Function.comp_apply, coe_id', id_eq]
+    simp only [Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply, comp_apply,
+      id_apply]
     convert! ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v
     simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
   have : (trivializationAt F E x).continuousLinearMapAt ℝ y =
@@ -333,8 +333,8 @@ lemma eventually_norm_symmL_trivializationAt_lt (x : B) :
       ((trivializationAt F E x).symmL ℝ x) = ContinuousLinearMap.id _ _ := by
     ext v
     have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x
-    simp only [coe_comp', Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply,
-      Function.comp_apply, coe_id', id_eq]
+    simp only [Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply, comp_apply,
+      id_apply]
     convert! ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v
     simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
   have : (trivializationAt F E x).symmL ℝ y =
diff --git a/MathlibTest/CategoryTheory/ConcreteCategory/TopModuleCat.lean b/MathlibTest/CategoryTheory/ConcreteCategory/TopModuleCat.lean
index 06e94671b3ddf4..2d61aa25decd59 100644
--- a/MathlibTest/CategoryTheory/ConcreteCategory/TopModuleCat.lean
+++ b/MathlibTest/CategoryTheory/ConcreteCategory/TopModuleCat.lean
@@ -26,32 +26,32 @@ example {X Y : Type v}
     [AddCommGroup Y] [Module R Y] [TopologicalSpace Y] [ContinuousAdd Y] [ContinuousSMul R Y]
     (f : X →L[R] Y) (x : X) : (TopModuleCat.ofHom f) x = f x := by simp
 
-example {X Y Z : TopModuleCat R} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(f ≫ g) = ⇑g ∘ ⇑f := by simp
+example {X Y Z : TopModuleCat R} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(f ≫ g) = ⇑g ∘ ⇑f := by ext; simp
 
 example {X Y Z : Type v}
     [AddCommGroup X] [Module R X] [TopologicalSpace X] [ContinuousAdd X] [ContinuousSMul R X]
     [AddCommGroup Y] [Module R Y] [TopologicalSpace Y] [ContinuousAdd Y] [ContinuousSMul R Y]
     [AddCommGroup Z] [Module R Z] [TopologicalSpace Z] [ContinuousAdd Z] [ContinuousSMul R Z]
     (f : X →L[R] Y) (g : Y →L[R] Z) :
-    ⇑(TopModuleCat.ofHom f ≫ TopModuleCat.ofHom g) = g ∘ f := by simp
+    ⇑(TopModuleCat.ofHom f ≫ TopModuleCat.ofHom g) = g ∘ f := by ext; simp
 
 example {X Y : Type v}
     [AddCommGroup X] [Module R X] [TopologicalSpace X] [ContinuousAdd X] [ContinuousSMul R X]
     [AddCommGroup Y] [Module R Y] [TopologicalSpace Y] [ContinuousAdd Y] [ContinuousSMul R Y]
     {Z : TopModuleCat R}
     (f : X →L[R] Y) (g : of R Y ⟶ Z) :
-    ⇑(TopModuleCat.ofHom f ≫ g) = g ∘ f := by simp
+    ⇑(TopModuleCat.ofHom f ≫ g) = g ∘ f := by ext; simp
 
 example {Y Z : TopModuleCat R} {X : Type v}
     [AddCommGroup X] [Module R X] [TopologicalSpace X] [ContinuousAdd X] [ContinuousSMul R X]
     (f : of R X ⟶ Y) (g : Y ⟶ Z) :
-    ⇑(f ≫ g) = g ∘ f := by simp
+    ⇑(f ≫ g) = g ∘ f := by ext; simp
 
 example {X : Type v}
     [AddCommGroup X] [Module R X] [TopologicalSpace X] [ContinuousAdd X] [ContinuousSMul R X]
     {Y Z : TopModuleCat R}
     (f : X →L[R] Y) (g : of R Y ⟶ Z) :
-    ⇑(TopModuleCat.ofHom f ≫ g) = g ∘ f := by simp
+    ⇑(TopModuleCat.ofHom f ≫ g) = g ∘ f := by ext; simp
 
 example {X Y Z : TopModuleCat R} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp