diff --git a/Mathlib/CategoryTheory/Functor/Category.lean b/Mathlib/CategoryTheory/Functor/Category.lean
index c157e50875..d060ac1d7e 100644
--- a/Mathlib/CategoryTheory/Functor/Category.lean
+++ b/Mathlib/CategoryTheory/Functor/Category.lean
@@ -150,7 +150,7 @@ end NatTrans
 namespace Functor
 
 /-- Flip the arguments of a bifunctor. See also `Currying.lean`. -/
-@[simps (attr := grind =) obj_obj obj_map]
+@[implicit_reducible, simps (attr := grind =) obj_obj obj_map]
 protected def flip (F : C ⥤ D ⥤ E) : D ⥤ C ⥤ E where
   obj k :=
     { obj := fun j => (F.obj j).obj k,
@@ -164,7 +164,7 @@ protected def flip (F : C ⥤ D ⥤ E) : D ⥤ C ⥤ E where
 
 /-- The left unitor, a natural isomorphism `((𝟭 _) ⋙ F) ≅ F`.
 -/
-@[simps]
+@[implicit_reducible, simps]
 def leftUnitor (F : C ⥤ D) :
     𝟭 C ⋙ F ≅ F where
   hom := { app := fun X => 𝟙 (F.obj X) }
@@ -172,7 +172,7 @@ def leftUnitor (F : C ⥤ D) :
 
 /-- The right unitor, a natural isomorphism `(F ⋙ (𝟭 B)) ≅ F`.
 -/
-@[simps]
+@[implicit_reducible, simps]
 def rightUnitor (F : C ⥤ D) :
     F ⋙ 𝟭 D ≅ F where
   hom := { app := fun X => 𝟙 (F.obj X) }
@@ -183,7 +183,7 @@ def rightUnitor (F : C ⥤ D) :
 (In fact, `iso.refl _` will work here, but it tends to make Lean slow later,
 and it's usually best to insert explicit associators.)
 -/
-@[simps]
+@[implicit_reducible, simps]
 def associator (F : C ⥤ D) (G : D ⥤ E) (H : E ⥤ E') :
     (F ⋙ G) ⋙ H ≅ F ⋙ G ⋙ H where
   hom := { app := fun _ => 𝟙 _ }
@@ -196,7 +196,7 @@ end Functor
 
 variable (C D E) in
 /-- The functor `(C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E` which flips the variables. -/
-@[simps]
+@[implicit_reducible, simps]
 def flipFunctor : (C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E where
   obj F := F.flip
   map {F₁ F₂} φ :=
diff --git a/Mathlib/CategoryTheory/Functor/Currying.lean b/Mathlib/CategoryTheory/Functor/Currying.lean
index d003000bce..7824fb6c39 100644
--- a/Mathlib/CategoryTheory/Functor/Currying.lean
+++ b/Mathlib/CategoryTheory/Functor/Currying.lean
@@ -54,6 +54,7 @@ def uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E where
 
 /-- The object level part of the currying functor. (See `curry` for the functorial version.)
 -/
+@[implicit_reducible]
 def curryObj (F : C × D ⥤ E) : C ⥤ D ⥤ E where
   obj X :=
     { obj := fun Y => F.obj (X, Y)
@@ -68,7 +69,7 @@ def curryObj (F : C × D ⥤ E) : C ⥤ D ⥤ E where
 
 /-- The currying functor, taking a functor `(C × D) ⥤ E` and producing a functor `C ⥤ (D ⥤ E)`.
 -/
-@[simps! obj_obj_obj obj_obj_map obj_map_app map_app_app]
+@[implicit_reducible, simps! obj_obj_obj obj_obj_map obj_map_app map_app_app]
 def curry : (C × D ⥤ E) ⥤ C ⥤ D ⥤ E where
   obj F := curryObj F
   map T :=
@@ -81,12 +82,10 @@ def curry : (C × D ⥤ E) ⥤ C ⥤ D ⥤ E where
         ext; dsimp [curryObj]
         rw [NatTrans.naturality] }
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 -- create projection simp lemmas even though this isn't a `{ .. }`.
 /-- The equivalence of functor categories given by currying/uncurrying.
 -/
-@[simps!]
+@[implicit_reducible, simps!]
 def currying : C ⥤ D ⥤ E ≌ C × D ⥤ E where
   functor := uncurry
   inverse := curry
@@ -98,10 +97,8 @@ def currying : C ⥤ D ⥤ E ≌ C × D ⥤ E where
       dsimp at f₁ f₂ ⊢
       simp only [← F.map_comp, prod_comp, Category.comp_id, Category.id_comp]))
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 /-- The equivalence of functor categories given by flipping. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def flipping : C ⥤ D ⥤ E ≌ D ⥤ C ⥤ E where
   functor := flipFunctor _ _ _
   inverse := flipFunctor _ _ _
@@ -132,8 +129,6 @@ instance : (uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E).Full :=
 instance : (uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E).Faithful :=
   fullyFaithfulUncurry.faithful
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 /-- Given functors `F₁ : C ⥤ D`, `F₂ : C' ⥤ D'` and `G : D × D' ⥤ E`, this is the isomorphism
 between `curry.obj ((F₁.prod F₂).comp G)` and
 `F₁ ⋙ curry.obj G ⋙ (whiskeringLeft C' D' E).obj F₂` in the category `C ⥤ C' ⥤ E`. -/
@@ -144,37 +139,29 @@ def curryObjProdComp {C' D' : Type*} [Category* C'] [Category* D']
       F₁ ⋙ curry.obj G ⋙ (whiskeringLeft C' D' E).obj F₂ :=
   NatIso.ofComponents (fun X₁ ↦ NatIso.ofComponents (fun X₂ ↦ Iso.refl _))
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 /-- `F.flip` is isomorphic to uncurrying `F`, swapping the variables, and currying. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def flipIsoCurrySwapUncurry (F : C ⥤ D ⥤ E) : F.flip ≅ curry.obj (Prod.swap _ _ ⋙ uncurry.obj F) :=
   NatIso.ofComponents fun d => NatIso.ofComponents fun _ => Iso.refl _
 
-set_option backward.defeqAttrib.useBackward true in
 /-- The uncurrying of `F.flip` is isomorphic to
 swapping the factors followed by the uncurrying of `F`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def uncurryObjFlip (F : C ⥤ D ⥤ E) : uncurry.obj F.flip ≅ Prod.swap _ _ ⋙ uncurry.obj F :=
   NatIso.ofComponents fun _ => Iso.refl _
 
 variable (B C D E)
 
-#adaptation_note
-/-- `respectTransparency.types true` changes the auto-generated lemmas' signature -/
-set_option backward.isDefEq.respectTransparency.types false in
 /-- A version of `CategoryTheory.whiskeringRight` for bifunctors, obtained by uncurrying,
 applying `whiskeringRight` and currying back
 -/
-@[simps!]
+@[implicit_reducible, simps!]
 def whiskeringRight₂ : (C ⥤ D ⥤ E) ⥤ (B ⥤ C) ⥤ (B ⥤ D) ⥤ B ⥤ E :=
   uncurry ⋙
     whiskeringRight _ _ _ ⋙ (whiskeringLeft _ _ _).obj (prodFunctorToFunctorProd _ _ _) ⋙ curry
 
 variable {B C D E}
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 lemma uncurry_obj_curry_obj (F : B × C ⥤ D) : uncurry.obj (curry.obj F) = F :=
   Functor.ext (by simp) (fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨f₁, f₂⟩ => by
     dsimp
@@ -184,8 +171,6 @@ lemma curry_obj_injective {F₁ F₂ : C × D ⥤ E} (h : curry.obj F₁ = curry
     F₁ = F₂ := by
   rw [← uncurry_obj_curry_obj F₁, ← uncurry_obj_curry_obj F₂, h]
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 lemma curry_obj_uncurry_obj (F : B ⥤ C ⥤ D) : curry.obj (uncurry.obj F) = F :=
   Functor.ext (fun _ => Functor.ext (by simp) (by simp)) (by cat_disch)
 
@@ -199,16 +184,12 @@ lemma flip_injective {F₁ F₂ : B ⥤ C ⥤ D} (h : F₁.flip = F₂.flip) :
     F₁ = F₂ := by
   rw [← flip_flip F₁, ← flip_flip F₂, h]
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 lemma uncurry_obj_curry_obj_flip_flip (F₁ : B ⥤ C) (F₂ : D ⥤ E) (G : C × E ⥤ H) :
     uncurry.obj (F₂ ⋙ (F₁ ⋙ curry.obj G).flip).flip = (F₁.prod F₂) ⋙ G :=
   Functor.ext (by simp) (fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨f₁, f₂⟩ => by
     dsimp
     simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp])
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 lemma uncurry_obj_curry_obj_flip_flip' (F₁ : B ⥤ C) (F₂ : D ⥤ E) (G : C × E ⥤ H) :
     uncurry.obj (F₁ ⋙ (F₂ ⋙ (curry.obj G).flip).flip) = (F₁.prod F₂) ⋙ G :=
   Functor.ext (by simp) (fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨f₁, f₂⟩ => by
@@ -216,7 +197,7 @@ lemma uncurry_obj_curry_obj_flip_flip' (F₁ : B ⥤ C) (F₂ : D ⥤ E) (G : C
     simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp])
 
 /-- Natural isomorphism witnessing `comp_flip_uncurry_eq`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def compFlipUncurryIso (F : B ⥤ D) (G : D ⥤ C ⥤ E) :
     uncurry.obj (F ⋙ G).flip ≅ (𝟭 C).prod F ⋙ uncurry.obj G.flip := .refl _
 
@@ -224,7 +205,7 @@ lemma comp_flip_uncurry_eq (F : B ⥤ D) (G : D ⥤ C ⥤ E) :
     uncurry.obj (F ⋙ G).flip = (𝟭 C).prod F ⋙ uncurry.obj G.flip := rfl
 
 /-- Natural isomorphism witnessing `comp_flip_curry_eq`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def curryObjCompIso (F : C × B ⥤ D) (G : D ⥤ E) :
     (curry.obj (F ⋙ G)).flip ≅ (curry.obj F).flip ⋙ (whiskeringRight _ _ _).obj G := .refl _
 
@@ -233,7 +214,7 @@ lemma curry_obj_comp_flip (F : C × B ⥤ D) (G : D ⥤ E) :
       (curry.obj F).flip ⋙ (whiskeringRight _ _ _).obj G := rfl
 
 /-- The equivalence of types of bifunctors giving by flipping the arguments. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def flippingEquiv : C ⥤ D ⥤ E ≃ D ⥤ C ⥤ E where
   toFun F := F.flip
   invFun F := F.flip
@@ -241,7 +222,7 @@ def flippingEquiv : C ⥤ D ⥤ E ≃ D ⥤ C ⥤ E where
   right_inv _ := rfl
 
 /-- The equivalence of types of bifunctors given by currying. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def curryingEquiv : C ⥤ D ⥤ E ≃ C × D ⥤ E where
   toFun F := uncurry.obj F
   invFun G := curry.obj G
@@ -249,7 +230,7 @@ def curryingEquiv : C ⥤ D ⥤ E ≃ C × D ⥤ E where
   right_inv := uncurry_obj_curry_obj
 
 /-- The flipped equivalence of types of bifunctors given by currying. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def curryingFlipEquiv : D ⥤ C ⥤ E ≃ C × D ⥤ E :=
   flippingEquiv.trans curryingEquiv
 
diff --git a/Mathlib/CategoryTheory/Iso.lean b/Mathlib/CategoryTheory/Iso.lean
index 24aca08503..2cb8120023 100644
--- a/Mathlib/CategoryTheory/Iso.lean
+++ b/Mathlib/CategoryTheory/Iso.lean
@@ -83,7 +83,7 @@ theorem ext ⦃α β : X ≅ Y⦄ (w : α.hom = β.hom) : α = β :=
     _     = β.inv                 := by grind
 
 /-- Inverse isomorphism. -/
-@[symm]
+@[symm, implicit_reducible]
 def symm (I : X ≅ Y) : Y ≅ X where
   hom := I.inv
   inv := I.hom
@@ -112,7 +112,7 @@ theorem nonempty_iso_symm (X Y : C) : Nonempty (X ≅ Y) ↔ Nonempty (Y ≅ X)
   ⟨fun h => ⟨h.some.symm⟩, fun h => ⟨h.some.symm⟩⟩
 
 /-- Identity isomorphism. -/
-@[refl, simps (attr := grind =)]
+@[refl, simps (attr := grind =), implicit_reducible]
 def refl (X : C) : X ≅ X where
   hom := 𝟙 X
   inv := 𝟙 X
@@ -127,7 +127,7 @@ theorem nonempty_iso_refl (X : C) : Nonempty (X ≅ X) := ⟨default⟩
 theorem refl_symm (X : C) : (Iso.refl X).symm = Iso.refl X := rfl
 
 /-- Composition of two isomorphisms -/
-@[simps (attr := grind =)]
+@[simps (attr := grind =), implicit_reducible]
 def trans (α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z where
   hom := α.hom ≫ β.hom
   inv := β.inv ≫ α.inv
@@ -219,7 +219,7 @@ theorem hom_eq_inv (α : X ≅ Y) (β : Y ≅ X) : α.hom = β.inv ↔ β.hom =
 attribute [local grind] Function.LeftInverse Function.RightInverse
 
 /-- The bijection `(Z ⟶ X) ≃ (Z ⟶ Y)` induced by `α : X ≅ Y`. -/
-@[to_dual (attr := simps) homFromEquiv
+@[implicit_reducible, to_dual (attr := simps) homFromEquiv
 /-- The bijection `(X ⟶ Z) ≃ (Y ⟶ Z)` induced by `α : X ≅ Y`. -/]
 def homToEquiv (α : X ≅ Y) {Z : C} : (Z ⟶ X) ≃ (Z ⟶ Y) where
   toFun f := f ≫ α.hom
@@ -469,7 +469,7 @@ variable {D : Type u₂}
 variable [Category.{v₂} D]
 
 /-- A functor `F : C ⥤ D` sends isomorphisms `i : X ≅ Y` to isomorphisms `F.obj X ≅ F.obj Y` -/
-@[simps]
+@[simps, implicit_reducible]
 def mapIso (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : F.obj X ≅ F.obj Y where
   hom := F.map i.hom
   inv := F.map i.inv
diff --git a/Mathlib/CategoryTheory/NatIso.lean b/Mathlib/CategoryTheory/NatIso.lean
index f5393261e2..23a505d37e 100644
--- a/Mathlib/CategoryTheory/NatIso.lean
+++ b/Mathlib/CategoryTheory/NatIso.lean
@@ -176,7 +176,7 @@ set_option linter.translate.warnInvalid false in
 /-- Construct a natural isomorphism between functors by giving object level isomorphisms,
 and checking naturality only in the forward direction.
 -/
-@[to_dual (attr := simps (attr := grind =)) ofComponents'
+@[implicit_reducible, to_dual (attr := simps (attr := grind =)) ofComponents'
 /-- The dual of `ofComponents` -/]
 def ofComponents (app : ∀ X : C, F.obj X ≅ G.obj X)
     (naturality : ∀ {X Y : C} (f : X ⟶ Y),
diff --git a/Mathlib/CategoryTheory/Preadditive/Projective/Preserves.lean b/Mathlib/CategoryTheory/Preadditive/Projective/Preserves.lean
index 8bd387dfa4..e1cef58eec 100644
--- a/Mathlib/CategoryTheory/Preadditive/Projective/Preserves.lean
+++ b/Mathlib/CategoryTheory/Preadditive/Projective/Preserves.lean
@@ -12,7 +12,7 @@ public import Mathlib.CategoryTheory.Preadditive.Projective.Basic
 
 We define a typeclass `Functor.PreservesProjectiveObjects`.
 
-We restate the existing result that if `F ⊣ G` is an adjunction and `G` preserves monomorphisms,
+We restate the existing result that if `F ⊣ G` is an adjunction and `G` preserves epimorphisms,
 then `F` preserves projective objects. We show that the converse is true if the domain of `F` has
 enough projectives.
 -/
diff --git a/Mathlib/CategoryTheory/Products/Basic.lean b/Mathlib/CategoryTheory/Products/Basic.lean
index 67dcaa8d15..b528e8fa56 100644
--- a/Mathlib/CategoryTheory/Products/Basic.lean
+++ b/Mathlib/CategoryTheory/Products/Basic.lean
@@ -171,36 +171,34 @@ def sectR {C : Type u₁} [Category.{v₁} C] (Z : C) (D : Type u₂) [Category.
 variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
 
 /-- `fst` is the functor `(X, Y) ↦ X`. -/
-@[simps]
+@[implicit_reducible, simps]
 def fst : C × D ⥤ C where
   obj X := X.1
   map f := f.1
 
 /-- `snd` is the functor `(X, Y) ↦ Y`. -/
-@[simps]
+@[implicit_reducible, simps]
 def snd : C × D ⥤ D where
   obj X := X.2
   map f := f.2
 
 /-- The functor swapping the factors of a Cartesian product of categories, `C × D ⥤ D × C`. -/
-@[simps]
+@[implicit_reducible, simps]
 def swap : C × D ⥤ D × C where
   obj X := (X.2, X.1)
   map f := f.2 ×ₘ f.1
 
-set_option backward.defeqAttrib.useBackward true in
 /-- Swapping the factors of a Cartesian product of categories twice is naturally isomorphic
 to the identity functor.
 -/
-@[simps]
+@[implicit_reducible, simps]
 def symmetry : swap C D ⋙ swap D C ≅ 𝟭 (C × D) where
   hom := { app := fun X => 𝟙 X }
   inv := { app := fun X => 𝟙 X }
 
-set_option backward.defeqAttrib.useBackward true in
 /-- The equivalence, given by swapping factors, between `C × D` and `D × C`.
 -/
-@[simps]
+@[implicit_reducible, simps]
 def braiding : C × D ≌ D × C where
   functor := swap C D
   inverse := swap D C
@@ -243,16 +241,15 @@ def evaluation : C ⥤ (C ⥤ D) ⥤ D where
 /-- The "evaluation of `F` at `X`" functor,
 as a functor `C × (C ⥤ D) ⥤ D`.
 -/
-@[simps]
+@[implicit_reducible, simps]
 def evaluationUncurried : C × (C ⥤ D) ⥤ D where
   obj p := p.2.obj p.1
   map := fun {x} {y} f => x.2.map f.1 ≫ f.2.app y.1
 
 variable {C}
 
-set_option backward.defeqAttrib.useBackward true in
 /-- The constant functor followed by the evaluation functor is just the identity. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def Functor.constCompEvaluationObj (X : C) : Functor.const C ⋙ (evaluation C D).obj X ≅ 𝟭 D :=
   NatIso.ofComponents fun _ => Iso.refl _
 
@@ -272,20 +269,18 @@ def prod (F : A ⥤ B) (G : C ⥤ D) : A × C ⥤ B × D where
 /- Because of limitations in Lean 3's handling of notations, we do not setup a notation `F × G`.
 You can use `F.prod G` as a "poor man's infix", or just write `functor.prod F G`. -/
 /-- Similar to `prod`, but both functors start from the same category `A` -/
-@[simps]
+@[implicit_reducible, simps]
 def prod' (F : A ⥤ B) (G : A ⥤ C) : A ⥤ B × C where
   obj a := (F.obj a, G.obj a)
   map f := F.map f ×ₘ G.map f
 
-set_option backward.defeqAttrib.useBackward true in
 /-- The product `F.prod' G` followed by projection on the first component is isomorphic to `F` -/
-@[simps!]
+@[implicit_reducible, simps!]
 def prod'CompFst (F : A ⥤ B) (G : A ⥤ C) : F.prod' G ⋙ CategoryTheory.Prod.fst B C ≅ F :=
   NatIso.ofComponents fun _ => Iso.refl _
 
-set_option backward.defeqAttrib.useBackward true in
 /-- The product `F.prod' G` followed by projection on the second component is isomorphic to `G` -/
-@[simps!]
+@[implicit_reducible, simps!]
 def prod'CompSnd (F : A ⥤ B) (G : A ⥤ C) : F.prod' G ⋙ CategoryTheory.Prod.snd B C ≅ G :=
   NatIso.ofComponents fun _ => Iso.refl _
 
@@ -294,7 +289,7 @@ section
 variable (C)
 
 /-- The diagonal functor. -/
-@[simps! obj map]
+@[implicit_reducible, simps! obj map]
 def diag : C ⥤ C × C :=
   (𝟭 C).prod' (𝟭 C)
 
@@ -304,36 +299,32 @@ end Functor
 
 namespace NatTrans
 
-set_option backward.defeqAttrib.useBackward true in
 /-- The Cartesian product of two natural transformations. -/
-@[simps! app_fst app_snd]
+@[implicit_reducible, simps! app_fst app_snd]
 def prod {F G : A ⥤ B} {H I : C ⥤ D} (α : F ⟶ G) (β : H ⟶ I) : F.prod H ⟶ G.prod I where
   app X := α.app X.1 ×ₘ β.app X.2
 
 /- Again, it is inadvisable in Lean 3 to setup a notation `α × β`;
 use instead `α.prod β` or `NatTrans.prod α β`. -/
 
-set_option backward.defeqAttrib.useBackward true in
 /-- The Cartesian product of two natural transformations where both functors have the
 same source. -/
-@[simps! app_fst app_snd]
+@[implicit_reducible, simps! app_fst app_snd]
 def prod' {F G : A ⥤ B} {H K : A ⥤ C} (α : F ⟶ G) (β : H ⟶ K) : F.prod' H ⟶ G.prod' K where
   app X := α.app X ×ₘ β.app X
 
 end NatTrans
 
 /-- The Cartesian product functor between functor categories -/
-@[simps]
+@[implicit_reducible, simps]
 def prodFunctor : (A ⥤ B) × (C ⥤ D) ⥤ A × C ⥤ B × D where
   obj FG := FG.1.prod FG.2
   map nm := NatTrans.prod nm.1 nm.2
 
 namespace NatIso
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 /-- The Cartesian product of two natural isomorphisms. -/
-@[simps]
+@[implicit_reducible, simps]
 def prod {F F' : A ⥤ B} {G G' : C ⥤ D} (e₁ : F ≅ F') (e₂ : G ≅ G') :
     F.prod G ≅ F'.prod G' where
   hom := NatTrans.prod e₁.hom e₂.hom
@@ -343,10 +334,8 @@ end NatIso
 
 namespace Equivalence
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 /-- The Cartesian product of two equivalences of categories. -/
-@[simps]
+@[implicit_reducible, simps]
 def prod (E₁ : A ≌ B) (E₂ : C ≌ D) : A × C ≌ B × D where
   functor := E₁.functor.prod E₂.functor
   inverse := E₁.inverse.prod E₂.inverse
@@ -355,18 +344,16 @@ def prod (E₁ : A ≌ B) (E₂ : C ≌ D) : A × C ≌ B × D where
 
 end Equivalence
 
-set_option backward.defeqAttrib.useBackward true in
 /-- `F.flip` composed with evaluation is the same as evaluating `F`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def flipCompEvaluation (F : A ⥤ B ⥤ C) (a) : F.flip ⋙ (evaluation _ _).obj a ≅ F.obj a :=
   NatIso.ofComponents fun b => Iso.refl _
 
 theorem flip_comp_evaluation (F : A ⥤ B ⥤ C) (a) : F.flip ⋙ (evaluation _ _).obj a = F.obj a :=
   rfl
 
-set_option backward.defeqAttrib.useBackward true in
 /-- `F` composed with evaluation is the same as evaluating `F.flip`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def compEvaluation (F : A ⥤ B ⥤ C) (b) : F ⋙ (evaluation _ _).obj b ≅ F.flip.obj b :=
   NatIso.ofComponents fun a => Iso.refl _
 
@@ -374,7 +361,7 @@ theorem comp_evaluation (F : A ⥤ B ⥤ C) (b) : F ⋙ (evaluation _ _).obj b =
   rfl
 
 /-- Whiskering by `F` and then evaluating at `a` is the same as evaluating at `F.obj a`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def whiskeringLeftCompEvaluation (F : A ⥤ B) (a : A) :
     (whiskeringLeft A B C).obj F ⋙ (evaluation A C).obj a ≅ (evaluation B C).obj (F.obj a) :=
   Iso.refl _
@@ -387,7 +374,7 @@ theorem whiskeringLeft_comp_evaluation (F : A ⥤ B) (a : A) :
 
 /-- Whiskering by `F` and then evaluating at `a` is the same as evaluating at `F` and then
 applying `F`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def whiskeringRightCompEvaluation (F : B ⥤ C) (a : A) :
     (whiskeringRight A B C).obj F ⋙ (evaluation _ _).obj a ≅ (evaluation _ _).obj a ⋙ F :=
   Iso.refl _
@@ -402,39 +389,33 @@ theorem whiskeringRight_comp_evaluation (F : B ⥤ C) (a : A) :
 variable (A B C)
 
 /-- The forward direction for `functorProdFunctorEquiv` -/
-@[simps]
+@[implicit_reducible, simps]
 def prodFunctorToFunctorProd : (A ⥤ B) × (A ⥤ C) ⥤ A ⥤ B × C where
   obj F := F.1.prod' F.2
   map {F G} f := NatTrans.prod' f.1 f.2
 
 /-- The backward direction for `functorProdFunctorEquiv` -/
-@[simps]
+@[implicit_reducible, simps]
 def functorProdToProdFunctor : (A ⥤ B × C) ⥤ (A ⥤ B) × (A ⥤ C) where
   obj F := ⟨F ⋙ CategoryTheory.Prod.fst B C, F ⋙ CategoryTheory.Prod.snd B C⟩
   map α := whiskerRight α _ ×ₘ whiskerRight α _
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 /-- The unit isomorphism for `functorProdFunctorEquiv` -/
-@[simps!]
+@[implicit_reducible, simps!]
 def functorProdFunctorEquivUnitIso :
     𝟭 _ ≅ prodFunctorToFunctorProd A B C ⋙ functorProdToProdFunctor A B C :=
   NatIso.ofComponents (fun F =>
     Functor.prod'CompFst F.fst F.snd |>.prod (Functor.prod'CompSnd F.fst F.snd) |>.trans
       (prod.etaIso F) |>.symm)
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 /-- The counit isomorphism for `functorProdFunctorEquiv` -/
-@[simps!]
+@[implicit_reducible, simps!]
 def functorProdFunctorEquivCounitIso :
     functorProdToProdFunctor A B C ⋙ prodFunctorToFunctorProd A B C ≅ 𝟭 _ :=
   NatIso.ofComponents fun F => NatIso.ofComponents fun X => prod.etaIso (F.obj X)
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 /-- The equivalence of categories between `(A ⥤ B) × (A ⥤ C)` and `A ⥤ (B × C)` -/
-@[simps]
+@[implicit_reducible, simps]
 def functorProdFunctorEquiv : (A ⥤ B) × (A ⥤ C) ≌ A ⥤ B × C :=
   { functor := prodFunctorToFunctorProd A B C,
     inverse := functorProdToProdFunctor A B C,
@@ -446,7 +427,7 @@ section Opposite
 open Opposite
 
 /-- The equivalence between the opposite of a product and the product of the opposites. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def prodOpEquiv : (C × D)ᵒᵖ ≌ Cᵒᵖ × Dᵒᵖ where
   functor :=
     { obj := fun X ↦ ⟨op X.unop.1, op X.unop.2⟩,
diff --git a/Mathlib/CategoryTheory/Shift/CommShiftTwo.lean b/Mathlib/CategoryTheory/Shift/CommShiftTwo.lean
index f9a6e80269..daec21fca9 100644
--- a/Mathlib/CategoryTheory/Shift/CommShiftTwo.lean
+++ b/Mathlib/CategoryTheory/Shift/CommShiftTwo.lean
@@ -115,7 +115,6 @@ attribute [instance_reducible] commShiftObj commShiftFlipObj
 attribute [instance] commShiftObj commShiftFlipObj commShift_map commShift_flip_map
 
 set_option backward.defeqAttrib.useBackward true in
-set_option backward.inferInstanceAs.wrap.data false in
 set_option backward.isDefEq.respectTransparency false in
 instance precomp₁ {M : Type*} [AddCommMonoid M] [HasShift C₁ M] [HasShift C₁' M]
     [HasShift C₂ M] [HasShift D M] (F : C₁' ⥤ C₁) [F.CommShift M]
@@ -123,7 +122,7 @@ instance precomp₁ {M : Type*} [AddCommMonoid M] [HasShift C₁ M] [HasShift C
     (F ⋙ G).CommShift₂ h where
   commShiftObj (X₁' : C₁') := inferInstanceAs ((G.obj (F.obj X₁')).CommShift M)
   commShift_map {X₁' Y₁' : C₁'} (f : X₁' ⟶ Y₁') := by dsimp; infer_instance
-  commShiftFlipObj (X₂ : C₂) := inferInstanceAs ((F ⋙ G.flip.obj X₂).CommShift M)
+  commShiftFlipObj (X₂ : C₂) := CommShift.comp F (G.flip.obj X₂)
   commShift_flip_map {X₂ Y₂ : C₂} (g : X₂ ⟶ Y₂) :=
     inferInstanceAs (NatTrans.CommShift (whiskerLeft F (G.flip.map g)) M)
   comm X₁' X₂ m n := by
@@ -135,12 +134,11 @@ instance precomp₁ {M : Type*} [AddCommMonoid M] [HasShift C₁ M] [HasShift C
 
 set_option backward.isDefEq.respectTransparency.types false in
 set_option backward.defeqAttrib.useBackward true in
-set_option backward.inferInstanceAs.wrap false in
 instance precomp₂ {M : Type*} [AddCommMonoid M] [HasShift C₁ M] [HasShift C₂' M]
     [HasShift C₂ M] [HasShift D M] (F : C₂' ⥤ C₂) [F.CommShift M]
     (G : C₁ ⥤ C₂ ⥤ D) (h : CommShift₂Setup D M) [G.CommShift₂ h] :
     (G ⋙ (whiskeringLeft C₂' C₂ D).obj F).CommShift₂ h where
-  commShiftObj (X₁ : C₁) := inferInstanceAs ((F ⋙ G.obj X₁).CommShift M)
+  commShiftObj (X₁ : C₁) := CommShift.comp F (G.obj X₁)
   commShift_map {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) := by dsimp; infer_instance
   commShiftFlipObj (X₂' : C₂') := inferInstanceAs ((G.flip.obj (F.obj X₂')).CommShift M)
   commShift_flip_map {X₂' Y₂' : C₂'} (g : X₂' ⟶ Y₂') :=
diff --git a/Mathlib/CategoryTheory/ShrinkYoneda.lean b/Mathlib/CategoryTheory/ShrinkYoneda.lean
index e73c03841d..02d6f534fe 100644
--- a/Mathlib/CategoryTheory/ShrinkYoneda.lean
+++ b/Mathlib/CategoryTheory/ShrinkYoneda.lean
@@ -36,16 +36,15 @@ protected abbrev Small (F : C ⥤ Type w') := ∀ (X : C), _root_.Small.{w} (F.o
 
 /-- If a functor `F : C ⥤ Type w'` is `w`-small, this is the functor `C ⥤ Type w`
 obtained by shrinking `F.obj X` for all `X : C`. -/
-@[simps obj map, pp_with_univ]
+@[implicit_reducible, simps obj map, pp_with_univ]
 noncomputable def shrink (F : C ⥤ Type w') [FunctorToTypes.Small.{w} F] :
     C ⥤ Type w where
   obj X := Shrink.{w} (F.obj X)
   map f := ↾(equivShrink.{w} _ ∘ F.map f ∘ (equivShrink.{w} _).symm)
 
-set_option backward.defeqAttrib.useBackward true in
 /-- The natural transformation `shrink.{w} F ⟶ shrink.{w} G` induces by a natural
 transformation `τ : F ⟶ G` between `w`-small functors to types. -/
-@[simps]
+@[implicit_reducible, simps]
 noncomputable def shrinkMap {F G : C ⥤ Type w'} (τ : F ⟶ G) [FunctorToTypes.Small.{w} F]
     [FunctorToTypes.Small.{w} G] :
     shrink.{w} F ⟶ shrink.{w} G where
@@ -75,7 +74,6 @@ set_option backward.defeqAttrib.useBackward true in
 instance (X : C) : FunctorToTypes.Small.{w} (yoneda.obj X) :=
   fun _ ↦ by dsimp; infer_instance
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- The Yoneda embedding `C ⥤ Cᵒᵖ ⥤ Type w` for a locally `w`-small category `C`. -/
 @[simps -isSimp obj map, pp_with_univ]
 noncomputable def shrinkYoneda :
@@ -385,7 +383,8 @@ noncomputable def fullyFaithfulShrinkCoyoneda :
   map_preimage f := by
     obtain ⟨f, rfl⟩ := shrinkCoyonedaEquiv.symm.surjective f
     cat_disch
-  preimage_map f := by simp [shrinkCoyonedaEquiv_shrinkCoyoneda_map]
+  preimage_map f := by
+    simp [shrinkCoyonedaEquiv_shrinkCoyoneda_map f]
 
 instance : (shrinkCoyoneda.{w} (C := C)).Faithful := (fullyFaithfulShrinkCoyoneda C).faithful
 
diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean
index 43e3c24542..0f43ae85c1 100644
--- a/Mathlib/CategoryTheory/Yoneda.lean
+++ b/Mathlib/CategoryTheory/Yoneda.lean
@@ -39,7 +39,7 @@ universe w v v₁ v₂ u₁ u₂
 variable {C : Type u₁} [Category.{v₁} C]
 
 /-- The Yoneda embedding, as a functor from `C` into presheaves on `C`. -/
-@[simps obj_obj obj_map map_app, stacks 001O]
+@[implicit_reducible, simps obj_obj obj_map map_app, stacks 001O]
 def yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁ where
   obj X :=
     { obj Y := (unop Y) ⟶ X
@@ -720,6 +720,7 @@ variable {C}
 /-- We have a type-level equivalence between natural transformations from the yoneda embedding
 and elements of `F.obj X`, without any universe switching.
 -/
+@[implicit_reducible]
 def yonedaEquiv {X : C} {F : Cᵒᵖ ⥤ Type v₁} : (yoneda.obj X ⟶ F) ≃ F.obj (op X) where
   toFun η := η.app (op X) (𝟙 X)
   invFun ξ := { app _ := ↾fun f ↦ F.map f.op ξ }
@@ -739,7 +740,7 @@ theorem yonedaEquiv_symm_app {X : C} {F : Cᵒᵖ ⥤ Type v₁} (x : F.obj (op
   rfl
 
 theorem yonedaEquiv_symm_app_apply {X : C} {F : Cᵒᵖ ⥤ Type v₁} (x : F.obj (op X)) (Y : Cᵒᵖ)
-    (f : Y.unop ⟶ X) : (yonedaEquiv.symm x).app Y f = F.map f.op x :=
+    (f : Y.unop ⟶ X) : dsimp% (yonedaEquiv.symm x).app Y f = F.map f.op x :=
   rfl
 
 /-- See also `yonedaEquiv_naturality'` for a more general version. -/
@@ -1000,6 +1001,7 @@ variable {C}
 /-- We have a type-level equivalence between natural transformations from the coyoneda embedding
 and elements of `F.obj X.unop`, without any universe switching.
 -/
+@[implicit_reducible]
 def coyonedaEquiv {X : C} {F : C ⥤ Type v₁} : (coyoneda.obj (op X) ⟶ F) ≃ F.obj X where
   toFun η := η.app X (𝟙 X)
   invFun ξ := { app _ := ↾fun x ↦ F.map x ξ }
@@ -1014,7 +1016,7 @@ theorem coyonedaEquiv_apply {X : C} {F : C ⥤ Type v₁} (f : coyoneda.obj (op
 
 @[simp]
 theorem coyonedaEquiv_symm_app_apply {X : C} {F : C ⥤ Type v₁} (x : F.obj X) (Y : C)
-    (f : X ⟶ Y) : (coyonedaEquiv.symm x).app Y f = F.map f x :=
+    (f : X ⟶ Y) : dsimp% (coyonedaEquiv.symm x).app Y f = F.map f x :=
   rfl
 
 lemma coyonedaEquiv_naturality {X Y : C} {F : C ⥤ Type v₁} (f : coyoneda.obj (op X) ⟶ F)
diff --git a/Mathlib/Combinatorics/Quiver/Basic.lean b/Mathlib/Combinatorics/Quiver/Basic.lean
index 85d6377076..0fa3bb7291 100644
--- a/Mathlib/Combinatorics/Quiver/Basic.lean
+++ b/Mathlib/Combinatorics/Quiver/Basic.lean
@@ -55,11 +55,11 @@ instance opposite {V} [Quiver V] : Quiver Vᵒᵖ :=
   ⟨fun a b => (unop b ⟶ unop a)ᵒᵖ⟩
 
 /-- The opposite of an arrow in `V`. -/
-@[to_dual self]
+@[implicit_reducible, to_dual self]
 def Hom.op {V} [Quiver V] {X Y : V} (f : X ⟶ Y) : op Y ⟶ op X := ⟨f⟩
 
 /-- Given an arrow in `Vᵒᵖ`, we can take the "unopposite" back in `V`. -/
-@[to_dual self]
+@[implicit_reducible, to_dual self]
 def Hom.unop {V} [Quiver V] {X Y : Vᵒᵖ} (f : X ⟶ Y) : unop Y ⟶ unop X := Opposite.unop f
 
 /-- The bijection `(X ⟶ Y) ≃ (op Y ⟶ op X)`. -/
diff --git a/Mathlib/Data/Finsupp/MonomialOrder.lean b/Mathlib/Data/Finsupp/MonomialOrder.lean
index 551bdf44f3..9e49002bae 100644
--- a/Mathlib/Data/Finsupp/MonomialOrder.lean
+++ b/Mathlib/Data/Finsupp/MonomialOrder.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Data.Finsupp.Lex
 public import Mathlib.Data.Finsupp.WellFounded
 public import Mathlib.Data.List.TFAE
+public import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
 
 /-! # Monomial orders
 
@@ -95,6 +96,9 @@ instance isOrderedCancelAddMonoid_syn : IsOrderedCancelAddMonoid m.syn :=
 
 @[deprecated (since := "2026-07-07")] alias iocam := MonomialOrder.isOrderedCancelAddMonoid_syn
 
+/-- A `WithBot m.syn` version of `m.toSyn`. -/
+noncomputable def toWithBotSyn : WithBot (σ →₀ ℕ) ≃+ WithBot m.syn := m.toSyn.withBotCongr
+
 lemma le_add_right (a b : σ →₀ ℕ) :
     m.toSyn a ≤ m.toSyn a + m.toSyn b := by
   rw [← map_add]
@@ -123,6 +127,32 @@ lemma toSyn_lt_iff_ne_zero {a : m.syn} :
 lemma toSyn_strictMono : StrictMono (m.toSyn) := by
   apply m.toSyn_monotone.strictMono_of_injective m.toSyn.injective
 
+@[simp]
+lemma toWithBotSyn_apply_bot : m.toWithBotSyn ⊥ = ⊥ := rfl
+
+@[simp]
+lemma toWithBotSyn_symm_apply_bot : m.toWithBotSyn.symm ⊥ = ⊥ := rfl
+
+@[simp]
+lemma toWithBotSyn_apply_eq_bot_iff (a) : m.toWithBotSyn a = ⊥ ↔ a = ⊥ := by
+  simp [← m.toWithBotSyn.eq_symm_apply]
+
+lemma toWithBotSyn_apply_le_bot_iff (a) : m.toWithBotSyn a ≤ ⊥ ↔ a = ⊥ := by
+  simp
+
+@[simp]
+lemma toWithBotSyn_apply_coe (a : σ →₀ ℕ) : m.toWithBotSyn a = m.toSyn a := rfl
+
+@[simp]
+lemma bot_lt_toWithBotSyn_apply_iff (a) : ⊥ < m.toWithBotSyn a ↔ ⊥ < a := by
+  simp [bot_lt_iff_ne_bot]
+
+@[simp]
+lemma toWithBotSyn_symm_apply_eq_bot (a) : m.toWithBotSyn.symm a = ⊥ ↔ a = ⊥ := by
+  simp [m.toWithBotSyn.symm_apply_eq]
+
+lemma toWithBotSyn_apply (a : WithBot (σ →₀ ℕ)) : m.toWithBotSyn a = a.map m.toSyn := rfl
+
 /-- Given a monomial order, notation for the corresponding strict order relation on `σ →₀ ℕ` -/
 scoped
 notation:50 c " ≺[" m:25 "] " d:50 => (MonomialOrder.toSyn m c < MonomialOrder.toSyn m d)
@@ -131,6 +161,18 @@ notation:50 c " ≺[" m:25 "] " d:50 => (MonomialOrder.toSyn m c < MonomialOrder
 scoped
 notation:50 c " ≼[" m:25 "] " d:50 => (MonomialOrder.toSyn m c ≤ MonomialOrder.toSyn m d)
 
+/-- Given a monomial order with bot, notation for the corresponding strict order relation on
+`WithBot (σ →₀ ℕ)` -/
+scoped
+notation:50 c " ≺'[" m:25 "] " d:50 =>
+  (MonomialOrder.toWithBotSyn m c < MonomialOrder.toWithBotSyn m d)
+
+/-- Given a monomial order with bot, notation for the corresponding order relation on
+`WithBot (σ →₀ ℕ)` -/
+scoped
+notation:50 c " ≼'[" m:25 "] " d:50 =>
+  (MonomialOrder.toWithBotSyn m c ≤ MonomialOrder.toWithBotSyn m d)
+
 end MonomialOrder
 
 section Lex
diff --git a/Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean b/Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
index 049f199d56..4a110d6e96 100644
--- a/Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
+++ b/Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
@@ -16,7 +16,9 @@ public import Mathlib.RingTheory.MvPolynomial.Homogeneous
 We consider a type `σ` of indeterminates and a commutative semiring `R`
 and a monomial order `m : MonomialOrder σ`.
 
-* `m.degree f` is the degree of `f` for the monomial ordering `m`.
+* `m.degree f` is the degree of `f` for the monomial ordering `m`, where the polynomial `0` has
+  degree `0`. For the variant mapping polynomial `0` to `⊥` which is less than `0`, see
+  `MonomialOrder.withBotDegree`.
 
 * `m.leadingCoeff f` is the leading coefficient of `f` for the monomial ordering `m`.
 
@@ -26,6 +28,10 @@ and a monomial order `m : MonomialOrder σ`.
 
 * `m.sPolynomial f g` is S-polynomial of `f` and `g`.
 
+* `m.withBotDegree f` is the degree of `f` for the monomial ordering `m`, where the polynomial `0`
+  has degree `⊥`, which is not equal to `0`. `MonomialOrder.withBotDegree` is to
+  `MonomialOrder.degree` as `Polynomial.degree` is to `Polynomial.natDegree`.
+
 * `m.leadingCoeff_ne_zero_iff f` asserts that this coefficient is nonzero iff `f ≠ 0`.
 
 * in a field, `m.isUnit_leadingCoeff f` asserts that this coefficient is a unit iff `f ≠ 0`.
@@ -104,7 +110,9 @@ section Semiring
 variable {R : Type*} [CommSemiring R]
 
 variable (m) in
-/-- the degree of a multivariate polynomial with respect to a monomial ordering -/
+/-- the degree of a multivariate polynomial with respect to a monomial ordering, where the
+polynomial `0` has degree `0`. For the variant mapping polynomial `0` to `⊥` which is less than
+`0`, see `MonomialOrder.withBotDegree`. -/
 noncomputable def degree (f : MvPolynomial σ R) : σ →₀ ℕ :=
   m.toSyn.symm (f.support.sup m.toSyn)
 
@@ -836,6 +844,195 @@ lemma mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors
   simp [← m.leadingCoeff_eq_zero_iff (f := f * g),
     m.leadingCoeff_mul_of_left_mem_nonZeroDivisors hf, mul_left_mem_nonZeroDivisors_eq_zero_iff hf]
 
+section withBotDegree
+
+variable (f g : MvPolynomial σ R)
+
+variable (m) in
+/-- the degree of a multivariate polynomial with respect to a monomial ordering, where polynomial
+`0` has degree `⊥`, which is not equal to `0`. `MonomialOrder.withBotDegree` is to
+`MonomialOrder.degree` as `Polynomial.degree` is to `Polynomial.natDegree`. -/
+noncomputable def withBotDegree : WithBot (σ →₀ ℕ) :=
+  f.support.image m.toSyn |>.max.map m.toSyn.symm
+
+lemma withBotDegree_eq [Decidable (f = 0)] :
+    m.withBotDegree f = if f = 0 then ⊥ else ↑(m.degree f) := by
+  simp [withBotDegree, degree]
+  by_cases hf : f = 0
+  · simp [hf]
+  · simp [hf, Finset.max_eq_sup_coe, ← Finset.coe_sup_of_nonempty _ (⇑m.toSyn)]
+
+@[simp]
+lemma withBotDegree_eq_coe_degree_iff : m.withBotDegree f = m.degree f ↔ f ≠ 0 := by
+  classical
+  simp [withBotDegree_eq]
+
+@[simp]
+lemma withBotDegree_eq_bot_iff : m.withBotDegree f = ⊥ ↔ f = 0 := by
+  classical
+  simp [withBotDegree_eq]
+
+lemma degree_eq_unbotD_withBotDegree : m.degree f = (m.withBotDegree f).unbotD 0 := by
+  classical
+  by_cases h : f = 0 <;> simp [withBotDegree_eq, h]
+
+@[simp]
+lemma withBotDegree_zero : m.withBotDegree (R := R) 0 = ⊥ := rfl
+
+lemma withBotDegree_monomial (d) (c) [Decidable (c = 0)] :
+    m.withBotDegree (R := R) (monomial d c) = if c = 0 then ⊥ else ↑d := by
+  classical
+  split_ifs <;> simp [withBotDegree_eq, *, m.degree_monomial]
+
+lemma withBotDegree_C (c) [Decidable (c = 0)] :
+    m.withBotDegree (R := R) (C c) = if c = 0 then ⊥ else 0 := by
+  simp [← monomial_zero', withBotDegree_monomial]
+
+@[simp]
+lemma withBotDegree_leadingTerm : m.withBotDegree (m.leadingTerm f) = m.withBotDegree f := by
+  classical
+  simp [withBotDegree_eq]
+
+@[simp]
+lemma withBotDegree_one [Nontrivial R] : m.withBotDegree (R := R) 1 = 0 := by
+  classical
+  simp [withBotDegree_eq]
+
+variable {f g} in
+lemma withBotDegree_mul_of_left_mem_nonZeroDivisors (hf : m.leadingCoeff f ∈ nonZeroDivisors _) :
+    m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g := by
+  classical
+  by_cases! h0 : f = 0 ∨ g = 0
+  · rcases h0 with h0 | h0 <;> simp [h0]
+  suffices f * g ≠ 0 by simp [withBotDegree_eq, m.degree_mul_of_left_mem_nonZeroDivisors hf, *]
+  apply mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors at hf
+  rw [mem_nonZeroDivisors_iff_left] at hf
+  tauto
+
+variable {f g} in
+lemma withBotDegree_mul_of_right_mem_nonZeroDivisors (hf : m.leadingCoeff g ∈ nonZeroDivisors _) :
+    m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g := by
+  rw [mul_comm, add_comm, withBotDegree_mul_of_left_mem_nonZeroDivisors (hf := hf)]
+
+@[simp]
+lemma withBotDegree_mul [NoZeroDivisors R] :
+    m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g := by
+  nontriviality R using Subsingleton.eq_zero (α := MvPolynomial σ R)
+  by_cases! hf : f = 0
+  · simp [hf]
+  rw [← m.leadingCoeff_ne_zero_iff, ← mem_nonZeroDivisors_iff_ne_zero] at hf
+  exact m.withBotDegree_mul_of_left_mem_nonZeroDivisors hf
+
+lemma withBotDegree_mul_le :
+    m.withBotDegree (f * g) ≼'[m] m.withBotDegree f + m.withBotDegree g := by
+  by_cases! h0 : f * g = 0
+  · simp [h0]
+  simp [-map_add, m.withBotDegree_eq_coe_degree_iff _ |>.mpr h0,
+    m.withBotDegree_eq_coe_degree_iff f |>.mpr (by grind),
+    m.withBotDegree_eq_coe_degree_iff g |>.mpr (by grind), ← WithBot.coe_add, m.degree_mul_le]
+
+lemma toWithBotSyn_withBotDegree_mul_le :
+    m.toWithBotSyn (m.withBotDegree (f * g)) ≤
+      m.toWithBotSyn (m.withBotDegree f) + m.toWithBotSyn (m.withBotDegree g) := by
+  by_cases h0 : f * g = 0
+  · simp [h0]
+  simp [m.withBotDegree_eq_coe_degree_iff f |>.mpr (by grind),
+    m.withBotDegree_eq_coe_degree_iff g |>.mpr (by grind),
+    m.withBotDegree_eq_coe_degree_iff _ |>.mpr h0, ← WithBot.coe_add,
+    m.toSyn_degree_mul_le]
+
+lemma withBotDegree_le_withBotDegree_iff :
+    m.withBotDegree f ≼'[m] m.withBotDegree g ↔
+      (m.degree f ≼[m] m.degree g ∧ (g = 0 → f = 0)) := by
+  classical
+  by_cases! +distrib h : f ≠ 0 ∧ g ≠ 0
+  · simp [m.withBotDegree_eq, h, m.toWithBotSyn_apply]
+  rcases h with h | _
+  · simp [h]
+  · aesop
+
+variable {g} in
+lemma withBotDegree_le_withBotDegree_iff_of_ne_zero (hg : g ≠ 0) :
+    m.withBotDegree f ≼'[m] m.withBotDegree g ↔ m.degree f ≼[m] m.degree g := by
+  simp [withBotDegree_le_withBotDegree_iff, hg]
+
+lemma withBotDegree_lt_withBotDegree_iff :
+    m.withBotDegree f ≺'[m] m.withBotDegree g ↔
+      (m.degree f ≺[m] m.degree g ∨ (f = 0 ∧ g ≠ 0)) := by
+  classical
+  by_cases! hg : g = 0
+  · simp_rw [toWithBotSyn_apply]
+    aesop
+  by_cases! hf : f = 0
+  · simp [hg, hf, bot_lt_iff_ne_bot, toWithBotSyn_apply]
+  simp [withBotDegree_eq, hf, hg, toWithBotSyn_apply]
+
+variable {f} in
+lemma withBotDegree_lt_withBotDegree_iff_of_ne_zero (hf : f ≠ 0) :
+    m.withBotDegree f ≺'[m] m.withBotDegree g ↔ m.degree f ≺[m] m.degree g := by
+  simp [withBotDegree_lt_withBotDegree_iff, hf]
+
+lemma withBotDegree_eq_withBotDegree_iff :
+    m.withBotDegree f = m.withBotDegree g ↔ (m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)) := by
+  classical
+  by_cases! +distrib h : f ≠ 0 ∧ g ≠ 0
+  · simp [h, m.withBotDegree_eq]
+  rcases h with h | h
+  all_goals
+    simp_rw [h]
+    revert f g
+    simp [m.withBotDegree_eq, m.degree_zero]
+
+lemma withBotDegree_add_le :
+    (m.toWithBotSyn <| m.withBotDegree (f + g)) ≤
+      (m.toWithBotSyn <| m.withBotDegree f) ⊔ (m.toWithBotSyn <| m.withBotDegree g) := by
+  by_cases! h : f = 0 ∨ g = 0
+  · rcases h with h | h <;> simp [h, m.toWithBotSyn_apply]
+  simpa [withBotDegree_le_withBotDegree_iff, h] using degree_add_le (R := R)
+
+variable {f g} in
+lemma withBotDegree_add_of_lt (h : m.withBotDegree g ≺'[m] m.withBotDegree f) :
+    m.withBotDegree (f + g) = m.withBotDegree f := by
+  by_cases hg : g = 0
+  · simp [hg]
+  simp only [withBotDegree_lt_withBotDegree_iff, hg, ne_eq, false_and, or_false] at h
+  simp only [withBotDegree_eq_withBotDegree_iff, show f ≠ 0 by contrapose h; simp [h], iff_false]
+  apply (show ∀ {p q}, p → (p → q) → (p ∧ q) by tauto) (m.degree_add_of_lt h)
+  intro h'
+  contrapose! h
+  simp [← h', h]
+
+variable {f g} in
+lemma withBotDegree_add_of_right_lt (h : m.withBotDegree f ≺'[m] m.withBotDegree g) :
+    m.withBotDegree (f + g) = m.withBotDegree g := by
+  rw [add_comm, withBotDegree_add_of_lt h]
+
+lemma withBotDegree_sum_le {α : Type*} {s : Finset α} {f : α → MvPolynomial σ R} :
+    (m.toWithBotSyn <| m.withBotDegree <| ∑ x ∈ s, f x) ≤
+      s.sup fun x ↦ (m.toWithBotSyn <| m.withBotDegree <| f x) := by
+  induction s using Finset.cons_induction_on with
+  | empty => simp
+  | cons a s haA h =>
+    rw [Finset.sum_cons, Finset.sup_cons]
+    exact le_trans (m.withBotDegree_add_le _ _) (max_le_max le_rfl h)
+
+variable {f} in
+lemma le_withBotDegree {d : σ →₀ ℕ} (hd : d ∈ f.support) :
+    d ≼'[m] m.withBotDegree f := by
+  classical
+  simp [withBotDegree_eq, toWithBotSyn_apply, ne_zero_iff.mpr ⟨d, by simpa using hd⟩, le_degree hd]
+
+variable {f g} in
+lemma withBotDegree_le_withBotDegree_of_support_subset
+    (h : f.support ⊆ g.support) :
+    m.withBotDegree f ≼'[m] m.withBotDegree g := by
+  by_cases hg : g = 0
+  · simpa [hg] using h
+  rw [m.withBotDegree_le_withBotDegree_iff_of_ne_zero _ hg]
+  exact m.degree_le_degree_of_support_subset h
+
+end withBotDegree
+
 end Semiring
 
 section Ring
@@ -1090,6 +1287,12 @@ lemma sPolynomial_decomposition {d : m.syn} {ι : Type*}
       obtain (⟨h, -⟩ | h) := hd b' hb' <;>
         simp [h, ← smul_eq_C_mul, smul_sub, ← mul_smul, mul_comm (m.leadingCoeff (g b'))]
 
+@[simp]
+lemma withBotDegree_neg (f : MvPolynomial σ R) :
+    m.withBotDegree (-f) = m.withBotDegree f := by
+  classical
+  simp [m.withBotDegree_eq]
+
 end Ring
 
 section Field
diff --git a/Mathlib/Tactic/Translate/Core.lean b/Mathlib/Tactic/Translate/Core.lean
index 2c7b61fedf..6e83933521 100644
--- a/Mathlib/Tactic/Translate/Core.lean
+++ b/Mathlib/Tactic/Translate/Core.lean
@@ -111,7 +111,7 @@ syntax bracketedOption := "(" attrOption <|> reorderOption <|>
 syntax translationHint := (ppSpace (&"existing" <|> &"self" <|> &"none"))?
 
 syntax attrArgs :=
-  translationHint (ppSpace bracketedOption)* (ppSpace ident)? (ppSpace (str <|> docComment))?
+  translationHint (ppSpace bracketedOption)* (ppSpace ident)? (ppSpace docComment)?
 
 -- We omit a doc-string on these syntaxes to instead show the `to_additive` or `to_dual` doc-string
 attribute [nolint docBlame] attrArgs bracketedOption
@@ -319,7 +319,7 @@ structure Config : Type where
   and the translate tactic auto-generates a name instead -/
   target : Name := Name.anonymous
   /-- An optional doc string. -/
-  doc : Option String := .none
+  doc : Option (TSyntax ``Lean.Parser.Command.docComment) := .none
   /-- If `allowAutoName` is `false` (default) then
   we check whether the given name can be auto-generated. -/
   allowAutoName : Bool := false
@@ -1151,30 +1151,6 @@ def elabTranslationAttr (declName : Name) (stx : Syntax) : CoreM Config := do
         Instead, you can write the attributes in the usual way."
     trace[translate_detail]
       "attributes: {attrs}; reorder arguments: {reorder?.elim "none" (·.toString)}"
-    let doc ← doc.mapM fun
-      | `(str|$doc:str) => open Linter in do
-        -- Deprecate `str` docstring syntax (since := "2025-08-12")
-        if getLinterValue linter.deprecated (← getLinterOptions) then
-          let hintSuggestion := {
-            diffGranularity := .none
-            toTryThisSuggestion := { suggestion := "/-- " ++ doc.getString.trimAscii ++ " -/" }
-          }
-          let sugg ← Hint.mkSuggestionsMessage #[hintSuggestion] doc
-            (codeActionPrefix? := "Update to: ") (forceList := false)
-          logWarningAt doc <| .tagged ``Linter.deprecatedAttr
-            m!"String syntax for `to_additive` docstrings is deprecated: Use \
-              docstring syntax instead (e.g. `@[to_additive /-- example -/]`)\n\
-              \n\
-              Update deprecated syntax to:{sugg}"
-        return doc.getString
-      | `(docComment|$doc:docComment) => do
-        -- TODO: rely on `addDocString`s call to `validateDocComment` after removing `str` support
-        validateDocComment doc
-        /- Note: the following replicates the behavior of `addDocString`. However, this means that
-        trailing whitespace might appear in docstrings added via `docComment` syntax when compared
-        to those added via `str` syntax. See this [Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Why.20do.20docstrings.20include.20trailing.20whitespace.3F/with/533553356). -/
-        return (← getDocStringText doc).removeLeadingSpaces
-      | _ => throwUnsupportedSyntax
     return {
       trace := !stx[1].isNone
       target := match tgt with | some tgt => tgt.getId | _ => Name.anonymous
@@ -1299,7 +1275,9 @@ partial def addTranslationAttr (t : TranslateData) (src : Name) (cfg : Config)
     -- tgt doesn't exist, so let's make it
     transformDeclRec t cfg src tgt src reorder cfg.rename
   if let some doc := cfg.doc then
-    addDocStringCore tgt doc
+    -- TODO: `Syntax.missing` means we do not add binders to the context,
+    -- so the docstring is going to have incomplete syntax highlighting.
+    addDocString tgt Syntax.missing doc |>.run'.run'
   let nestedNames ← copyMetaData t cfg src tgt
   -- add pop-up information when mousing over the given translated name
   -- (the information will be over the attribute if no translated name is given)
diff --git a/MathlibTest/Attribute/ToAdditive/Basic.lean b/MathlibTest/Attribute/ToAdditive/Basic.lean
index f9ee3c8b40..2be7a076c0 100644
--- a/MathlibTest/Attribute/ToAdditive/Basic.lean
+++ b/MathlibTest/Attribute/ToAdditive/Basic.lean
@@ -691,35 +691,14 @@ warning: `to_additive` did not change the type of theorem `mulTrivial`. Please r
 Note: This linter can be disabled with `set_option linter.translateRedundant false`
 -/
 #guard_msgs in
-@[to_additive /-- (via `docComment` syntax) I am an additive docstring! -/]
+@[to_additive /-- I am an additive docstring! -/]
 theorem mulTrivial : True := trivial
 
-/-- info: (via `docComment` syntax) I am an additive docstring! -/
+/-- info: I am an additive docstring! -/
 #guard_msgs in
 run_cmd
   let some doc ← findDocString? (← getEnv) ``addTrivial
-    | throwError "no `docComment` docstring found"
-  logInfo doc
-
-/--
-warning: String syntax for `to_additive` docstrings is deprecated: Use docstring syntax instead (e.g. `@[to_additive /-- example -/]`)
-
-Update deprecated syntax to:
-  [apply] /-- (via `str` syntax) I am an additive docstring! -/
----
-warning: `to_additive` did not change the type of theorem `mulTrivial'`. Please remove the attribute.
-
-Note: This linter can be disabled with `set_option linter.translateRedundant false`
--/
-#guard_msgs in
-@[to_additive "(via `str` syntax) I am an additive docstring!"]
-theorem mulTrivial' : True := trivial
-
-/-- info: (via `str` syntax) I am an additive docstring! -/
-#guard_msgs in
-run_cmd
-  let some doc ← findDocString? (← getEnv) ``addTrivial'
-    | throwError "no `str` docstring found"
+    | throwError "no docstring found"
   logInfo doc
 
 /-! Test handling of noncomputability -/
diff --git a/MathlibTest/CategoryTheory/CheckDsimp.lean b/MathlibTest/CategoryTheory/CheckDsimp.lean
new file mode 100644
index 0000000000..f650ae1028
--- /dev/null
+++ b/MathlibTest/CategoryTheory/CheckDsimp.lean
@@ -0,0 +1,85 @@
+import Mathlib.CategoryTheory.NatIso
+import Mathlib.CategoryTheory.Functor.Currying
+
+/-!
+# Testing the `@[defeq]` attribute on some important equalities in category theory
+
+Category theory in mathlib relies heavily on the `dsimp` tactic to simplify terms
+in dependent position. The `dsimp` tactic makes use of the `@[defeq]` attribute.
+In lean v4.31.0, automatic tagging for this attribute was restricted to theorems that are type-correct
+at `implicit_reducible` transparency.
+An attribute `@[backward_defeq]` was added for theorems that are definitional equalities
+but that do not type-check at `implicit_reducible` transparency.
+
+In practice, this means that many lemma generated `@[simps]` on semi-reducible `def`s
+are not seen by `dsimp`, unless the option `set_option backward.defeqAttrib.useBackward`
+is set to true. This is usually an indicator that the definition needs to be implicit-reducible.
+
+This test file ensures that some of the important "dsimplification" equalities in category
+theory are tagged with `@[defeq]`.
+
+You should feel free to add more here when tagging definitions with `@[implicit_reducible]`.
+-/
+
+/-- Throwaway command for this test: `#ensure_defeq foo` returns an error if
+the declaration `foo` does not have the `@[defeq]` tag (e.g., if it has
+the `@[backward_defeq]` tag instead). -/
+syntax (name := ensureDefeqCmd) "#ensure_defeq " ident : command
+
+open Lean in
+elab_rules : command
+  | `(command| #ensure_defeq $ident:ident) => do
+    let name := ident.getId
+    let env ← getEnv
+    match env.find? name with
+    | ConstantInfo.thmInfo _ =>
+      if defeqAttr.hasTag env name then
+        logInfo m!"`{.ofConstName name}` is tagged with @[defeq]"
+        return ()
+      else if backwardDefeqAttr.hasTag env name then
+        throwError "`{.ofConstName name}` is tagged with @[backward_defeq] instead of @[defeq]!"
+      else
+        throwError "`{.ofConstName name}` is not tagged @[defeq] nor @[backward_defeq]!"
+    | none => throwError "Unknown identifier `{.ofConstName name}`"
+    | _ => throwError "#ensure_defeq can only be run on equality theorems."
+
+-- intentional error to test the command
+/-- error: `CategoryTheory.Category.assoc` is not tagged @[defeq] nor @[backward_defeq]! -/
+#guard_msgs (error) in
+#ensure_defeq CategoryTheory.Category.assoc
+
+/-- info: `CategoryTheory.NatIso.ofComponents_hom_app` is tagged with @[defeq] -/
+#guard_msgs in
+#ensure_defeq CategoryTheory.NatIso.ofComponents_hom_app
+
+/-- info: `CategoryTheory.Iso.trans_hom` is tagged with @[defeq] -/
+#guard_msgs in
+#ensure_defeq CategoryTheory.Iso.trans_hom
+
+/-- info: `CategoryTheory.Functor.comp_map` is tagged with @[defeq] -/
+#guard_msgs in
+#ensure_defeq CategoryTheory.Functor.comp_map
+
+/-- info: `CategoryTheory.Functor.comp_obj` is tagged with @[defeq] -/
+#guard_msgs in
+#ensure_defeq CategoryTheory.Functor.comp_obj
+
+/-- info: `CategoryTheory.Functor.curry_obj_obj_obj` is tagged with @[defeq] -/
+#guard_msgs in
+#ensure_defeq CategoryTheory.Functor.curry_obj_obj_obj
+
+/-- info: `CategoryTheory.Functor.uncurry_obj_obj` is tagged with @[defeq] -/
+#guard_msgs in
+#ensure_defeq CategoryTheory.Functor.uncurry_obj_obj
+
+/-- info: `CategoryTheory.Functor.associator_hom_app` is tagged with @[defeq] -/
+#guard_msgs in
+#ensure_defeq CategoryTheory.Functor.associator_hom_app
+
+/-- info: `CategoryTheory.Functor.leftUnitor_hom_app` is tagged with @[defeq] -/
+#guard_msgs in
+#ensure_defeq CategoryTheory.Functor.leftUnitor_hom_app
+
+/-- info: `CategoryTheory.Functor.rightUnitor_hom_app` is tagged with @[defeq] -/
+#guard_msgs in
+#ensure_defeq CategoryTheory.Functor.rightUnitor_hom_app
diff --git a/upstream_sha b/upstream_sha
index 89165a9fa7..a674d0877d 100644
--- a/upstream_sha
+++ b/upstream_sha
@@ -1 +1 @@
-9cebae57f419f984d008f357605b2621a1d9f13b
+65fe2a1f85b506b0ef7df1990697be5a1ad64317