diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean
index 3b835150026483..23b27d5abf5f41 100644
--- a/Mathlib/Algebra/DirectSum/Basic.lean
+++ b/Mathlib/Algebra/DirectSum/Basic.lean
@@ -40,11 +40,11 @@ def DirectSum [∀ i, AddCommMonoid (β i)] : Type _ :=
   Π₀ i, β i
 #align direct_sum DirectSum
 
--- Porting note: Added inhabited instance manually
+-- Porting note (#10754): Added inhabited instance manually
 instance [∀ i, AddCommMonoid (β i)] : Inhabited (DirectSum ι β) :=
   inferInstanceAs (Inhabited (Π₀ i, β i))
 
--- Porting note: Added addCommMonoid instance manually
+-- Porting note (#10754): Added addCommMonoid instance manually
 instance [∀ i, AddCommMonoid (β i)] : AddCommMonoid (DirectSum ι β) :=
   inferInstanceAs (AddCommMonoid (Π₀ i, β i))
 
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean b/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
index 7734abca5199ef..a4c70c355c3943 100644
--- a/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
+++ b/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
@@ -132,7 +132,7 @@ theorem targetAffineLocally_respectsIso {P : AffineTargetMorphismProperty}
     (hP : P.toProperty.RespectsIso) : (targetAffineLocally P).RespectsIso := by
   constructor
   · introv H U
-    -- Porting note: added this instance
+    -- Porting note (#10754): added this instance
     haveI : IsAffine _ := U.prop
     rw [morphismRestrict_comp, affine_cancel_left_isIso hP]
     exact H U
@@ -265,7 +265,7 @@ theorem AffineTargetMorphismProperty.IsLocal.affine_openCover_TFAE
     refine' ⟨Y.openCoverOfSuprEqTop U hU, hU', _⟩
     intro i
     specialize H i
-    -- Porting note: added these two instances manually
+    -- Porting note (#10754): added these two instances manually
     haveI i2 : IsAffine (Scheme.OpenCover.obj (Scheme.openCoverOfSuprEqTop Y U hU) i) := hU' i
     haveI i3 : IsAffine (Y.restrict (U i).openEmbedding) := hU' i
     rw [← P.toProperty_apply, ← hP.1.arrow_mk_iso_iff (morphismRestrictOpensRange f _)]
diff --git a/Mathlib/Analysis/NormedSpace/Extend.lean b/Mathlib/Analysis/NormedSpace/Extend.lean
index c9160ce453821a..933528b4f5cf7f 100644
--- a/Mathlib/Analysis/NormedSpace/Extend.lean
+++ b/Mathlib/Analysis/NormedSpace/Extend.lean
@@ -141,7 +141,7 @@ theorem norm_extendTo𝕜' (fr : F →L[ℝ] ℝ) : ‖(fr.extendTo𝕜' : F →
 
 end ContinuousLinearMap
 
--- Porting note: Added a new instance. This instance is needed for the rest of the file.
+-- Porting note (#10754): Added a new instance. This instance is needed for the rest of the file.
 instance : NormedSpace 𝕜 (RestrictScalars ℝ 𝕜 F) := by
   unfold RestrictScalars
   infer_instance
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
index 004101c3955f2b..751599191024fd 100644
--- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
@@ -32,15 +32,15 @@ def Angle : Type :=
 
 namespace Angle
 
--- Porting note: added due to missing instances due to no deriving
+-- Porting note (#10754): added due to missing instances due to no deriving
 instance : NormedAddCommGroup Angle :=
   inferInstanceAs (NormedAddCommGroup (AddCircle (2 * π)))
 
--- Porting note: added due to missing instances due to no deriving
+-- Porting note (#10754): added due to missing instances due to no deriving
 instance : Inhabited Angle :=
   inferInstanceAs (Inhabited (AddCircle (2 * π)))
 
--- Porting note: added due to missing instances due to no deriving
+-- Porting note (#10754): added due to missing instances due to no deriving
 -- also, without this, a plain `QuotientAddGroup.mk`
 -- causes coerced terms to be of type `ℝ ⧸ AddSubgroup.zmultiples (2 * π)`
 /-- The canonical map from `ℝ` to the quotient `Angle`. -/
diff --git a/Mathlib/CategoryTheory/Closed/Ideal.lean b/Mathlib/CategoryTheory/Closed/Ideal.lean
index 467f43b6106510..35b2de3392fb49 100644
--- a/Mathlib/CategoryTheory/Closed/Ideal.lean
+++ b/Mathlib/CategoryTheory/Closed/Ideal.lean
@@ -149,7 +149,7 @@ variable [ExponentialIdeal i]
 itself cartesian closed.
 -/
 def cartesianClosedOfReflective : CartesianClosed D :=
-  { monoidalOfHasFiniteProducts D with -- Porting note: Added this instance
+  { monoidalOfHasFiniteProducts D with -- Porting note (#10754): added this instance
     closed := fun B =>
       { isAdj :=
           { right := i ⋙ exp (i.obj B) ⋙ leftAdjoint i
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
index bef40e0ef27e0f..34225970c7500c 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
@@ -1123,7 +1123,7 @@ end
 
 section
 
--- Porting note: added category instance as it did not propagate
+-- Porting note (#10754): added category instance as it did not propagate
 variable {C} [Category.{v} C] [HasBinaryCoproducts C]
 
 /-- The braiding isomorphism which swaps a binary coproduct. -/
@@ -1196,7 +1196,7 @@ end
 
 section ProdFunctor
 
--- Porting note: added category instance as it did not propagate
+-- Porting note (#10754): added category instance as it did not propagate
 variable {C} [Category.{v} C] [HasBinaryProducts C]
 
 /-- The binary product functor. -/
@@ -1219,7 +1219,7 @@ end ProdFunctor
 
 section CoprodFunctor
 
--- Porting note: added category instance as it did not propagate
+-- Porting note (#10754): added category instance as it did not propagate
 variable {C} [Category.{v} C] [HasBinaryCoproducts C]
 
 /-- The binary coproduct functor. -/
diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean
index 5bc6bf6216ddeb..6b2a07a9c9f077 100644
--- a/Mathlib/Data/NNRat/Defs.lean
+++ b/Mathlib/Data/NNRat/Defs.lean
@@ -35,7 +35,7 @@ def NNRat := { q : ℚ // 0 ≤ q } deriving
   CanonicallyOrderedCommSemiring, CanonicallyLinearOrderedAddCommMonoid, Sub, Inhabited
 #align nnrat NNRat
 
--- Porting note: Added these instances to get `OrderedSub, DenselyOrdered, Archimedean`
+-- Porting note (#10754): Added these instances to get `OrderedSub, DenselyOrdered, Archimedean`
 -- instead of `deriving` them
 instance : OrderedSub NNRat := Nonneg.orderedSub
 
diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean
index 4a6628b6f2ad7f..7ed66fe4ac19f3 100644
--- a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean
+++ b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean
@@ -317,7 +317,7 @@ variable [Algebra R L] [NoZeroSMulDivisors R L] [IsAlgClosure R L]
 
 /-- A (random) isomorphism between two algebraic closures of `R`. -/
 noncomputable def equiv : L ≃ₐ[R] M :=
-  -- Porting note: added to replace local instance above
+  -- Porting note (#10754): added to replace local instance above
   haveI : IsAlgClosed L := IsAlgClosure.alg_closed R
   haveI : IsAlgClosed M := IsAlgClosure.alg_closed R
   AlgEquiv.ofBijective _ (IsAlgClosure.algebraic.algHom_bijective₂
diff --git a/Mathlib/FieldTheory/IsSepClosed.lean b/Mathlib/FieldTheory/IsSepClosed.lean
index 7c9867860288e3..e7d1cbe393ecc7 100644
--- a/Mathlib/FieldTheory/IsSepClosed.lean
+++ b/Mathlib/FieldTheory/IsSepClosed.lean
@@ -267,7 +267,7 @@ variable [Algebra K L] [IsSepClosure K L]
 
 /-- A (random) isomorphism between two separable closures of `K`. -/
 noncomputable def equiv : L ≃ₐ[K] M :=
-  -- Porting note: added to replace local instance above
+  -- Porting note (#10754): added to replace local instance above
   haveI : IsSepClosed L := IsSepClosure.sep_closed K
   haveI : IsSepClosed M := IsSepClosure.sep_closed K
   AlgEquiv.ofBijective _ (Normal.isAlgebraic'.algHom_bijective₂
diff --git a/Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean b/Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
index 8f90c1a29fd6c9..73195104a4e936 100644
--- a/Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
+++ b/Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@@ -99,8 +99,8 @@ noncomputable def stalk (X : LocallyRingedSpace) (x : X) : CommRingCat :=
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.LocallyRingedSpace.stalk AlgebraicGeometry.LocallyRingedSpace.stalk
 
--- Porting note: added this instance to help Lean realize stalks are local (so that `0 ≠ 1`
--- works below)
+-- Porting note (#10754): added this instance to help Lean realize stalks are local
+-- (so that `0 ≠ 1` works below)
 instance stalkLocal (x : X) : LocalRing <| X.stalk x := X.localRing x
 
 /-- A morphism of locally ringed spaces `f : X ⟶ Y` induces
diff --git a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean
index 2bd33baa0bfb13..5314c7455fc8ee 100644
--- a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean
+++ b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean
@@ -425,7 +425,8 @@ theorem unifIntegrable_fin (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) {n : ℕ} {f
   revert f
   induction' n with n h
   · intro f hf
-    have : Subsingleton (Fin Nat.zero) := subsingleton_fin_zero -- Porting note: Added this instance
+  -- Porting note (#10754): added this instance
+    have : Subsingleton (Fin Nat.zero) := subsingleton_fin_zero
     exact unifIntegrable_subsingleton hp_one hp_top hf
   intro f hfLp ε hε
   let g : Fin n → α → β := fun k => f k
diff --git a/Mathlib/ModelTheory/DirectLimit.lean b/Mathlib/ModelTheory/DirectLimit.lean
index 0f7bb6d522e688..65b433cfd84d1b 100644
--- a/Mathlib/ModelTheory/DirectLimit.lean
+++ b/Mathlib/ModelTheory/DirectLimit.lean
@@ -166,7 +166,7 @@ def DirectLimit [DirectedSystem G fun i j h => f i j h] [IsDirected ι (· ≤ 
 
 attribute [local instance] DirectLimit.setoid
 
--- Porting note: Added local instance
+-- Porting note (#10754): Added local instance
 attribute [local instance] DirectLimit.sigmaStructure
 
 
diff --git a/Mathlib/Topology/Category/UniformSpace.lean b/Mathlib/Topology/Category/UniformSpace.lean
index 72ec1fd1d23471..4223c808c28e29 100644
--- a/Mathlib/Topology/Category/UniformSpace.lean
+++ b/Mathlib/Topology/Category/UniformSpace.lean
@@ -194,7 +194,7 @@ noncomputable def extensionHom {X : UniformSpaceCat} {Y : CpltSepUniformSpace}
   property := Completion.uniformContinuous_extension
 #align UniformSpace.extension_hom UniformSpaceCat.extensionHom
 
--- Porting note: added this instance to make things compile
+-- Porting note (#10754): added this instance to make things compile
 instance (X : UniformSpaceCat) : UniformSpace ((forget _).obj X) :=
   show UniformSpace X from inferInstance
 
diff --git a/Mathlib/Topology/Connected/PathConnected.lean b/Mathlib/Topology/Connected/PathConnected.lean
index 179c307b5406bc..4b9045d8930f92 100644
--- a/Mathlib/Topology/Connected/PathConnected.lean
+++ b/Mathlib/Topology/Connected/PathConnected.lean
@@ -84,7 +84,7 @@ instance Path.funLike : FunLike (Path x y) I X where
     simp only [DFunLike.coe_fn_eq] at h
     cases γ₁; cases γ₂; congr
 
--- porting note: added this instance so that we can use `FunLike.coe` for `CoeFun`
+-- Porting note (#10754): added this instance so that we can use `FunLike.coe` for `CoeFun`
 -- this also fixed very strange `simp` timeout issues
 instance Path.continuousMapClass : ContinuousMapClass (Path x y) I X where
   map_continuous := fun γ => show Continuous γ.toContinuousMap by continuity
diff --git a/Mathlib/Topology/FiberBundle/Constructions.lean b/Mathlib/Topology/FiberBundle/Constructions.lean
index b509f4a88a7d1a..84cd88a598f77b 100644
--- a/Mathlib/Topology/FiberBundle/Constructions.lean
+++ b/Mathlib/Topology/FiberBundle/Constructions.lean
@@ -41,7 +41,7 @@ namespace Trivial
 
 variable (B : Type*) (F : Type*)
 
--- Porting note: Added name for this instance.
+-- Porting note (#10754): Added name for this instance.
 -- TODO: use `TotalSpace.toProd`
 instance topologicalSpace [t₁ : TopologicalSpace B]
     [t₂ : TopologicalSpace F] : TopologicalSpace (TotalSpace F (Trivial B F)) :=