diff --git a/Mathlib/Algebra/Category/FGModuleCat/Basic.lean b/Mathlib/Algebra/Category/FGModuleCat/Basic.lean
index ec81058f733f55..9c83f276980cf7 100644
--- a/Mathlib/Algebra/Category/FGModuleCat/Basic.lean
+++ b/Mathlib/Algebra/Category/FGModuleCat/Basic.lean
@@ -185,19 +185,19 @@ def forget₂Monoidal : MonoidalFunctor (FGModuleCat R) (ModuleCat.{u} R) :=
 
 instance forget₂Monoidal_faithful : Faithful (forget₂Monoidal R).toFunctor := by
   dsimp [forget₂Monoidal]
-  -- Porting note: was `infer_instance`
+  -- Porting note (#11187): was `infer_instance`
   exact FullSubcategory.faithful _
 #align fgModule.forget₂_monoidal_faithful FGModuleCat.forget₂Monoidal_faithful
 
 instance forget₂Monoidal_additive : (forget₂Monoidal R).toFunctor.Additive := by
   dsimp [forget₂Monoidal]
-  -- Porting note: was `infer_instance`
+  -- Porting note (#11187): was `infer_instance`
   exact Functor.fullSubcategoryInclusion_additive _
 #align fgModule.forget₂_monoidal_additive FGModuleCat.forget₂Monoidal_additive
 
 instance forget₂Monoidal_linear : (forget₂Monoidal R).toFunctor.Linear R := by
   dsimp [forget₂Monoidal]
-  -- Porting note: was `infer_instance`
+  -- Porting note (#11187): was `infer_instance`
   exact Functor.fullSubcategoryInclusionLinear _ _
 #align fgModule.forget₂_monoidal_linear FGModuleCat.forget₂Monoidal_linear
 
@@ -222,7 +222,7 @@ instance closedPredicateModuleFinite :
 
 instance : MonoidalClosed (FGModuleCat K) := by
   dsimp [FGModuleCat]
-  -- Porting note: was `infer_instance`
+  -- Porting note (#11187): was `infer_instance`
   exact MonoidalCategory.fullMonoidalClosedSubcategory
     (fun V : ModuleCat.{u} K => Module.Finite K V)
 
diff --git a/Mathlib/AlgebraicGeometry/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/OpenImmersion.lean
index 006b20f26731a5..7eb61c720b5133 100644
--- a/Mathlib/AlgebraicGeometry/OpenImmersion.lean
+++ b/Mathlib/AlgebraicGeometry/OpenImmersion.lean
@@ -59,7 +59,7 @@ protected def scheme (X : LocallyRingedSpace)
     skip
     apply PresheafedSpace.IsOpenImmersion.isoOfRangeEq (PresheafedSpace.ofRestrict _ _) f.1
     · exact Subtype.range_coe_subtype
-    · exact Opens.openEmbedding _ -- Porting note: was `infer_instance`
+    · exact Opens.openEmbedding _ -- Porting note (#11187): was `infer_instance`
 #align algebraic_geometry.LocallyRingedSpace.IsOpenImmersion.Scheme AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.scheme
 
 end LocallyRingedSpace.IsOpenImmersion
diff --git a/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean b/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
index d1ecf3f8476838..438d9ad181cc8d 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
@@ -189,7 +189,7 @@ theorem card_filter_equitabilise_small (hm : m ≠ 0) :
 theorem card_parts_equitabilise (hm : m ≠ 0) : (P.equitabilise h).parts.card = a + b := by
   rw [← filter_true_of_mem fun x => card_eq_of_mem_parts_equitabilise, filter_or,
     card_union_of_disjoint, P.card_filter_equitabilise_small _ hm, P.card_filter_equitabilise_big]
-  -- Porting note: was `infer_instance`
+  -- Porting note (#11187): was `infer_instance`
   exact disjoint_filter.2 fun x _ h₀ h₁ => Nat.succ_ne_self m <| h₁.symm.trans h₀
 #align finpartition.card_parts_equitabilise Finpartition.card_parts_equitabilise