diff --git a/Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean b/Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
index 3fde74fdd517d6..6d0c444536dbd5 100644
--- a/Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
+++ b/Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
@@ -344,7 +344,6 @@ instance instNonUnitalSemiring [Fintype n] [NonUnitalSemiring A] :
     NonUnitalSemiring (CStarMatrix n n A) :=
   inferInstanceAs <| NonUnitalSemiring (Matrix n n A)
 
-set_option backward.inferInstanceAs.wrap false in
 instance instNonAssocSemiring [Fintype n] [DecidableEq n] [NonAssocSemiring A] :
     NonAssocSemiring (CStarMatrix n n A) :=
   inferInstanceAs <| NonAssocSemiring (Matrix n n A)
@@ -353,17 +352,14 @@ instance instNonUnitalRing [Fintype n] [NonUnitalRing A] :
     NonUnitalRing (CStarMatrix n n A) :=
   inferInstanceAs <| NonUnitalRing (Matrix n n A)
 
-set_option backward.inferInstanceAs.wrap false in
 instance instNonAssocRing [Fintype n] [DecidableEq n] [NonAssocRing A] :
     NonAssocRing (CStarMatrix n n A) :=
   inferInstanceAs <| NonAssocRing (Matrix n n A)
 
-set_option backward.inferInstanceAs.wrap false in
 instance instSemiring [Fintype n] [DecidableEq n] [Semiring A] :
     Semiring (CStarMatrix n n A) :=
   inferInstanceAs <| Semiring (Matrix n n A)
 
-set_option backward.inferInstanceAs.wrap false in
 instance instRing [Fintype n] [DecidableEq n] [Ring A] : Ring (CStarMatrix n n A) :=
   inferInstanceAs <| Ring (Matrix n n A)
 
diff --git a/Mathlib/GroupTheory/Abelianization/Defs.lean b/Mathlib/GroupTheory/Abelianization/Defs.lean
index 950c5ca84135b7..ef2b4d1b467194 100644
--- a/Mathlib/GroupTheory/Abelianization/Defs.lean
+++ b/Mathlib/GroupTheory/Abelianization/Defs.lean
@@ -40,8 +40,6 @@ def Abelianization : Type u :=
 
 namespace Abelianization
 
-attribute [local instance] QuotientGroup.leftRel
-
 instance commGroup : CommGroup (Abelianization G) where
   __ := QuotientGroup.Quotient.group _
   mul_comm x y := Quotient.inductionOn₂ x y fun a b ↦ Quotient.sound' <|
diff --git a/Mathlib/GroupTheory/FreeAbelianGroup.lean b/Mathlib/GroupTheory/FreeAbelianGroup.lean
index 86c2d955ee513e..bc7ab476fce41b 100644
--- a/Mathlib/GroupTheory/FreeAbelianGroup.lean
+++ b/Mathlib/GroupTheory/FreeAbelianGroup.lean
@@ -172,8 +172,6 @@ instance [Nonempty α] : Nontrivial (FreeAbelianGroup α) where
 
 end
 
-attribute [local instance] QuotientGroup.leftRel
-
 @[elab_as_elim]
 protected theorem induction_on
     {motive : FreeAbelianGroup α → Prop} (z : FreeAbelianGroup α) (zero : motive 0)
diff --git a/Mathlib/Topology/MetricSpace/Gluing.lean b/Mathlib/Topology/MetricSpace/Gluing.lean
index 843aeb1d0dc9ef..0c3d873c6adce0 100644
--- a/Mathlib/Topology/MetricSpace/Gluing.lean
+++ b/Mathlib/Topology/MetricSpace/Gluing.lean
@@ -592,8 +592,6 @@ def inductivePremetric (I : ∀ n, Isometry (f n)) : PseudoMetricSpace (Σ n, X
       _ = inductiveLimitDist f x y + inductiveLimitDist f y z := by
         rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y z m hy hz]
 
-attribute [local instance] inductivePremetric
-
 /-- The type giving the inductive limit in a metric space context. -/
 def InductiveLimit (I : ∀ n, Isometry (f n)) : Type _ :=
   @SeparationQuotient _ (inductivePremetric I).toUniformSpace.toTopologicalSpace
diff --git a/MathlibTest/ToDual.lean b/MathlibTest/ToDual.lean
index b9bb47f4ad4a2b..f7958b84b06ade 100644
--- a/MathlibTest/ToDual.lean
+++ b/MathlibTest/ToDual.lean
@@ -32,8 +32,8 @@ structure Lattice (α : Type) extends SemilatticeInf α, SemilatticeSup α
 attribute [to_dual existing] Lattice.toSemilatticeInf
 
 -- we can reorder arguments of arguments in `SemilatticeInf.mk`
-@[to_dual]
-instance [Min α] (le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c) : SemilatticeInf α where
+@[to_dual, reducible]
+def le_inf_test [Min α] (le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c) : SemilatticeInf α where
   le_inf
 
 -- we can reorder arguments of arguments of arguments in `SemilatticeInf.casesOn`
