diff --git a/Mathlib/Data/Nat/PartENat.lean b/Mathlib/Data/Nat/PartENat.lean
index 9185c5feb5b06d..fd447b39dd5f67 100644
--- a/Mathlib/Data/Nat/PartENat.lean
+++ b/Mathlib/Data/Nat/PartENat.lean
@@ -680,7 +680,7 @@ def ofENat : ℕ∞ → PartENat :=
   | Option.none => none
   | Option.some n => some n
 
--- Porting note: new
+-- Porting note (#10754): new instance
 instance : Coe ℕ∞ PartENat := ⟨ofENat⟩
 
 -- Porting note: new. This could probably be moved to tests or removed.
diff --git a/Mathlib/Data/PNat/Defs.lean b/Mathlib/Data/PNat/Defs.lean
index 9e46eca4840db1..510f12cb0274ca 100644
--- a/Mathlib/Data/PNat/Defs.lean
+++ b/Mathlib/Data/PNat/Defs.lean
@@ -44,7 +44,7 @@ instance coePNatNat : Coe ℕ+ ℕ :=
 instance : Repr ℕ+ :=
   ⟨fun n n' => reprPrec n.1 n'⟩
 
--- Porting note: New instance not in Lean3
+--Porting note (#10754): New instance not in Lean3
 instance (n : ℕ) : OfNat ℕ+ (n+1) :=
   ⟨⟨n + 1, Nat.succ_pos n⟩⟩
 
diff --git a/Mathlib/InformationTheory/Hamming.lean b/Mathlib/InformationTheory/Hamming.lean
index 3e65c9a035ffb0..08e8e8cf03185d 100644
--- a/Mathlib/InformationTheory/Hamming.lean
+++ b/Mathlib/InformationTheory/Hamming.lean
@@ -450,7 +450,7 @@ theorem nndist_eq_hammingDist (x y : Hamming β) :
   rfl
 #align hamming.nndist_eq_hamming_dist Hamming.nndist_eq_hammingDist
 
--- Porting note: new
+-- Porting note (#10754): new instance
 instance : DiscreteTopology (Hamming β) := ⟨rfl⟩
 
 instance : MetricSpace (Hamming β) := .ofT0PseudoMetricSpace _
diff --git a/Mathlib/Init/Order/Defs.lean b/Mathlib/Init/Order/Defs.lean
index 73672ebce145a7..07479d154512db 100644
--- a/Mathlib/Init/Order/Defs.lean
+++ b/Mathlib/Init/Order/Defs.lean
@@ -129,7 +129,7 @@ theorem gt_of_ge_of_gt {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) : a > c :=
   lt_of_lt_of_le h₂ h₁
 #align gt_of_ge_of_gt gt_of_ge_of_gt
 
--- Porting note: new
+-- Porting note (#10754): new instance
 instance (priority := 900) : @Trans α α α LE.le LE.le LE.le := ⟨le_trans⟩
 instance (priority := 900) : @Trans α α α LT.lt LT.lt LT.lt := ⟨lt_trans⟩
 instance (priority := 900) : @Trans α α α LT.lt LE.le LT.lt := ⟨lt_of_lt_of_le⟩