diff --git a/Mathlib/Algebra/Invertible/Defs.lean b/Mathlib/Algebra/Invertible/Defs.lean
index e2c27988ece5ec..1c53a6e5ca8b08 100644
--- a/Mathlib/Algebra/Invertible/Defs.lean
+++ b/Mathlib/Algebra/Invertible/Defs.lean
@@ -45,7 +45,7 @@ variables {α : Type*} [Monoid α]
 def something_that_needs_inverses (x : α) [Invertible x] := sorry
 
 section
-local attribute [instance] invertibleOne
+attribute [local instance] invertibleOne
 def something_one := something_that_needs_inverses 1
 end
 ```
diff --git a/Mathlib/Analysis/NormedSpace/MatrixExponential.lean b/Mathlib/Analysis/NormedSpace/MatrixExponential.lean
index 1b5667dc366d9b..623189753a84a2 100644
--- a/Mathlib/Analysis/NormedSpace/MatrixExponential.lean
+++ b/Mathlib/Analysis/NormedSpace/MatrixExponential.lean
@@ -29,7 +29,7 @@ Lemmas like `exp_add_of_commute` require a canonical norm on the type; while the
 sensible choices for the norm of a `Matrix` (`Matrix.normedAddCommGroup`,
 `Matrix.frobeniusNormedAddCommGroup`, `Matrix.linftyOpNormedAddCommGroup`), none of them
 are canonical. In an application where a particular norm is chosen using
-`local attribute [instance]`, then the usual lemmas about `exp` are fine. When choosing a norm is
+`attribute [local instance]`, then the usual lemmas about `exp` are fine. When choosing a norm is
 undesirable, the results in this file can be used.
 
 In this file, we copy across the lemmas about `exp`, but hide the requirement for a norm inside the
diff --git a/Mathlib/CategoryTheory/EqToHom.lean b/Mathlib/CategoryTheory/EqToHom.lean
index cdd6df33260d7f..a41a5ae10f8773 100644
--- a/Mathlib/CategoryTheory/EqToHom.lean
+++ b/Mathlib/CategoryTheory/EqToHom.lean
@@ -300,7 +300,7 @@ end Functor
 as we lose the ability to use results that interact with `F`,
 e.g. the naturality of a natural transformation.
 
-In some files it may be appropriate to use `local attribute [simp] eqToHom_map`, however.
+In some files it may be appropriate to use `attribute [local simp] eqToHom_map`, however.
 -/
 theorem eqToHom_map (F : C ⥤ D) {X Y : C} (p : X = Y) :
     F.map (eqToHom p) = eqToHom (congr_arg F.obj p) := by cases p; simp
diff --git a/Mathlib/CategoryTheory/Limits/Pi.lean b/Mathlib/CategoryTheory/Limits/Pi.lean
index be7a30790cb12c..360f07831e3606 100644
--- a/Mathlib/CategoryTheory/Limits/Pi.lean
+++ b/Mathlib/CategoryTheory/Limits/Pi.lean
@@ -144,7 +144,7 @@ With the addition of
 `import CategoryTheory.Limits.Shapes.Types`
 we can use:
 ```
-local attribute [instance] hasLimit_of_hasLimit_comp_eval
+attribute [local instance] hasLimit_of_hasLimit_comp_eval
 example : hasBinaryProducts (I → Type v₁) := ⟨by infer_instance⟩
 ```
 -/
diff --git a/Mathlib/CategoryTheory/Types.lean b/Mathlib/CategoryTheory/Types.lean
index 35456798097a1e..6c2727485d1ea6 100644
--- a/Mathlib/CategoryTheory/Types.lean
+++ b/Mathlib/CategoryTheory/Types.lean
@@ -396,7 +396,7 @@ instance : SplitEpiCategory (Type u) where
 end CategoryTheory
 
 -- We prove `equivIsoIso` and then use that to sneakily construct `equivEquivIso`.
--- (In this order the proofs are handled by `obviously`.)
+-- (In this order the proofs are handled by `aesop_cat`.)
 /-- Equivalences (between types in the same universe) are the same as (isomorphic to) isomorphisms
 of types. -/
 @[simps]
diff --git a/Mathlib/Data/Prod/TProd.lean b/Mathlib/Data/Prod/TProd.lean
index 0a9d0066fce5e4..fb6d7969bd1b04 100644
--- a/Mathlib/Data/Prod/TProd.lean
+++ b/Mathlib/Data/Prod/TProd.lean
@@ -24,7 +24,7 @@ construction/theorem that is easier to define/prove on binary products than on f
 * Then we can use the equivalence `List.TProd.piEquivTProd` below (or enhanced versions of it,
   like a `MeasurableEquiv` for product measures) to get the construction on `∀ i : ι, α i`, at
   least when assuming `[Fintype ι] [Encodable ι]` (using `Encodable.sortedUniv`).
-  Using `local attribute [instance] Fintype.toEncodable` we can get rid of the argument
+  Using `attribute [local instance] Fintype.toEncodable` we can get rid of the argument
   `[Encodable ι]`.
 
 ## Main definitions
diff --git a/Mathlib/Logic/Equiv/List.lean b/Mathlib/Logic/Equiv/List.lean
index 549d6baa791cff..f55c6bb1faca3a 100644
--- a/Mathlib/Logic/Equiv/List.lean
+++ b/Mathlib/Logic/Equiv/List.lean
@@ -139,7 +139,7 @@ def _root_.Fintype.truncEncodable (α : Type*) [DecidableEq α] [Fintype α] : T
 
 /-- A noncomputable way to arbitrarily choose an ordering on a finite type.
 It is not made into a global instance, since it involves an arbitrary choice.
-This can be locally made into an instance with `local attribute [instance] Fintype.toEncodable`. -/
+This can be locally made into an instance with `attribute [local instance] Fintype.toEncodable`. -/
 noncomputable def _root_.Fintype.toEncodable (α : Type*) [Fintype α] : Encodable α := by
   classical exact (Fintype.truncEncodable α).out
 #align fintype.to_encodable Fintype.toEncodable
diff --git a/Mathlib/RingTheory/Bezout.lean b/Mathlib/RingTheory/Bezout.lean
index a90da2b0e911c8..9b18d649f959f7 100644
--- a/Mathlib/RingTheory/Bezout.lean
+++ b/Mathlib/RingTheory/Bezout.lean
@@ -95,7 +95,7 @@ end Gcd
 
 attribute [local instance] toGCDDomain
 
--- Note that the proof depends on the `local attribute [instance]` above, and is thus necessary to
+-- Note that the proof depends on the `attribute [local instance]` above, and is thus necessary to
 -- be stated.
 instance (priority := 100) [IsDomain R] [IsBezout R] : IsIntegrallyClosed R := by
   classical exact GCDMonoid.toIsIntegrallyClosed