diff --git a/MathlibTest/globalAttributeIn.lean b/MathlibTest/globalAttributeIn.lean
index 56ced2d39e8426..1c124f2b4d4ed0 100644
--- a/MathlibTest/globalAttributeIn.lean
+++ b/MathlibTest/globalAttributeIn.lean
@@ -8,28 +8,30 @@ import Mathlib.Tactic.Linter.GlobalAttributeIn
 
 /-! Tests for the `globalAttributeIn` linter. -/
 
--- After https://github.com/leanprover/lean4/pull/12263,
--- we need to add `instance_reducible` before we can add `instance` to `Int.add`.
-set_option allowUnsafeReducibility true in
-attribute [instance_reducible] Int.add
+-- Since lean4#13223 applying a global attribute using ... `in` ... is an error
+
+class Dummy where
+  field : True
+
+@[reducible] def dummyInst : Dummy := ⟨True.intro⟩
 
 /--
-error: Despite the `in`, the attribute instance 1100 is added globally to Int.add
+error: Despite the `in`, the attribute instance 1100 is added globally to dummyInst
 please remove the `in` or make this a `local instance 1100`
 -/
 #guard_msgs in
 set_option autoImplicit false in
-attribute [instance 1100] Int.add in
+attribute [instance 1100] dummyInst in
 set_option autoImplicit false in
 instance : Inhabited Int where
   default := 0
 
 /--
-error: Despite the `in`, the attribute instance is added globally to Int.add
+error: Despite the `in`, the attribute instance is added globally to dummyInst
 please remove the `in` or make this a `local instance`
 -/
 #guard_msgs in
-attribute [instance] Int.add in
+attribute [instance] dummyInst in
 instance : Inhabited Int where
   default := 0
 
@@ -58,42 +60,31 @@ please remove the `in` or make this a `local ext`
 -/
 #guard_msgs in
 set_option warning.simp.varHead false in
-attribute [simp, local simp, ext, scoped instance, -simp, -ext] foo in
+attribute [simp, local simp, ext, -simp, -ext] foo in
 def bar := False
 
 #guard_msgs in
 -- `local instance` is allowed with `in`
-attribute [local instance] Int.add in
+attribute [local instance] dummyInst in
 instance : Inhabited Int where
   default := 0
 
 #guard_msgs in
 -- `local instance priority` is allowed with `in`
-attribute [local instance 42] Int.add in
+attribute [local instance 42] dummyInst in
 instance : Inhabited Int where
   default := 0
 
 #guard_msgs in
 -- `scoped instance` is allowed with `in`
-attribute [scoped instance] Int.add in
+attribute [scoped instance] dummyInst in
 instance : Inhabited Int where
   default := 0
 
 #guard_msgs in
 -- `scoped instance priority` is allowed with `in`
-attribute [scoped instance 42] Int.add in
+attribute [scoped instance 42] dummyInst in
 instance : Inhabited Int where
   default := 0
 
 end X
-
--- Omitting the `in` is also fine.
-
-attribute [local instance 42] X.foo
-
--- Global instance without the `in` are also left alone.
-attribute [instance 20000] X.foo
-
-namespace X
-
-attribute [scoped instance 0] foo
diff --git a/lake-manifest.json b/lake-manifest.json
index 5714e5948fbf7c..aef5b0e480b807 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -35,20 +35,20 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "82d457fb3bdd9efadbae06608ff337d689efdddf",
+   "rev": "2db6054a44326f8c0230ee0570e2ddb894816511",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.97",
+   "inputRev": "v0.0.98",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ad416ddf6cc9d5b1c00eaf04a48e703538132760",
+   "rev": "bf91f5d1e444cf2bd9795bd2499658b802759af7",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "bf91f5d1e444cf2bd9795bd2499658b802759af7",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4b591181697264394a76288a163fd1d47621c96e",
+   "rev": "667d80cc94e379283e9f0216673fff456692fa5c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
diff --git a/lakefile.lean b/lakefile.lean
index ccb3d90f94a5d8..882b061737b683 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -8,7 +8,7 @@ open Lake DSL
 
 require "leanprover-community" / "batteries" @ git "nightly-testing"
 require "leanprover-community" / "Qq" @ git "nightly-testing"
-require "leanprover-community" / "aesop" @ git "nightly-testing"
+require "leanprover-community" / "aesop" @ git "bf91f5d1e444cf2bd9795bd2499658b802759af7"
 require "leanprover-community" / "proofwidgets" @ git "v0.0.98"
   with NameMap.empty.insert `errorOnBuild
     "ProofWidgets failed to reuse pre-built JS code. \
diff --git a/lean-toolchain b/lean-toolchain
index 844e3659d22483..1883470497275d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-04-16
+leanprover/lean4:nightly-2026-04-19