diff --git a/Archive/Wiedijk100Theorems/CubingACube.lean b/Archive/Wiedijk100Theorems/CubingACube.lean
index 03113afd3a5aa..f5612ef8b1109 100644
--- a/Archive/Wiedijk100Theorems/CubingACube.lean
+++ b/Archive/Wiedijk100Theorems/CubingACube.lean
@@ -219,7 +219,7 @@ theorem shiftUp_bottom_subset_bottoms (hc : (cs i).xm ≠ 1) :
   rw [mem_iUnion]; use i'; refine' ⟨_, fun j => hi' j.succ⟩
   have : i ≠ i' := by rintro rfl; apply not_le_of_lt (hi' 0).2; rw [hp0]; rfl
   have := h.1 this
-  rw [onFun, comp, comp, toSet_disjoint, exists_fin_succ] at this
+  rw [onFun, comp_apply, comp_apply, toSet_disjoint, exists_fin_succ] at this
   rcases this with (h0 | ⟨j, hj⟩)
   rw [hp0]; symm; apply eq_of_Ico_disjoint h0 (by simp [hw]) _
   convert hi' 0; rw [hp0]; rfl
diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
index 45a6494e386a8..a02aa37dea621 100644
--- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@@ -747,7 +747,7 @@ def counit : restrictScalars.{max v u₂,u₁,u₂} f ⋙ extendScalars f ⟶ 
     induction' z using TensorProduct.induction_on with s' y z₁ z₂ ih₁ ih₂
     · rw [map_zero, map_zero]
     · dsimp
