diff --git a/Cache/Requests.lean b/Cache/Requests.lean
index 8b9e0db8351b1e..8c9e156e4fe2f0 100644
--- a/Cache/Requests.lean
+++ b/Cache/Requests.lean
@@ -94,7 +94,7 @@ def findMathlibRemote (mathlibDepPath : FilePath) : IO String := do
       let remoteUrl := parts[1]!.takeWhile (· != ' ') |>.copy -- Remove (fetch) or (push) suffix
 
       -- Check if this remote points to leanprover-community/mathlib4
-      let isMathlibRepo := remoteUrl.containsSubstr "leanprover-community/mathlib4"
+      let isMathlibRepo := remoteUrl.contains "leanprover-community/mathlib4"
 
       if isMathlibRepo then
         if remoteName == "origin" then
diff --git a/Mathlib/Algebra/Colimit/DirectLimit.lean b/Mathlib/Algebra/Colimit/DirectLimit.lean
index 3c8edf21854754..3862c8a850e511 100644
--- a/Mathlib/Algebra/Colimit/DirectLimit.lean
+++ b/Mathlib/Algebra/Colimit/DirectLimit.lean
@@ -613,10 +613,10 @@ lemma map₀_algebraMap (i : ι) (r : R) :
 instance : Algebra R (DirectLimit G f) where
   algebraMap := map₀RingHom (f := f).comp (algebraMap R (∀ i, G i))
   commutes' r := DirectLimit.induction f fun i _ ↦ by
-    dsimp [Pi.algebraMap_def]
+    dsimp [Pi.algebraMap_def, map₀RingHom]
     rw [map₀_algebraMap i, mul_def, mul_def, Algebra.commutes]
   smul_def' r := DirectLimit.induction _ fun i _ => by
