refactor: add explicit equation lemmas for comp and flip (#8371)

This will mostly be a no-op in the current version of Lean, but will override the new behavior from leanprover/lean4#2783.

Once consequence of this is that `rw [comp]` no longer uses "smart unfolding"; it introduces a non-beta reduced term if the composition was applied. As a result, these places need to use `rw [comp_apply]` instead.
My claim is that this is no big deal.

This is split from the lean bump PR #8023, targeting master, to make clear what the fallout is.

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

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

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 → α) :

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

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]

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
 

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