feat: when simps is used on inst names, omit the name (#25125)

eric-wieser · eric-wieser · commit 3bf06aea8f70 · 2025-05-30T10:05:09.000Z
When `@[simps]` is used on
```lean
namespace Foo

@[simps]
instance : Group Foo := ...

end Foo
```
this now generates the names `Foo.mul_def`, `Foo.inv_def`, etc. If `Foo` has `simps` projections, these will be used as `Foo.mul_proj`, `Foo.inv_proj` (respecting prefixes as usual).

This introduces `@[simps (nameStem := "")]` to opt into the behavior explicitly, and `@[simps (nameStem := "instGroup")]` to opt out.

Note that this does not deprecate the old auto-generated names, as in practice it is tricky to exhaustively list them all, and adding support to `simps` to generate them does not seem worth the effort.

It's perhaps worth noting that we didn't need this feature as much in Lean 3, as there the instances were called `instance mul : mul X` instead of `instance instMul : Mul X`, and so we got `theorem mul_mul` instead of `theorem instMul_mul`.
diff --git a/Mathlib/Algebra/BigOperators/Fin.lean b/Mathlib/Algebra/BigOperators/Fin.lean
@@ -626,7 +626,7 @@ theorem finSigmaFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) ×
   rcases k with ⟨⟨iv, hi⟩, j⟩
   rw [finSigmaFinEquiv]
   unfold finSumFinEquiv