-    dsimp [Pi.algebraMap_def]
+    dsimp [Pi.algebraMap_def, map₀RingHom]
     rw [smul_def, map₀_algebraMap i, mul_def, Algebra.smul_def']
 
 lemma algebraMap_def (i : ι) (r : R) :
@@ -871,7 +871,6 @@ variable [Nonempty ι]
 
 variable (G f) in
 /-- The canonical map from a component to the direct limit. -/
-@[simps]
 def of (i) : G i →ₙₐ[R] DirectLimit G f where
   toFun x := ⟦⟨i, x⟩⟧
   __ := (DirectLimit.NonUnitalRing.of G f i)
@@ -886,7 +885,7 @@ variable (G f) in
 that respect the directed system structure (i.e. make some diagram commute) give rise
 to a unique map out of the direct limit.
 -/
-@[simps]
+@[simps toFun]
 def lift (g : ∀ i, G i →ₙₐ[R] P) (Hg : ∀ i j hij x, g j (f i j hij x) = g i x) :
     DirectLimit G f →ₙₐ[R] P where
   toFun := _root_.DirectLimit.lift _ (g · ·) fun i j h x ↦ (Hg i j h x).symm
diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index dcec6c6f8cfda4..bba22597b54516 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -15,6 +15,7 @@ public import Mathlib.Tactic.MkIffOfInductiveProp
 public import Mathlib.Tactic.OfNat
 public import Mathlib.Data.Nat.Notation
 public import Mathlib.Tactic.Simps.Basic
+public import Mathlib.Tactic.AdaptationNote
 
 /-!
 # Typeclasses for (semi)groups and monoids
diff --git a/Mathlib/Algebra/Group/Nat/Even.lean b/Mathlib/Algebra/Group/Nat/Even.lean
index e4b871f2e05a76..a668854556b0fe 100644
--- a/Mathlib/Algebra/Group/Nat/Even.lean
+++ b/Mathlib/Algebra/Group/Nat/Even.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Group.Even
 public import Mathlib.Algebra.Group.Nat.Defs
 public import Mathlib.Data.Nat.Sqrt
+public import Mathlib.Tactic.Attr.Register
 
 /-!
 # `IsSquare` and `Even` for natural numbers
diff --git a/Mathlib/Algebra/Homology/DerivedCategory/Basic.lean b/Mathlib/Algebra/Homology/DerivedCategory/Basic.lean
index 1b3321ed9858ae..72369bf49d4c35 100644
--- a/Mathlib/Algebra/Homology/DerivedCategory/Basic.lean
+++ b/Mathlib/Algebra/Homology/DerivedCategory/Basic.lean
@@ -114,15 +114,17 @@ variable (C) in
 def quotientCompQhIso : HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh ≅ Q :=
   HomologicalComplexUpToQuasiIso.quotientCompQhIso C (ComplexShape.up ℤ)
 
+#adaptation_note /-- Prior to nightly-2026-05-07, the LHS of these statements was guarded with
+`dsimp%`; it now reports `made no progress`, so we write the (already-reduced) form directly. -/
 @[reassoc (attr := simp)]
 lemma quotientCompQhIso_hom_naturality {K L : CochainComplex C ℤ} (f : K ⟶ L) :
-    dsimp% Qh.map ((HomotopyCategory.quotient _ _).map f) ≫ (quotientCompQhIso C).hom.app L =
+    Qh.map ((HomotopyCategory.quotient _ _).map f) ≫ (quotientCompQhIso C).hom.app L =
       (quotientCompQhIso C).hom.app K ≫ Q.map f :=
   (quotientCompQhIso C).hom.naturality f
 
 @[reassoc]
 lemma quotientCompQhIso_inv_naturality {K L : CochainComplex C ℤ} (f : K ⟶ L) :
-    dsimp% Q.map f ≫ (quotientCompQhIso C).inv.app L =
+    Q.map f ≫ (quotientCompQhIso C).inv.app L =
       (quotientCompQhIso C).inv.app K ≫ Qh.map ((HomotopyCategory.quotient _ _).map f) :=
   (quotientCompQhIso C).inv.naturality f
 
diff --git a/Mathlib/Algebra/Homology/DerivedCategory/KInjective.lean b/Mathlib/Algebra/Homology/DerivedCategory/KInjective.lean
index fc71341ebfa741..b105b6b72fd993 100644
--- a/Mathlib/Algebra/Homology/DerivedCategory/KInjective.lean
+++ b/Mathlib/Algebra/Homology/DerivedCategory/KInjective.lean
@@ -56,8 +56,8 @@ lemma quasiIso_iff {K L : CochainComplex C ℤ} [K.IsKInjective] [L.IsKInjective
   obtain ⟨g, hg⟩ := (Qh_map_bijective _ _).surjective
     ((quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K)
   refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
-  · simp [hg]
-  · simp [hg, ← quotientCompQhIso_inv_naturality, -NatTrans.naturality]
+  · simp [hg]; rfl
+  · simp [hg, ← quotientCompQhIso_inv_naturality, -NatTrans.naturality]; rfl
 
 end IsKInjective
 
diff --git a/Mathlib/Algebra/Homology/DerivedCategory/KProjective.lean b/Mathlib/Algebra/Homology/DerivedCategory/KProjective.lean
index 865f95d1c027d8..24e2f6614795b3 100644
--- a/Mathlib/Algebra/Homology/DerivedCategory/KProjective.lean
+++ b/Mathlib/Algebra/Homology/DerivedCategory/KProjective.lean
@@ -57,8 +57,8 @@ lemma quasiIso_iff {K L : CochainComplex C ℤ} [K.IsKProjective] [L.IsKProjecti
   obtain ⟨g, hg⟩ := (Qh_map_bijective _ _).surjective
     ((quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K)
   refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
-  · simp [hg]
-  · simp [hg, ← quotientCompQhIso_inv_naturality f, -NatTrans.naturality]
+  · simp [hg]; rfl
+  · simp [hg, ← quotientCompQhIso_inv_naturality f, -NatTrans.naturality]; rfl
 
 end IsKProjective
 
diff --git a/Mathlib/Algebra/Homology/Embedding/ExtendHomotopy.lean b/Mathlib/Algebra/Homology/Embedding/ExtendHomotopy.lean
index 533d41ec284f64..117b9a21ec44a6 100644
--- a/Mathlib/Algebra/Homology/Embedding/ExtendHomotopy.lean
+++ b/Mathlib/Algebra/Homology/Embedding/ExtendHomotopy.lean
@@ -222,7 +222,12 @@ lemma HomologicalComplex.homotopyEquivalences_extendMap_iff
     (e : ComplexShape.Embedding c c') [e.IsRelIff] :
     homotopyEquivalences C c' (extendMap f e) ↔
       homotopyEquivalences C c f := by
-  simp [← HomotopyCategory.inverseImage_quotient_isomorphisms,
+  #adaptation_note /-- Prior to nightly-2026-05-07, `dsimp%` was used directly inline as the last
+  argument to the original `simp`; it now reports `made no progress` so we apply
+  `NatIso.isIso_map_iff` via a `change` + `rw` after the rest of the simp set has done its work. -/
+  simp only [← HomotopyCategory.inverseImage_quotient_isomorphisms,
     MorphismProperty.inverseImage_iff, MorphismProperty.isomorphisms.iff,
-    ← isIso_iff_of_reflects_iso _ (e.extendHomotopyFunctor C),
-    dsimp% NatIso.isIso_map_iff (e.extendHomotopyFunctorFactors C) f]
+    ← isIso_iff_of_reflects_iso _ (e.extendHomotopyFunctor C)]
+  change _ ↔ IsIso ((HomotopyCategory.quotient C c ⋙ e.extendHomotopyFunctor C).map f)
+  rw [NatIso.isIso_map_iff (e.extendHomotopyFunctorFactors C) f]
+  rfl
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
index df2589c4073533..0cbfbfd1c3d41f 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
+++ b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
@@ -548,8 +548,8 @@ lemma isStableUnderBaseChange (hP : RingHom.IsStableUnderBaseChange Q) :
   · rw [IsZariskiLocalAtSource.iff_of_openCover (P := P)
       (Scheme.Pullback.openCoverOfRight Y.affineCover f g)]
     intro i
-    simp only [Scheme.Pullback.openCoverOfRight_f,
-      limit.lift_π, PullbackCone.mk_π_app, Category.comp_id]
+    simp only [Scheme.Pullback.openCoverOfRight_f, limit.lift_π, PullbackCone.mk_π_app,
+      Category.comp_id]
     apply this _ (comp_of_isOpenImmersion _ _ _ H) inferInstance
   rw [iff_of_isAffine (P := P)] at H ⊢
   exact hP.pullback_fst_appTop _ (isLocal_ringHomProperty P).respectsIso _ _ H
diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Functor.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Functor.lean
index 89d9cb26712aba..13e1cd50a9aaef 100644
--- a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Functor.lean
+++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Functor.lean
@@ -203,8 +203,8 @@ an affine open cover of `Proj ℬ` consisting of `D(f(s))` for `s ∈ A` positiv
 set_option backward.isDefEq.respectTransparency false in
 theorem map_comp : map (g.comp f) (irrelevant_le_map_comp hf hg) = map g hg ≫ map f hf := by
   refine (mapAffineOpenCover _ <| irrelevant_le_map_comp hf hg).openCover.hom_ext _ _ fun s ↦ ?_
-  simp only [Scheme.AffineOpenCover.openCover_f,
-    mapAffineOpenCover_f, awayι_comp_map (g.comp f) _ s.1.2 _ s.2.2]
+  simp only [Scheme.AffineOpenCover.openCover_f, mapAffineOpenCover_f,
+    awayι_comp_map (g.comp f) _ s.1.2 _ s.2.2]
   simp [awayι_comp_map_assoc _ _ _ _ (map_mem f s.2.2), awayι_comp_map _ _ _ _ s.2.2]
 
 set_option backward.isDefEq.respectTransparency false in
diff --git a/Mathlib/AlgebraicGeometry/Restrict.lean b/Mathlib/AlgebraicGeometry/Restrict.lean
index d21be905d7c89e..fcc06281a91ea1 100644
--- a/Mathlib/AlgebraicGeometry/Restrict.lean
+++ b/Mathlib/AlgebraicGeometry/Restrict.lean
@@ -767,8 +767,7 @@ set_option backward.isDefEq.respectTransparency false in
 noncomputable def arrowResLEAppIso (f : X ⟶ Y) (U : Y.Opens) (V : X.Opens) (e : V ≤ f ⁻¹ᵁ U) :
     Arrow.mk ((f.resLE U V e).appTop) ≅ Arrow.mk (f.appLE U V e) :=
   Arrow.isoMk U.topIso V.topIso <| by
-  simp only [Scheme.Opens.topIso_hom,
-    eqToHom_op, Arrow.mk_hom, Scheme.Hom.map_appLE]
+  simp only [Scheme.Opens.topIso_hom, eqToHom_op, Arrow.mk_hom, Scheme.Hom.map_appLE]
   rw [Scheme.Hom.appTop, ← Scheme.Hom.appLE_eq_app, Scheme.Hom.resLE_appLE, Scheme.Hom.appLE_map]
 
 lemma Scheme.Hom.isPullback_resLE
diff --git a/Mathlib/CategoryTheory/Discrete/Basic.lean b/Mathlib/CategoryTheory/Discrete/Basic.lean
index 17597b8699dfd7..fecaa93e0cc081 100644
--- a/Mathlib/CategoryTheory/Discrete/Basic.lean
+++ b/Mathlib/CategoryTheory/Discrete/Basic.lean
@@ -323,6 +323,7 @@ def piEquivalenceFunctorDiscrete (J : Type u₂) (C : Type u₁) [Category.{v₁
       obtain rfl : f = 𝟙 _ := rfl
       simp))) (by cat_disch)
 
+set_option backward.defeqAttrib.useBackward true in
 /-- `piEquivalenceFunctorDiscrete` is compatible with `evaluation`. -/
 @[simps!]
 def piEquivalenceFunctorDiscreteCompEvaluationIso (C : Type*) [Category* C] {J : Type*} (j : J) :
diff --git a/Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean b/Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean
index a762979a0a700b..835fdebf706f1d 100644
--- a/Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean
+++ b/Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean
@@ -61,6 +61,8 @@ maps `k : ∀ i, I i` to `∏ᶜ fun (s : α) => (F s).obj (k s)`. -/
 noncomputable abbrev pointwiseProduct : (∀ i, I i) ⥤ C :=
   Functor.pi F ⋙ Pi.functor α
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 attribute [local simp] Functor.pi in
 /-- `pointwiseProduct` is invariant under re-indexing. -/
 @[simps!]
@@ -81,6 +83,8 @@ noncomputable def coconePointwiseProduct (c : ∀ i, Cocone (F i)) :
   pt := ∏ᶜ fun i ↦ (c i).pt
   ι := Functor.whiskerRight (NatTrans.pi fun i ↦ (c i).ι) _ ≫ (Pi.constCompPiIsoConst _).hom
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 /-- `coconePointwiseProduct` is invariant under isomorphisms of cocones. -/
 noncomputable def coconePointwiseProductIso {c c' : ∀ i, Cocone (F i)} (e : ∀ i, c i ≅ c' i) :
     coconePointwiseProduct c ≅ coconePointwiseProduct c' :=
@@ -99,6 +103,7 @@ noncomputable def colimitPointwiseProductToProductColimit [∀ i, HasColimit (F
 
 variable [∀ i, HasColimit (F i)] [HasColimit (pointwiseProduct F)]
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 @[reassoc (attr := simp)]
 theorem ι_colimitPointwiseProductToProductColimit_π (k : ∀ i, I i) (s : α) :
@@ -126,6 +131,8 @@ noncomputable def pointwiseProductCompEvaluation (d : D) :
   NatIso.ofComponents (fun k => piObjIso _ _)
     (fun f => Pi.hom_ext _ _ (by simp [Functor.pi, ← NatTrans.comp_app]))
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 /-- In a functor category, `coconePointwiseProduct` commutes with evaluation. -/
 noncomputable def evaluationCoconePointwiseProductIso (X : D) (c : ∀ i, Cocone (F i)) :
     ((evaluation D C).obj X).mapCocone (coconePointwiseProduct c) ≅
@@ -199,6 +206,8 @@ lemma IsIPCOfShape.of_isIso
   obtain ⟨_, h⟩ := H J F
   rwa [IsColimit.nonempty_isColimit_iff_isIso_desc (colimit.isColimit _)]
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 attribute [local simp] Functor.pi in
 lemma IsIPCOfShape.of_equiv {ι' : Type*} [HasProductsOfShape ι' C] [IsIPCOfShape.{w} ι C]
     (e : ι ≃ ι') :
diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean
index ce31b1c90adae4..40c166c873b799 100644
--- a/Mathlib/CategoryTheory/Limits/HasLimits.lean
+++ b/Mathlib/CategoryTheory/Limits/HasLimits.lean
@@ -489,6 +489,7 @@ def lim : (J ⥤ C) ⥤ C where
     apply Limits.limit.hom_ext; intro j
     simp [assoc]
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The natural transformation induced by `limit.π`. -/
 @[simps]
 def lim.π (j : J) : lim ⟶ (evaluation J C).obj j where
@@ -1074,6 +1075,7 @@ def colim : (J ⥤ C) ⥤ C where
   obj F := colimit F
   map α := colimMap α
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The natural transformation induced by `colimit.ι`. -/
 @[simps]
 def colim.ι (j : J) : (evaluation J C).obj j ⟶ colim where
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
index ac86ca6eee41dc..2ba0a03f202cfe 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
@@ -322,6 +322,8 @@ structure BinaryBicone.IsBilimit {P Q : C} (b : BinaryBicone P Q) where
 attribute [inherit_doc BinaryBicone.IsBilimit] BinaryBicone.IsBilimit.isLimit
   BinaryBicone.IsBilimit.isColimit
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 /-- If a binary bicone for `P` and `Q` is bilimit, then the binary bicone for `P'` and `Q'`
 obtained using isomorphisms `P ≅ P'` and `Q ≅ Q'` is also bilimit. -/
 def BinaryBicone.IsBilimit.ofIso {P Q P' Q' : C} {b : BinaryBicone P Q} (hb : b.IsBilimit)
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
index 37edb79c667196..03e337f5a34ccc 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
@@ -997,12 +997,14 @@ noncomputable def Pi.functor [HasProductsOfShape α C] : (α → C) ⥤ C where
   obj f := ∏ᶜ f
   map {f g} t := Pi.map t
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The natural transformation induced by `Pi.π`. -/
 @[simps]
 def Pi.functorπ [HasProductsOfShape α C] (a : α) :
     Pi.functor α ⟶ Pi.eval (fun _ ↦ C) a where
   app f := Pi.π f a
 
+set_option backward.defeqAttrib.useBackward true in
 variable (α) in
 /-- Up to pre-composing with an equivalence of categories, `Pi.functor` is isomorphic to `lim`. -/
 @[simps!]
@@ -1010,6 +1012,7 @@ def piEquivalenceFunctorDiscreteCompLim [HasProductsOfShape α C] :
     (piEquivalenceFunctorDiscrete α C).functor ⋙ lim ≅ Pi.functor _ :=
   NatIso.ofComponents fun _ ↦ Iso.refl _
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc]
 lemma piEquivalenceFunctorDiscreteCompLim_comp_functorπ [HasProductsOfShape α C] (a : α) :
     (piEquivalenceFunctorDiscreteCompLim (C := C) α).hom ≫ Pi.functorπ a =
@@ -1017,6 +1020,7 @@ lemma piEquivalenceFunctorDiscreteCompLim_comp_functorπ [HasProductsOfShape α
         (piEquivalenceFunctorDiscreteCompEvaluationIso _ _).hom := by
   cat_disch
 
+set_option backward.defeqAttrib.useBackward true in
 attribute [local simp] Functor.pi in
 /-- The `∏ᶜ` functor composed with the pointwise constant functor `Π i, I i ⥤ (α → C)` is isomorphic
 to the constant functor with value `∏ᶜ X`. -/
@@ -1034,12 +1038,14 @@ noncomputable def Sigma.functor [HasCoproductsOfShape α C] : (α → C) ⥤ C w
   obj f := ∐ f
   map {f g} t := Sigma.map t
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The natural transformation induced by `Sigma.ι`. -/
 @[simps]
 def Sigma.functorι [HasCoproductsOfShape α C] (a : α) :
     Pi.eval (fun _ ↦ C) a ⟶ Sigma.functor α where
   app f := Sigma.ι f a
 
+set_option backward.defeqAttrib.useBackward true in
 variable (α) in
 /-- Up to pre-composing with an equivalence of categories, `Sigma.functor` is isomorphic
 to `colim`. -/
@@ -1048,6 +1054,7 @@ def piEquivalenceFunctorDiscreteCompColim [HasCoproductsOfShape α C] :
     (piEquivalenceFunctorDiscrete α C).functor ⋙ colim ≅ Sigma.functor _ :=
   NatIso.ofComponents fun _ ↦ Iso.refl _
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc]
 lemma piEquivalenceFunctorDiscreteCompColim_comp_functorι [HasCoproductsOfShape α C] (a : α) :
     Functor.whiskerLeft _ (colim.ι <| .mk a) ≫ (piEquivalenceFunctorDiscreteCompColim α).hom =
@@ -1058,6 +1065,7 @@ lemma piEquivalenceFunctorDiscrete_functor_comp_colim [HasCoproductsOfShape α C
     (piEquivalenceFunctorDiscrete α C).functor ⋙ colim = Sigma.functor _ :=
   rfl
 
+set_option backward.defeqAttrib.useBackward true in
 attribute [local simp] Functor.pi in
 /-- The `∐` functor composed with the pointwise constant functor `Π i, I i ⥤ (α → C)` is isomorphic
 to the constant functor with value `∐ X`. -/
diff --git a/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean b/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean
index 74040db5901e8d..b60209d56ddf55 100644
--- a/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean
+++ b/Mathlib/CategoryTheory/MorphismProperty/Factorization.lean
@@ -247,6 +247,8 @@ instance [HasFunctorialFactorization W₁ W₂] (J : Type*) [Category* J] :
     HasFunctorialFactorization (W₁.functorCategory J) (W₂.functorCategory J) :=
   ⟨⟨(functorialFactorizationData W₁ W₂).functorCategory J⟩⟩
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 variable {W₁ W₂} in
 /-- The term in `MapFactorizationData (W₁.inverseImage F) (W₂.inverseImage F) f`
 deduced from `h : MapFactorizationData W₁ W₂ (F.map f)` when `F` is an equivalence
@@ -260,10 +262,12 @@ noncomputable def MapFactorizationData.ofIsEquivalence {F : D ⥤ C}
   p := F.preimage ((F.objObjPreimageIso h.Z).hom ≫ h.p)
   hi := by
     refine (W₁.arrow_mk_iso_iff ?_).1 h.hi
-    exact Arrow.isoMk (Iso.refl _) (F.objObjPreimageIso h.Z).symm
+    refine Arrow.isoMk (Iso.refl _) (F.objObjPreimageIso h.Z).symm ?_
+    simp [F.map_preimage]
   hp := by
     refine (W₂.arrow_mk_iso_iff ?_).1 h.hp
-    exact Arrow.isoMk (F.objObjPreimageIso h.Z).symm (Iso.refl _)
+    refine Arrow.isoMk (F.objObjPreimageIso h.Z).symm (Iso.refl _) ?_
+    simp [F.map_preimage]
   fac := F.map_injective (by simp)
 
 instance (F : D ⥤ C) [F.IsEquivalence]
diff --git a/Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean b/Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean
index 8d323c9cf812ce..3612c6b1c49d0f 100644
--- a/Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean
+++ b/Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean
@@ -185,8 +185,17 @@ lemma Functor.hasLiftingProperty_iff_of_isEquivalence
     {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) :
     HasLiftingProperty (G.map i) (G.map p) ↔
       HasLiftingProperty i p := by
+  #adaptation_note /-- Prior to nightly-2026-05-07, the next three lines were just
+  ```
   simp only [dsimp% G.asEquivalence.toAdjunction.hasLiftingProperty_iff,
     ← MorphismProperty.rlp_ofHoms_iff_hasLiftingProperty Unit]
+  ```
+  This is a temporary repair, and authors/maintainers are encouraged to either find a better repair,
+  or identify a minimal example of an underlying problem in Lean.
+  -/
+  change HasLiftingProperty (G.asEquivalence.functor.map i) (G.asEquivalence.functor.map p) ↔ _
+  rw [G.asEquivalence.toAdjunction.hasLiftingProperty_iff]
+  simp only [← MorphismProperty.rlp_ofHoms_iff_hasLiftingProperty Unit]
   exact MorphismProperty.arrow_mk_iso_iff _
     (Arrow.isoMk (G.asEquivalence.unitIso.symm.app _)
       (G.asEquivalence.unitIso.symm.app _)
diff --git a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean
index a9b483aadac607..72bfb9eb14b469 100644
--- a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean
+++ b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean
@@ -137,6 +137,7 @@ lemma unop_isoClosure (P : ObjectProperty Cᵒᵖ) :
     P.isoClosure.unop = P.unop.isoClosure := by
   rw [← op_injective_iff, P.unop.op_isoClosure, op_unop, op_unop]
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Given `P : ObjectProperty C`, this is the equivalence between `P.op.FullSubcategory`
 and `P.FullSubcategoryᵒᵖ`. -/
 @[simps]
diff --git a/Mathlib/CategoryTheory/Opposites.lean b/Mathlib/CategoryTheory/Opposites.lean
index fb06df7fbd00da..d2e8d5259ffa28 100644
--- a/Mathlib/CategoryTheory/Opposites.lean
+++ b/Mathlib/CategoryTheory/Opposites.lean
@@ -310,6 +310,7 @@ set_option backward.defeqAttrib.useBackward true in
 protected def FullyFaithful.op {F : C ⥤ D} (hF : F.FullyFaithful) : F.op.FullyFaithful where
   preimage {X Y} f := .op <| hF.preimage f.unop
 
+set_option backward.defeqAttrib.useBackward true in
 /-- A functor is fully faithful when its opposite is fully faithful. -/
 protected def FullyFaithful.unop {F : Cᵒᵖ ⥤ Dᵒᵖ} (hF : F.FullyFaithful) :
     F.unop.FullyFaithful where
diff --git a/Mathlib/CategoryTheory/Shift/SingleFunctorsLift.lean b/Mathlib/CategoryTheory/Shift/SingleFunctorsLift.lean
index bc231bf2c45886..e73a7581854002 100644
--- a/Mathlib/CategoryTheory/Shift/SingleFunctorsLift.lean
+++ b/Mathlib/CategoryTheory/Shift/SingleFunctorsLift.lean
@@ -46,6 +46,7 @@ noncomputable def shiftIso (n a a' : A) (h : n + a = a') :
       isoWhiskerLeft _ (G.commShiftIso n) ≪≫ (Functor.associator _ _ _).symm ≪≫
       isoWhiskerRight (hΦ a') _ ≪≫ F.shiftIso n a a' h ≪≫ (hΦ a).symm)
 
+set_option backward.defeqAttrib.useBackward true in
 private lemma map_shiftIso_hom_app (n a a' : A) (h : n + a = a') (X : C) :
     dsimp% G.map ((lift.shiftIso hΦ n a a' h).hom.app X) =
       (G.commShiftIso n).hom.app _ ≫ (shiftFunctor E n).map ((hΦ a').hom.app X) ≫
@@ -54,6 +55,7 @@ private lemma map_shiftIso_hom_app (n a a' : A) (h : n + a = a') (X : C) :
 
 end lift
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- Let `C`, `D` and `E` be categories. Let `A` be an additive monoid.
 Assume that `D` and `E` have shifts by `A` and that we have
@@ -78,6 +80,7 @@ noncomputable def lift : SingleFunctors C D A where
     rw [F.shiftIso_add n m a a' a'' ha' ha'']
     simp [commShiftIso_add, ← Functor.map_comp_assoc, -Functor.map_comp]
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc]
 lemma map_lift_shiftIso_hom_app (n a a' : A) (h : n + a = a') (X : C) :
     dsimp% G.map (((lift F G Φ hΦ).shiftIso n a a' h).hom.app X) =
@@ -85,6 +88,7 @@ lemma map_lift_shiftIso_hom_app (n a a' : A) (h : n + a = a') (X : C) :
         (F.shiftIso n a a' h).hom.app X ≫ (hΦ a).inv.app X :=
   lift.map_shiftIso_hom_app ..
 
+set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 /-- After postcomposition with the fully faithful functor `G`,
 `lift F G Φ hΦ` becomes isomorphic to `F`. -/
@@ -96,6 +100,7 @@ noncomputable def liftPostcompIso : (lift F G Φ hΦ).postcomp G ≅ F :=
     dsimp at this
     simp [map_lift_shiftIso_hom_app, this])
 
+set_option backward.defeqAttrib.useBackward true in
 instance [Preadditive C] [Preadditive D] [Preadditive E] [G.Additive] (a : A)
     [(F.functor a).Additive] : ((lift F G Φ hΦ).functor a).Additive := by
   have : ((lift F G Φ hΦ).functor a ⋙ G).Additive := by
diff --git a/Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean b/Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
index 276eccbea19be0..1fc0f3524aa274 100644
--- a/Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
+++ b/Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
@@ -122,7 +122,7 @@ theorem equiv_symm_eq_apply {X : C} {P : Cᵒᵖ ⥤ D} {S : J.Cover X} [HasMult
     -- We can hint `ConcreteCategory.hom (Y := P.obj (op I.Y))` below to put it into `simp`-normal
     -- form, but that doesn't seem to fix the `erw`s below...
     (Multiequalizer.ι (S.index P) I) ((Meq.equiv P S).symm x) = x I := by
-  simp [← equiv_apply]
+  simp [- GrothendieckTopology.Cover.index_left, ← equiv_apply]
 
 end Meq
 
diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean
index 05308db5f83fac..7c33867dfece7e 100644
--- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean
+++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean
@@ -97,6 +97,8 @@ lemma isVerdierRightLocalizing_op_iff :
 variable [HasZeroObject C] [HasShift C ℤ] [Preadditive C]
   [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C]
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 lemma isVerdierRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated]
     [B.IsClosedUnderIsomorphisms] :
     A.IsVerdierRightLocalizing B ↔
@@ -107,7 +109,7 @@ lemma isVerdierRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated]
     obtain ⟨W, a, b, hT, hW⟩ := hs
     obtain ⟨W', c, d, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac a hW hX
     obtain ⟨U, hU, e, f, hT'⟩ := A.distinguished_cocone_triangle d h₁ hX
-    obtain ⟨g, hg, _⟩ := complete_distinguished_triangle_morphism _ _ hT hT'
+    obtain ⟨g, hg, _⟩ := Pretriangulated.complete_distinguished_triangle_morphism _ _ hT hT'
       c (𝟙 _) (by cat_disch)
     refine ⟨U, e, g, hU, ?_, by cat_disch⟩
     rw [ObjectProperty.trW_iff']
diff --git a/Mathlib/CategoryTheory/Triangulated/Subcategory.lean b/Mathlib/CategoryTheory/Triangulated/Subcategory.lean
index b100c6f06e233b..ecc1eec1e7dfaf 100644
--- a/Mathlib/CategoryTheory/Triangulated/Subcategory.lean
+++ b/Mathlib/CategoryTheory/Triangulated/Subcategory.lean
@@ -90,6 +90,8 @@ lemma ext_of_isTriangulatedClosed₃'
     (h₁ : P T.obj₁) (h₂ : P T.obj₂) : P.isoClosure T.obj₃ :=
   IsTriangulatedClosed₃.ext₃' T hT h₁ h₂
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 protected lemma distinguished_cocone_triangle [P.IsTriangulatedClosed₃]
     {X Y : C} (a : X ⟶ Y) (hX : P X) (hY : P Y) :
     ∃ (Z : C) (_ : P Z) (b : Y ⟶ Z) (c : Z ⟶ X⟦(1 : ℤ)⟧), Triangle.mk a b c ∈ distTriang _ := by
@@ -98,6 +100,8 @@ protected lemma distinguished_cocone_triangle [P.IsTriangulatedClosed₃]
   exact ⟨Z', hZ', b ≫ e.hom, e.inv ≫ c, isomorphic_distinguished _ h _
     (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) e.symm )⟩
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 protected lemma distinguished_cocone_triangle₁ [P.IsTriangulatedClosed₁]
     {Y Z : C} (b : Y ⟶ Z) (hY : P Y) (hZ : P Z) :
     ∃ (X : C) (_ : P X) (a : X ⟶ Y) (c : Z ⟶ X⟦(1 : ℤ)⟧), Triangle.mk a b c ∈ distTriang _ := by
@@ -106,6 +110,8 @@ protected lemma distinguished_cocone_triangle₁ [P.IsTriangulatedClosed₁]
   exact ⟨X', hX', e.inv ≫ a, c ≫ e.hom⟦1⟧', isomorphic_distinguished _ h _
     (Triangle.isoMk _ _ e.symm (Iso.refl _) (Iso.refl _))⟩
 
+set_option backward.defeqAttrib.useBackward true in
+set_option backward.isDefEq.respectTransparency false in
 protected lemma distinguished_cocone_triangle₂ [P.IsTriangulatedClosed₂]
     {X Z : C} (c : Z ⟶ X⟦(1 : ℤ)⟧) (hX : P X) (hZ : P Z) :
     ∃ (Y : C) (_ : P Y) (a : X ⟶ Y) (b : Y ⟶ Z), Triangle.mk a b c ∈ distTriang _ := by
diff --git a/Mathlib/Control/Bifunctor.lean b/Mathlib/Control/Bifunctor.lean
index b9cd394f8d7cf6..3082728a59b19c 100644
--- a/Mathlib/Control/Bifunctor.lean
+++ b/Mathlib/Control/Bifunctor.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Control.Functor
 public import Mathlib.Tactic.Common
+public import Mathlib.Tactic.Attr.Register
 
 /-!
 # Functors with two arguments
diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean
index a32788685ee0e0..b346ac6bdc1aae 100644
--- a/Mathlib/Data/Set/Basic.lean
+++ b/Mathlib/Data/Set/Basic.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Order.PropInstances
 public import Mathlib.Tactic.Lift
+public import Mathlib.Tactic.Attr.Register
 
 /-!
 # Basic properties of sets
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Pi.lean b/Mathlib/LinearAlgebra/TensorProduct/Pi.lean
index 99efa2312c3080..e897dd3604541f 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Pi.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Pi.lean
@@ -131,11 +131,15 @@ def piScalarRightHomBil : N →ₗ[S] (ι → R) →ₗ[R] (ι → N) where
     rw [← IsScalarTower.smul_assoc, _root_.Algebra.smul_def, mul_comm, mul_smul]
     simp
 
+set_option backward.privateInPublic true in
+set_option backward.privateInPublic.warn false in
 /-- For any `R`-module `N` and index type `ι`, there is a natural
 linear map `N ⊗[R] (ι → R) →ₗ (ι → N)`. This map is an isomorphism if `ι` is finite. -/
 def piScalarRightHom : N ⊗[R] (ι → R) →ₗ[S] (ι → N) :=
   AlgebraTensorModule.lift <| piScalarRightHomBil R S N ι
 
+set_option backward.privateInPublic true in
+set_option backward.privateInPublic.warn false in
 @[simp]
 lemma piScalarRightHom_tmul (x : N) (f : ι → R) :
     piScalarRightHom R S N ι (x ⊗ₜ f) = (fun j ↦ f j • x) := by
diff --git a/Mathlib/MeasureTheory/Integral/Prod.lean b/Mathlib/MeasureTheory/Integral/Prod.lean
index 6c872f1d9a8b54..b2c0975c972252 100644
--- a/Mathlib/MeasureTheory/Integral/Prod.lean
+++ b/Mathlib/MeasureTheory/Integral/Prod.lean
@@ -476,9 +476,6 @@ theorem continuous_integral_integral :
   apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le) _
   · exact fun i => ∫⁻ x, ∫⁻ y, ‖i (x, y) - g (x, y)‖ₑ ∂ν ∂μ
   swap; · exact fun i => lintegral_mono fun x => enorm_integral_le_lintegral_enorm _
-  change
-    Tendsto (fun i : α × β →₁[μ.prod ν] E => ∫⁻ x, ∫⁻ y : β, ‖i (x, y) - g (x, y)‖ₑ ∂ν ∂μ) (𝓝 g)
-      (𝓝 0)
   have this (i : α × β →₁[μ.prod ν] E) : Measurable fun z => ‖i z - g z‖ₑ :=
     ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm
   simp_rw [← lintegral_prod _ (this _).aemeasurable, ← L1.ofReal_norm_sub_eq_lintegral,
diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean
index 05f27f95cae3b1..81f47db9afc62f 100644
--- a/Mathlib/Order/Basic.lean
+++ b/Mathlib/Order/Basic.lean
@@ -13,6 +13,7 @@ public import Mathlib.Tactic.Convert
 public import Mathlib.Tactic.Inhabit
 public import Mathlib.Tactic.SimpRw
 public import Mathlib.Tactic.GCongr.Core
+public import Mathlib.Tactic.Attr.Register
 
 /-!
 # Basic definitions about `≤` and `<`
diff --git a/Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean b/Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
index 6395d12eaccb7b..73a083d1134099 100644
--- a/Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
+++ b/Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
@@ -222,10 +222,6 @@ theorem Kernel.continuous_integral_integral :
   apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i => zero_le) _
   · exact fun i => ∫⁻ x, ∫⁻ y, ‖i (x, y) - g (x, y)‖ₑ ∂η (a, x) ∂κ a
   swap; · exact fun i => lintegral_mono fun x => enorm_integral_le_lintegral_enorm _
-  change
-    Tendsto
-      (fun i : β × γ →₁[(κ ⊗ₖ η) a] E => ∫⁻ x, ∫⁻ y : γ, ‖i (x, y) - g (x, y)‖ₑ ∂η (a, x) ∂κ a)
-      (𝓝 g) (𝓝 0)
   have this (i : Lp (α := β × γ) E 1 (((κ ⊗ₖ η) a) : Measure (β × γ))) :
       Measurable fun z => ‖i z - g z‖ₑ :=
     ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm
diff --git a/Mathlib/RingTheory/Bialgebra/TensorProduct.lean b/Mathlib/RingTheory/Bialgebra/TensorProduct.lean
index 35a0ccd93d0ef1..898a3bdf4571e5 100644
--- a/Mathlib/RingTheory/Bialgebra/TensorProduct.lean
+++ b/Mathlib/RingTheory/Bialgebra/TensorProduct.lean
@@ -167,6 +167,7 @@ end Heterogeneous
 section Homogeneous
 variable (R S A B) [Bialgebra R A] [Bialgebra R B]
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The tensor product of `R`-bialgebras is commutative, up to bialgebra isomorphism. -/
 @[expose] def comm : A ⊗[R] B ≃ₐc[R] B ⊗[R] A :=
   .ofAlgEquiv (Algebra.TensorProduct.comm R A B) (by ext <;> simp) <| by
diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean
index 0a8d0ed84eebf8..1e98722a0e0929 100644
--- a/Mathlib/Tactic/Linter/TextBased.lean
+++ b/Mathlib/Tactic/Linter/TextBased.lean
@@ -290,9 +290,9 @@ def adaptationNoteLinter : TextbasedLinter := fun opts lines ↦ Id.run do
     -- (e.g. "-- Adaptation note:" or "-- adaptation note:"), but not lines that
     -- merely reference the concept (e.g. "-- see adaptation note") or that
     -- use the correct #adaptation_note command.
-    if line.containsSubstr "daptation note" &&
-        !line.containsSubstr "#adaptation_note" &&
-        !line.containsSubstr "see adaptation note" then
+    if line.contains "daptation note" &&
+        !line.contains "#adaptation_note" &&
+        !line.contains "see adaptation note" then
       errors := errors.push (StyleError.adaptationNote, idx + 1)
   return (errors, none)
 
diff --git a/Mathlib/Tactic/Translate/Reorder.lean b/Mathlib/Tactic/Translate/Reorder.lean
index 1f4755ac12298c..c2c614edeb632f 100644
--- a/Mathlib/Tactic/Translate/Reorder.lean
+++ b/Mathlib/Tactic/Translate/Reorder.lean
@@ -59,19 +59,6 @@ open Lean Meta Elab
 /-- A permutation, represented using cycle notation. -/
 abbrev Permutation := List {l : List Nat // 2 ≤ l.length}
 
-/-- Permute a list of either universe levels or universe parameters.
-The current heuristic is to swap the first two universes if the first argument is permuted. -/
-def Reorder.permuteUniv {α} (r : Reorder) (us : List α) : List α :=
-  if r.perm.any (·.1.contains 0) then
-    if let x :: y :: l := us then
-      y :: x :: l
-    else us
-  else us
-
-/-- Return `true` if the reorder doesn't do anything. -/
-def Reorder.isEmpty : Reorder → Bool
-  | { perm, argReorders } => perm.isEmpty && argReorders.isEmpty
-
 namespace Permutation
 
 /-- Permute an array of arguments using the given reorder. -/
@@ -122,7 +109,7 @@ structure ArgReorder where
 namespace ArgReorder
 
 /-- Return `true` if the reorder doesn't do anything. -/
-def isEmpty (r : ArgReorder) : Bool := r matches {}
+def isEmpty (r : ArgReorder) : Bool := r matches ⟨[], #[]⟩
 
 /-- Permute an array of arguments using the given reorder. -/
 def permute! {α} [Inhabited α] (r : ArgReorder) : Array α → Array α :=
diff --git a/MathlibTest/toAdditive.lean b/MathlibTest/toAdditive.lean
index ebc848b12813dd..3ee298c702cc4f 100644
--- a/MathlibTest/toAdditive.lean
+++ b/MathlibTest/toAdditive.lean
@@ -180,9 +180,8 @@ example {x} (h : 1 = x) : baz20 = x := by simp; guard_target = 1 = x; exact h
 @[to_additive bar21]
 def foo21 {N} {A} [Pow A N] (a : A) (n : N) : A := a ^ n
 
-run_meta do
-  let some ⟨`Test.bar21, r, .arg 1⟩ := translations.find? (← getEnv) `Test.foo21 | failure
-  guard <| r.isEmpty
+run_meta guard <| translations.find? (← getEnv) `Test.foo21
+  matches some ⟨`Test.bar21, ⟨[], ⟨[], #[]⟩⟩, .arg 1⟩
 
 @[to_additive bar22]
 abbrev foo22 {α} [Monoid α] (a : α) : ℕ → α
@@ -838,10 +837,9 @@ instance : Mul (MonoidAlgebra Nat G) where
 def monoidAlgebraFoo {k G : Type} [Inhabited k] : MonoidAlgebra k G × Nat :=
   (⟨fun _ ↦ default⟩, 2)
 
-run_meta do
-  let some ⟨``addMonoidAlgebraFoo, r, .arg 1⟩ := translations.find? (← getEnv) ``monoidAlgebraFoo
-    | failure
-  guard <| r.isEmpty
+run_meta guard <|
+  translations.find? (← getEnv) ``monoidAlgebraFoo
+    matches some ⟨``addMonoidAlgebraFoo, ⟨[], ⟨[], #[]⟩⟩, .arg 1⟩
 
 /--
 warning: `to_additive` correctly autogenerated `(relevant_arg := 2)` for `monoidAlgebraFoo₁`.
diff --git a/lake-manifest.json b/lake-manifest.json
index 4e00425ec68f0f..54f6bf9494c50c 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "71e6f956598ed639a0977b016cf7322a673bf134",
+   "rev": "25a8b1685158cc5b463b2cdf3d06f16846a3b919",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
diff --git a/lean-toolchain b/lean-toolchain
index f28bc4565ea06b..24588e1238c82c 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-05-03
+leanprover/lean4:nightly-2026-05-07