-      rw [ModuleCat.coe_comp, ModuleCat.coe_comp,Function.comp,Function.comp,
+      rw [ModuleCat.coe_comp, ModuleCat.coe_comp, Function.comp_apply, Function.comp_apply,
         ExtendScalars.map_tmul, restrictScalars.map_apply]
       -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
       erw [Counit.map_apply]
@@ -771,7 +771,7 @@ def extendRestrictScalarsAdj {R : Type u₁} {S : Type u₂} [CommRing R] [CommR
   counit := ExtendRestrictScalarsAdj.counit.{v,u₁,u₂} f
   homEquiv_unit {X Y g} := LinearMap.ext fun x => by
     dsimp
-    rw [ModuleCat.coe_comp, Function.comp, restrictScalars.map_apply]
+    rw [ModuleCat.coe_comp, Function.comp_apply, restrictScalars.map_apply]
     rfl
   homEquiv_counit {X Y g} := LinearMap.ext fun x => by
       -- Porting note: once again reminding Lean of the instances
diff --git a/Mathlib/Data/Fin/Tuple/Basic.lean b/Mathlib/Data/Fin/Tuple/Basic.lean
index 9a7a59a96197d..754a9aca44800 100644
--- a/Mathlib/Data/Fin/Tuple/Basic.lean
+++ b/Mathlib/Data/Fin/Tuple/Basic.lean
@@ -242,7 +242,7 @@ theorem comp_cons {α : Type*} {β : Type*} (g : α → β) (y : α) (q : Fin n
     rfl
   · let j' := pred j h
     have : j'.succ = j := succ_pred j h
-    rw [← this, cons_succ, comp, comp, cons_succ]
+    rw [← this, cons_succ, comp_apply, comp_apply, cons_succ]
 #align fin.comp_cons Fin.comp_cons
 
 theorem comp_tail {α : Type*} {β : Type*} (g : α → β) (q : Fin n.succ → α) :
diff --git a/Mathlib/Data/MvPolynomial/Rename.lean b/Mathlib/Data/MvPolynomial/Rename.lean
index e978c9dabbc4d..c2b154c0989d2 100644
--- a/Mathlib/Data/MvPolynomial/Rename.lean
+++ b/Mathlib/Data/MvPolynomial/Rename.lean
@@ -85,7 +85,7 @@ theorem rename_rename (f : σ → τ) (g : τ → α) (p : MvPolynomial σ R) :
     -- porting note: the Lean 3 proof of this was very fragile and included a nonterminal `simp`.
     -- Hopefully this is less prone to breaking
     rw [eval₂_comp_left (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C (X ∘ f) p]
-    simp only [(· ∘ ·), eval₂Hom_X', coe_eval₂Hom]
+    simp only [(· ∘ ·), eval₂Hom_X']
     refine' eval₂Hom_congr _ rfl rfl
     ext1; simp only [comp_apply, RingHom.coe_comp, eval₂Hom_C]
 #align mv_polynomial.rename_rename MvPolynomial.rename_rename
diff --git a/Mathlib/Init/Function.lean b/Mathlib/Init/Function.lean
index 49b5c55613678..b6a83ee09f6e0 100644
--- a/Mathlib/Init/Function.lean
+++ b/Mathlib/Init/Function.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Haitao Zhang
 import Mathlib.Init.Logic
 import Mathlib.Mathport.Rename
 import Mathlib.Tactic.Attr.Register
+import Mathlib.Tactic.Eqns
 
 #align_import init.function from "leanprover-community/lean"@"03a6a6015c0b12dce7b36b4a1f7205a92dfaa592"
 
@@ -25,6 +26,12 @@ variable {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ
 
 lemma comp_def {α β δ : Sort _} (f : β → δ) (g : α → β) : f ∘ g = fun x ↦ f (g x) := rfl
 
+attribute [eqns comp_def] comp
+
+lemma flip_def {f : α → β → φ} : flip f = fun b a => f a b := rfl
+
+attribute [eqns flip_def] flip
+
 /-- Composition of dependent functions: `(f ∘' g) x = f (g x)`, where type of `g x` depends on `x`
 and type of `f (g x)` depends on `x` and `g x`. -/
 @[inline, reducible]
diff --git a/Mathlib/NumberTheory/NumberField/Discriminant.lean b/Mathlib/NumberTheory/NumberField/Discriminant.lean
index 1e7efa51bd67d..5dfdac5462aa6 100644
--- a/Mathlib/NumberTheory/NumberField/Discriminant.lean
+++ b/Mathlib/NumberTheory/NumberField/Discriminant.lean
@@ -75,8 +75,8 @@ theorem _root_.NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis
           ← coe_discr, map_intCast, ← Complex.nnnorm_int]
   ext : 2
   dsimp only
-  rw [Matrix.map_apply, Basis.toMatrix_apply, Basis.coe_reindex, Function.comp, Equiv.symm_symm,
-    latticeBasis_apply, ← commMap_canonical_eq_mixed, Complex.ofReal_eq_coe,
+  rw [Matrix.map_apply, Basis.toMatrix_apply, Basis.coe_reindex, Function.comp_apply,
+    Equiv.symm_symm, latticeBasis_apply, ← commMap_canonical_eq_mixed, Complex.ofReal_eq_coe,
     stdBasis_repr_eq_matrixToStdBasis_mul K _ (fun _ => rfl)]
   rfl
 
diff --git a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean
index f08ecff849976..afc421f38e32e 100644
--- a/Mathlib/Topology/UniformSpace/AbstractCompletion.lean
+++ b/Mathlib/Topology/UniformSpace/AbstractCompletion.lean
@@ -208,7 +208,7 @@ theorem map_unique {f : α → β} {g : hatα → hatβ} (hg : UniformContinuous
   pkg.funext (pkg.continuous_map _ _) hg.continuous <| by
     intro a
     change pkg.extend (ι' ∘ f) _ = _
-    simp only [(· ∘ ·), h, ←comp_apply (f := g)]
+    simp_rw [(· ∘ ·), h, ←comp_apply (f := g)]
     rw [pkg.extend_coe (hg.comp pkg.uniformContinuous_coe)]
 #align abstract_completion.map_unique AbstractCompletion.map_unique