-  simp only [Equiv.coe_fn_mk, Equiv.sigmaCongrLeft, Equiv.coe_fn_symm_mk, Equiv.instTrans_trans,
+  simp only [Equiv.coe_fn_mk, Equiv.sigmaCongrLeft, Equiv.coe_fn_symm_mk, Equiv.trans_def,
     Equiv.trans_apply, finCongr_apply, Fin.coe_cast]
   conv  =>
     enter [1,1,3]
diff --git a/Mathlib/Algebra/Category/Ring/Adjunctions.lean b/Mathlib/Algebra/Category/Ring/Adjunctions.lean
@@ -87,7 +87,7 @@ def monoidAlgebra (R : CommRingCat.{max u v}) : CommMonCat.{v} ⥤ Under R where
   map f := Under.homMk (CommRingCat.ofHom <| MonoidAlgebra.mapDomainRingHom R f.hom)
   map_comp f g := by ext : 2; apply MonoidAlgebra.ringHom_ext <;> intro <;> simp
 
-@[simps]
+@[simps (nameStem := "commMon")]
 instance : HasForget₂ CommRingCat CommMonCat where
   forget₂ := { obj M := .of M, map f := CommMonCat.ofHom f.hom }
   forget_comp := rfl
diff --git a/Mathlib/Algebra/Homology/TotalComplexShift.lean b/Mathlib/Algebra/Homology/TotalComplexShift.lean
@@ -77,10 +77,10 @@ variable (x y : ℤ) [K.HasTotal (up ℤ)]
 instance : ((shiftFunctor₁ C x).obj K).HasTotal (up ℤ) := fun n =>
   hasCoproduct_of_equiv_of_iso (K.toGradedObject.mapObjFun (π (up ℤ) (up ℤ) (up ℤ)) (n + x)) _
     { toFun := fun ⟨⟨a, b⟩, h⟩ => ⟨⟨a + x, b⟩, by
-        simp only [Set.mem_preimage, instTotalComplexShape_π, Set.mem_singleton_iff] at h ⊢
+        simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢
         omega⟩
       invFun := fun ⟨⟨a, b⟩, h⟩ => ⟨(a - x, b), by
-        simp only [Set.mem_preimage, instTotalComplexShape_π, Set.mem_singleton_iff] at h ⊢
+        simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢
         omega⟩
       left_inv := by
         rintro ⟨⟨a, b⟩, h⟩
@@ -99,10 +99,10 @@ instance : ((shiftFunctor₁ C x).obj K).HasTotal (up ℤ) := fun n =>
 instance : ((shiftFunctor₂ C y).obj K).HasTotal (up ℤ) := fun n =>
   hasCoproduct_of_equiv_of_iso (K.toGradedObject.mapObjFun (π (up ℤ) (up ℤ) (up ℤ)) (n + y)) _
     { toFun := fun ⟨⟨a, b⟩, h⟩ => ⟨⟨a, b + y⟩, by
-        simp only [Set.mem_preimage, instTotalComplexShape_π, Set.mem_singleton_iff] at h ⊢
+        simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢
         omega⟩
       invFun := fun ⟨⟨a, b⟩, h⟩ => ⟨(a, b - y), by
-        simp only [Set.mem_preimage, instTotalComplexShape_π, Set.mem_singleton_iff] at h ⊢
+        simp only [Set.mem_preimage, π_def, Set.mem_singleton_iff] at h ⊢
         omega⟩
       left_inv _ := by simp
       right_inv _ := by simp }
diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean
@@ -1212,9 +1212,9 @@ instance instInv : Inv ℍ[R] :=
 instance instGroupWithZero : GroupWithZero ℍ[R] :=
   { Quaternion.instNontrivial with
     inv := Inv.inv
-    inv_zero := by rw [instInv_inv, star_zero, smul_zero]
+    inv_zero := by rw [inv_def, star_zero, smul_zero]
     mul_inv_cancel := fun a ha => by
-      rw [instInv_inv, Algebra.mul_smul_comm (normSq a)⁻¹ a (star a), self_mul_star, smul_coe,
+      rw [inv_def, Algebra.mul_smul_comm (normSq a)⁻¹ a (star a), self_mul_star, smul_coe,
         inv_mul_cancel₀ (normSq_ne_zero.2 ha), coe_one] }
 
 @[norm_cast, simp]
diff --git a/Mathlib/AlgebraicGeometry/ResidueField.lean b/Mathlib/AlgebraicGeometry/ResidueField.lean
@@ -227,7 +227,7 @@ instance {X : Scheme.{u}} (x : X) : IsPreimmersion (X.fromSpecResidueField x) :=
 @[simps] noncomputable
 instance (x : X) : (Spec (X.residueField x)).Over X := ⟨X.fromSpecResidueField x⟩
 
-@[simps! over] noncomputable
+noncomputable
 instance (x : X) : (Spec (X.residueField x)).CanonicallyOver X where
 
 @[reassoc (attr := simp)]
diff --git a/Mathlib/AlgebraicGeometry/Stalk.lean b/Mathlib/AlgebraicGeometry/Stalk.lean
@@ -68,7 +68,7 @@ noncomputable def Scheme.fromSpecStalk (X : Scheme) (x : X) :
 @[simps over] noncomputable
 instance (X : Scheme.{u}) (x : X) : (Spec (X.presheaf.stalk x)).Over X := ⟨X.fromSpecStalk x⟩
 
-@[simps! over] noncomputable
+noncomputable
 instance (X : Scheme.{u}) (x : X) : (Spec (X.presheaf.stalk x)).CanonicallyOver X where
 
 @[simp]
diff --git a/Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean b/Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
@@ -516,13 +516,13 @@ end SimplicialObject
 def CosimplicialObject :=
   SimplexCategory ⥤ C
 
+namespace CosimplicialObject
+
 @[simps!]
 instance : Category (CosimplicialObject C) := by
   dsimp only [CosimplicialObject]
   infer_instance
 
-namespace CosimplicialObject
-
 /-- `X ^⦋n⦌` denotes the `n`th-term of the cosimplicial object X -/
 scoped[Simplicial]
   notation3:1000 X " ^⦋" n "⦌" =>
diff --git a/Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean b/Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean
@@ -275,7 +275,7 @@ def vcomp : StrongTrans F H :=
 /-- `CategoryStruct` on `OplaxFunctor B C` where the (1-)morphisms are given by strong
 transformations. -/
 @[simps! id_app id_naturality comp_app comp_naturality]
-scoped instance : CategoryStruct (OplaxFunctor B C) where
+scoped instance OplaxFunctor.instCategoryStruct : CategoryStruct (OplaxFunctor B C) where
   Hom := StrongTrans
   id := StrongTrans.id
   comp := StrongTrans.vcomp
diff --git a/Mathlib/CategoryTheory/Comma/Over/OverClass.lean b/Mathlib/CategoryTheory/Comma/Over/OverClass.lean
@@ -72,10 +72,12 @@ instance : OverClass X X := ⟨𝟙 _⟩
 
 instance : IsIso (S ↘ S) := inferInstanceAs (IsIso (𝟙 S))
 
+namespace CanonicallyOverClass
 -- This cannot be a simp lemma be cause it loops with `comp_over`.
 @[simps -isSimp]
 instance (priority := 900) [CanonicallyOverClass X Y] [OverClass Y S] : OverClass X S :=
   ⟨X ↘ Y ≫ Y ↘ S⟩
+end CanonicallyOverClass
 
 /-- Given `OverClass X S` and `OverClass Y S` and `f : X ⟶ Y`,
 `HomIsOver f S` is the typeclass asserting `f` commutes with the structure morphisms. -/
diff --git a/Mathlib/CategoryTheory/Comma/StructuredArrow/Final.lean b/Mathlib/CategoryTheory/Comma/StructuredArrow/Final.lean
@@ -53,7 +53,7 @@ private lemma final_of_final_costructuredArrowToOver_small (L : A ⥤ T) (R : B
             Final.colimitIso _ _
       _ ≅ colimit G := (colimitIsoColimitGrothendieck (𝟭 T) G).symm
   convert Iso.isIso_hom i
-  simp only [Iso.instTransIso_trans, comp_obj, grothendieckProj_obj, Grothendieck.pre_obj_base,
+  simp only [Iso.trans_def, comp_obj, grothendieckProj_obj, Grothendieck.pre_obj_base,
     Grothendieck.pre_obj_fiber, Iso.trans_assoc, Iso.trans_hom, Iso.symm_hom, i]
   rw [← Iso.inv_comp_eq, Iso.eq_inv_comp]
   apply colimit.hom_ext (fun _ => by simp)
diff --git a/Mathlib/CategoryTheory/Dialectica/Monoidal.lean b/Mathlib/CategoryTheory/Dialectica/Monoidal.lean
@@ -29,20 +29,20 @@ local notation "π₂" => prod.snd
 local notation "π(" a ", " b ")" => prod.lift a b
 
 /-- The object `X ⊗ Y` in the `Dial C` category just tuples the left and right components. -/
-@[simps] def tensorObj (X Y : Dial C) : Dial C where
+@[simps] def tensorObjImpl (X Y : Dial C) : Dial C where
   src := X.src ⨯ Y.src
   tgt := X.tgt ⨯ Y.tgt
   rel :=
     (Subobject.pullback (prod.map π₁ π₁)).obj X.rel ⊓
     (Subobject.pullback (prod.map π₂ π₂)).obj Y.rel
 
 /-- The functorial action of `X ⊗ Y` in `Dial C`. -/
-@[simps] def tensorHom {X₁ X₂ Y₁ Y₂ : Dial C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) :
-    tensorObj X₁ Y₁ ⟶ tensorObj X₂ Y₂ where
+@[simps] def tensorHomImpl {X₁ X₂ Y₁ Y₂ : Dial C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) :
+    tensorObjImpl X₁ Y₁ ⟶ tensorObjImpl X₂ Y₂ where
   f := prod.map f.f g.f
   F := π(prod.map π₁ π₁ ≫ f.F, prod.map π₂ π₂ ≫ g.F)
   le := by
-    simp only [tensorObj, Subobject.inf_pullback]
+    simp only [tensorObjImpl, Subobject.inf_pullback]
     apply inf_le_inf <;> rw [← Subobject.pullback_comp, ← Subobject.pullback_comp]
     · have := (Subobject.pullback (prod.map π₁ π₁ :
         (X₁.src ⨯ Y₁.src) ⨯ X₂.tgt ⨯ Y₂.tgt ⟶ _)).monotone (Hom.le f)
@@ -54,32 +54,33 @@ local notation "π(" a ", " b ")" => prod.lift a b
       convert this using 3 <;> simp
 
 /-- The unit for the tensor `X ⊗ Y` in `Dial C`. -/
-@[simps] def tensorUnit : Dial C := { src := ⊤_ _, tgt := ⊤_ _, rel := ⊤ }
+@[simps] def tensorUnitImpl : Dial C := { src := ⊤_ _, tgt := ⊤_ _, rel := ⊤ }
 
 /-- Left unit cancellation `1 ⊗ X ≅ X` in `Dial C`. -/
-@[simps!] def leftUnitor (X : Dial C) : tensorObj tensorUnit X ≅ X :=
+@[simps!] def leftUnitorImpl (X : Dial C) : tensorObjImpl tensorUnitImpl X ≅ X :=
   isoMk (Limits.prod.leftUnitor _) (Limits.prod.leftUnitor _) <| by simp [Subobject.pullback_top]
 
 /-- Right unit cancellation `X ⊗ 1 ≅ X` in `Dial C`. -/
-@[simps!] def rightUnitor (X : Dial C) : tensorObj X tensorUnit ≅ X :=
+@[simps!] def rightUnitorImpl (X : Dial C) : tensorObjImpl X tensorUnitImpl ≅ X :=
   isoMk (Limits.prod.rightUnitor _) (Limits.prod.rightUnitor _) <| by simp [Subobject.pullback_top]
 
 /-- The associator for tensor, `(X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z)` in `Dial C`. -/
 @[simps!]
-def associator (X Y Z : Dial C) : tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z) :=
+def associatorImpl (X Y Z : Dial C) :
+    tensorObjImpl (tensorObjImpl X Y) Z ≅ tensorObjImpl X (tensorObjImpl Y Z) :=
   isoMk (prod.associator ..) (prod.associator ..) <| by
     simp [Subobject.inf_pullback, ← Subobject.pullback_comp, inf_assoc]
 
 @[simps!]
 instance : MonoidalCategoryStruct (Dial C) where
-  tensorUnit := tensorUnit
-  tensorObj := tensorObj
-  whiskerLeft X _ _ f := tensorHom (𝟙 X) f
-  whiskerRight f Y := tensorHom f (𝟙 Y)
-  tensorHom := tensorHom
-  leftUnitor := leftUnitor
-  rightUnitor := rightUnitor
-  associator := associator
+  tensorUnit := tensorUnitImpl
+  tensorObj := tensorObjImpl
+  whiskerLeft X _ _ f := tensorHomImpl (𝟙 X) f
+  whiskerRight f Y := tensorHomImpl f (𝟙 Y)
+  tensorHom := tensorHomImpl
+  leftUnitor := leftUnitorImpl
+  rightUnitor := rightUnitorImpl
+  associator := associatorImpl
 
 theorem tensor_id (X₁ X₂ : Dial C) : (𝟙 X₁ ⊗ 𝟙 X₂ : _ ⟶ _) = 𝟙 (X₁ ⊗ X₂ : Dial C) := by aesop_cat
 
diff --git a/Mathlib/CategoryTheory/Idempotents/Biproducts.lean b/Mathlib/CategoryTheory/Idempotents/Biproducts.lean
@@ -64,7 +64,7 @@ def bicone [HasFiniteBiproducts C] {J : Type} [Finite J] (F : J → Karoubi C) :
         id_f, hom_ext_iff, comp_f, assoc, bicone_ι_π_self_assoc, idem]
     · dsimp
       simp only [biproduct.ι_map, biproduct.map_π, hom_ext_iff, comp_f,
-        assoc, biproduct.ι_π_ne_assoc _ h, zero_comp, comp_zero, instZero_zero]
+        assoc, biproduct.ι_π_ne_assoc _ h, zero_comp, comp_zero, zero_def]
 
 end Biproducts
 
@@ -103,15 +103,15 @@ instance (P : Karoubi C) : HasBinaryBiproduct P P.complement :=
       inr := P.complement.decompId_i
       inl_fst := P.decompId.symm
       inl_snd := by
-        simp only [instZero_zero, hom_ext_iff, complement_X, comp_f,
+        simp only [zero_def, hom_ext_iff, complement_X, comp_f,
           decompId_i_f, decompId_p_f, complement_p, comp_sub, comp_id, idem, sub_self]
       inr_fst := by
-        simp only [instZero_zero, hom_ext_iff, complement_X, comp_f,
+        simp only [zero_def, hom_ext_iff, complement_X, comp_f,
           decompId_i_f, complement_p, decompId_p_f, sub_comp, id_comp, idem, sub_self]
       inr_snd := P.complement.decompId.symm }
     (by
       ext
-      simp only [complement_X, comp_f, decompId_i_f, decompId_p_f, complement_p, instAdd_add, idem,
+      simp only [complement_X, comp_f, decompId_i_f, decompId_p_f, complement_p, add_def, idem,
         comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero, add_sub_cancel, id_f])
 
 attribute [-simp] hom_ext_iff
@@ -129,16 +129,16 @@ def decomposition (P : Karoubi C) : P ⊞ P.complement ≅ (toKaroubi _).obj P.X
       refine (?_ =≫ _).trans zero_comp
       ext
       simp only [comp_f, toKaroubi_obj_X, decompId_i_f, decompId_p_f,
-        complement_p, comp_sub, comp_id, idem, sub_self, instZero_zero]
+        complement_p, comp_sub, comp_id, idem, sub_self, zero_def]
     · rw [biprod.inr_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc,
         add_eq_right, ← assoc]
       refine (?_ =≫ _).trans zero_comp
       ext
       simp only [complement_X, comp_f, decompId_i_f, complement_p,
-        decompId_p_f, sub_comp, id_comp, idem, sub_self, instZero_zero]
+        decompId_p_f, sub_comp, id_comp, idem, sub_self, zero_def]
   inv_hom_id := by
     ext
-    simp only [toKaroubi_obj_X, biprod.lift_desc, instAdd_add, comp_f, decompId_p_f, decompId_i_f,
+    simp only [toKaroubi_obj_X, biprod.lift_desc, add_def, comp_f, decompId_p_f, decompId_i_f,
       idem, complement_X, complement_p, comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero,
       add_sub_cancel, id_f, toKaroubi_obj_p]
 
diff --git a/Mathlib/CategoryTheory/Limits/Indization/LocallySmall.lean b/Mathlib/CategoryTheory/Limits/Indization/LocallySmall.lean
@@ -51,7 +51,7 @@ theorem colimitYonedaHomEquiv_π_apply (η : colimit (F ⋙ yoneda) ⟶ G) (i :
     limit.π (F.op ⋙ G) i (colimitYonedaHomEquiv F G η) =
       η.app (op (F.obj i.unop)) ((colimit.ι (F ⋙ yoneda) i.unop).app _ (𝟙 _)) := by
   simp only [Functor.comp_obj, Functor.op_obj, colimitYonedaHomEquiv, uliftFunctor_obj,
-    Iso.instTransIso_trans, Iso.trans_assoc, Iso.toEquiv_comp, Equiv.symm_trans_apply,
+    Iso.trans_def, Iso.trans_assoc, Iso.toEquiv_comp, Equiv.symm_trans_apply,
     Equiv.symm_symm, Equiv.trans_apply, Iso.toEquiv_fun, Iso.symm_hom, Equiv.ulift_apply]
   have (a) := congrArg ULift.down
     (congrFun (preservesLimitIso_inv_π uliftFunctor.{u, v} (F.op ⋙ G) i) a)
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Grothendieck.lean b/Mathlib/CategoryTheory/Limits/Preserves/Grothendieck.lean
@@ -77,7 +77,7 @@ instance preservesLimitsOfShape_colim_grothendieck [HasColimitsOfShape C H] [Has
   haveI : IsIso (limit.post K colim) := by
     convert Iso.isIso_hom i₂
     ext
-    simp only [colim_obj, Functor.comp_obj, limit.post_π, colim_map, Iso.instTransIso_trans,
+    simp only [colim_obj, Functor.comp_obj, limit.post_π, colim_map, Iso.trans_def,
       Iso.trans_assoc, Iso.trans_hom, Category.assoc, HasLimit.isoOfNatIso_hom_π,
       fiberwiseColim_obj, isoWhiskerLeft_hom, NatTrans.comp_app, Functor.associator_hom_app,
       whiskerLeft_app, fiberwiseColimCompColimIso_hom_app, Category.id_comp,
diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean
@@ -933,14 +933,8 @@ noncomputable instance instCartesianMonoidalCategory :
 
 lemma tensor_obj (X Y : F.EssImageSubcategory) : (X ⊗ Y).obj = X.obj ⊗ Y.obj := rfl
 
-lemma fst_def (X Y : F.EssImageSubcategory) : fst X Y = fst X.obj Y.obj := rfl
-lemma snd_def (X Y : F.EssImageSubcategory) : snd X Y = snd X.obj Y.obj := rfl
 lemma lift_def (f : T ⟶ X) (g : T ⟶ Y) : lift f g = lift (T := T.1) f g := rfl
 
-lemma whiskerLeft_def (X : F.EssImageSubcategory) (f : Y ⟶ Z) : X ◁ f = X.obj ◁ f := rfl
-lemma whiskerRight_def (f : Y ⟶ Z) (X : F.EssImageSubcategory) :
-    f ▷ X = MonoidalCategoryStruct.whiskerRight (C := D) f X.obj := rfl
-
 lemma associator_hom_def (X Y Z : F.EssImageSubcategory) :
     (α_ X Y Z).hom = (α_ X.obj Y.obj Z.obj).hom := rfl
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Mon_.lean b/Mathlib/CategoryTheory/Monoidal/Mon_.lean
@@ -618,6 +618,8 @@ theorem mul_rightUnitor {M : C} [Mon_Class M] :
   slice_lhs 1 3 => rw [← rightUnitor_monoidal]
   simp only [Category.assoc, Category.id_comp]
 
+namespace tensorObj
+
 @[simps]
 instance {M N : C} [Mon_Class M] [Mon_Class N] : Mon_Class (M ⊗ N) where
   one := (λ_ (𝟙_ C)).inv ≫ (η ⊗ η)
@@ -626,6 +628,8 @@ instance {M N : C} [Mon_Class M] [Mon_Class N] : Mon_Class (M ⊗ N) where
   mul_one' := Mon_tensor_mul_one M N
   mul_assoc' := Mon_tensor_mul_assoc M N
 
+end tensorObj
+
 open IsMon_Hom
 
 variable {X Y Z W : C} [Mon_Class X] [Mon_Class Y] [Mon_Class Z] [Mon_Class W]
@@ -660,7 +664,7 @@ instance : IsMon_Hom (ρ_ X).hom :=
   ⟨one_rightUnitor, mul_rightUnitor⟩
 
 theorem one_braiding (X Y : C) [Mon_Class X] [Mon_Class Y] : η ≫ (β_ X Y).hom = η := by
-  simp only [instTensorObj_one, Category.assoc, BraidedCategory.braiding_naturality,
+  simp only [tensorObj.one_def, Category.assoc, BraidedCategory.braiding_naturality,
     braiding_tensorUnit_right, Iso.cancel_iso_inv_left]
   monoidal
 
diff --git a/Mathlib/CategoryTheory/Sites/Adjunction.lean b/Mathlib/CategoryTheory/Sites/Adjunction.lean
@@ -63,7 +63,7 @@ lemma adjunction_counit_app_val [HasWeakSheafify J D] [HasSheafCompose J F] (adj
   simp only [Functor.comp_obj, sheafToPresheaf_obj, sheafCompose_obj_val, whiskeringRight_obj_obj,
     adjunction, Adjunction.map_restrictFullyFaithful_counit_app, Iso.refl_inv, NatTrans.id_app,
     Functor.comp_map, whiskeringRight_obj_map, Adjunction.comp_counit_app,
-    instCategorySheaf_comp_val, instCategorySheaf_id_val, sheafificationAdjunction_counit_app_val,
+    comp_val, id_val, sheafificationAdjunction_counit_app_val,
     sheafifyMap_sheafifyLift, Functor.id_obj, whiskerRight_id', Category.comp_id, Category.id_comp]
 
 
diff --git a/Mathlib/CategoryTheory/Sites/ConstantSheaf.lean b/Mathlib/CategoryTheory/Sites/ConstantSheaf.lean
@@ -190,11 +190,11 @@ lemma constantSheafAdj_counit_w {T : C} (hT : IsTerminal T) :
       ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)) =
         ((sheafCompose J U).map ((constantSheafAdj J D hT).counit.app F)) := by
   apply Sheaf.hom_ext
-  rw [instCategorySheaf_comp_val, constantCommuteCompose_hom_app_val, assoc, Iso.inv_comp_eq]
+  rw [comp_val, constantCommuteCompose_hom_app_val, assoc, Iso.inv_comp_eq]
   apply sheafify_hom_ext _ _ _ ((sheafCompose J U).obj F).cond
   ext
   simp? says simp only [comp_obj, const_obj_obj, sheafCompose_obj_val, id_obj,
-      constantSheafAdj_counit_app, instCategorySheaf_comp_val,
+      constantSheafAdj_counit_app, comp_val,
       sheafificationAdjunction_counit_app_val, sheafifyMap_sheafifyLift, comp_id,
       toSheafify_sheafifyLift, NatTrans.comp_app, constComp_hom_app,
       constantPresheafAdj_counit_app_app, Functor.comp_map, id_comp, flip_obj_obj,
diff --git a/Mathlib/CategoryTheory/Sites/Equivalence.lean b/Mathlib/CategoryTheory/Sites/Equivalence.lean
@@ -117,10 +117,10 @@ def sheafCongr : Sheaf J A ≌ Sheaf K A where
   functor_unitIso_comp X := by
     ext
     simp only [id_obj, sheafCongr.functor_obj_val_obj, comp_obj,
-      Sheaf.instCategorySheaf_comp_val, NatTrans.comp_app, sheafCongr.inverse_obj_val_obj,
+      Sheaf.comp_val, NatTrans.comp_app, sheafCongr.inverse_obj_val_obj,
       Opposite.unop_op, sheafCongr.functor_map_val_app,
       sheafCongr.unitIso_hom_app_val_app, sheafCongr.counitIso_hom_app_val_app,
-      sheafCongr.functor_obj_val_map, Quiver.Hom.unop_op, Sheaf.instCategorySheaf_id_val,
+      sheafCongr.functor_obj_val_map, Quiver.Hom.unop_op, Sheaf.id_val,
       NatTrans.id_app]
     simp [← Functor.map_comp, ← op_comp]
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Partition.lean b/Mathlib/Combinatorics/SimpleGraph/Partition.lean
@@ -122,9 +122,11 @@ def Coloring.toPartition {α : Type v} (C : G.Coloring α) : G.Partition where
     rintro s ⟨c, rfl⟩
     apply C.color_classes_independent
 
+namespace Partition
 /-- The partition where every vertex is in its own part. -/
 @[simps]
 instance : Inhabited (Partition G) := ⟨G.selfColoring.toPartition⟩
+end Partition
 
 theorem partitionable_iff_colorable {n : ℕ} : G.Partitionable n ↔ G.Colorable n := by
   constructor
diff --git a/Mathlib/Condensed/Discrete/LocallyConstant.lean b/Mathlib/Condensed/Discrete/LocallyConstant.lean
@@ -258,7 +258,7 @@ noncomputable def counit [HasExplicitFiniteCoproducts.{u} P] : haveI := CompHaus
     apply Sheaf.hom_ext
     simp only [functor, id_eq, eq_mpr_eq_cast, Functor.comp_obj, Functor.flip_obj_obj,
       sheafToPresheaf_obj, Functor.id_obj, Functor.comp_map, Functor.flip_obj_map,
-      sheafToPresheaf_map, Sheaf.instCategorySheaf_comp_val, Functor.id_map]
+      sheafToPresheaf_map, Sheaf.comp_val, Functor.id_map]
     ext S (f : LocallyConstant _ _)
     simp only [FunctorToTypes.comp, counitApp_app]
     apply presheaf_ext (f.map (g.val.app (op (CompHausLike.of P PUnit.{u + 1}))))
@@ -333,7 +333,7 @@ noncomputable def adjunction [HasExplicitFiniteCoproducts.{u} P] :
       sheafToPresheaf_obj, functor_obj_val, functorToPresheaves_obj_obj, coe_of, whiskerRight_app,
       Functor.associator_hom_app, whiskerLeft_app, Category.id_comp, NatTrans.id_app']
     apply Sheaf.hom_ext
-    rw [Sheaf.instCategorySheaf_comp_val, Sheaf.instCategorySheaf_id_val]
+    rw [Sheaf.comp_val, Sheaf.id_val]
     exact adjunction_left_triangle P hs X
   right_triangle_components := by
     intro X
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
@@ -458,7 +458,7 @@ theorem integerSetEquivNorm_apply_fst {n : ℕ}
     (a : {a : integerSet K // mixedEmbedding.norm (a : mixedSpace K) = n}) :
     ((integerSetEquivNorm K n a).1 : Ideal (𝓞 K)) =
       span {(preimageOfMemIntegerSet a.val : 𝓞 K)} := by
-  simp_rw [integerSetEquivNorm, Equiv.prodSubtypeFstEquivSubtypeProd, Equiv.instTrans_trans,
+  simp_rw [integerSetEquivNorm, Equiv.prodSubtypeFstEquivSubtypeProd, Equiv.trans_def,
     Equiv.prodCongrLeft, Equiv.trans_apply, Equiv.subtypeEquiv_apply, Equiv.coe_fn_mk,
     Equiv.subtypeSubtypeEquivSubtypeInter_apply_coe, integerSetEquiv_apply_fst]
 
diff --git a/Mathlib/Order/OmegaCompletePartialOrder.lean b/Mathlib/Order/OmegaCompletePartialOrder.lean
diff --git a/Mathlib/RepresentationTheory/Rep.lean b/Mathlib/RepresentationTheory/Rep.lean
diff --git a/Mathlib/Tactic/Simps/Basic.lean b/Mathlib/Tactic/Simps/Basic.lean
diff --git a/MathlibTest/Simps.lean b/MathlibTest/Simps.lean
