chore: classify added proof porting notes (#10889)

Classifies by adding issue number (#10888) to porting notes claiming `added proof`.

Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

@@ -85,7 +85,7 @@ def conesEquivFunctor (B : C) {J : Type w} (F : Discrete J ⥤ Over B) :
     { pt := Over.mk (c.π.app none)
       π :=
         { app := fun ⟨j⟩ => Over.homMk (c.π.app (some j)) (c.w (WidePullbackShape.Hom.term j))
-          -- Porting note: Added a proof for `naturality`
+          -- Porting note (#10888): added proof for `naturality`
           naturality := fun ⟨X⟩ ⟨Y⟩ ⟨⟨f⟩⟩ => by dsimp at f ⊢; aesop_cat } }
   map f := { hom := Over.homMk f.hom }
 #align category_theory.over.construct_products.cones_equiv_functor CategoryTheory.Over.ConstructProducts.conesEquivFunctor

Mathlib/Topology/Compactness/Paracompact.lean

@@ -99,7 +99,7 @@ indexed by the same type. -/
 theorem precise_refinement_set [ParacompactSpace X] {s : Set X} (hs : IsClosed s) (u : ι → Set X)
     (uo : ∀ i, IsOpen (u i)) (us : s ⊆ ⋃ i, u i) :
     ∃ v : ι → Set X, (∀ i, IsOpen (v i)) ∧ (s ⊆ ⋃ i, v i) ∧ LocallyFinite v ∧ ∀ i, v i ⊆ u i := by
-  -- Porting note: Added proof of uc
+  -- Porting note (#10888): added proof of uc
   have uc : (iUnion fun i => Option.elim' sᶜ u i) = univ := by
     apply Subset.antisymm (subset_univ _)
     · simp_rw [← compl_union_self s, Option.elim', iUnion_option]

Mathlib/Topology/ContinuousFunction/Bounded.lean

@@ -217,7 +217,7 @@ instance : PseudoMetricSpace (α →ᵇ β) where
   dist_comm f g := by simp [dist_eq, dist_comm]
   dist_triangle f g h := (dist_le (add_nonneg dist_nonneg' dist_nonneg')).2
     fun x => le_trans (dist_triangle _ _ _) (add_le_add (dist_coe_le_dist _) (dist_coe_le_dist _))
-  -- Porting note: Added proof for `edist_dist`
+  -- Porting note (#10888): added proof for `edist_dist`
   edist_dist x y := by dsimp; congr; simp [dist_nonneg']
 
 /-- The type of bounded continuous functions, with the uniform distance, is a metric space. -/
@@ -999,7 +999,7 @@ instance seminormedAddCommGroup : SeminormedAddCommGroup (α →ᵇ β) where
 instance normedAddCommGroup {α β} [TopologicalSpace α] [NormedAddCommGroup β] :
     NormedAddCommGroup (α →ᵇ β) :=
   { BoundedContinuousFunction.seminormedAddCommGroup with
-    -- Porting note: Added a proof for `eq_of_dist_eq_zero`
+    -- Porting note (#10888): added proof for `eq_of_dist_eq_zero`
     eq_of_dist_eq_zero }
 
 theorem nnnorm_def : ‖f‖₊ = nndist f 0 := rfl
@@ -1334,12 +1334,12 @@ instance commRing [SeminormedCommRing R] : CommRing (α →ᵇ R) :=
 
 instance [SeminormedCommRing R] : SeminormedCommRing (α →ᵇ R) :=
   { BoundedContinuousFunction.commRing, BoundedContinuousFunction.seminormedAddCommGroup with
-    -- Porting note: Added proof for `norm_mul`
+    -- Porting note (#10888): added proof for `norm_mul`
     norm_mul := norm_mul_le }
 
 instance [NormedCommRing R] : NormedCommRing (α →ᵇ R) :=
   { BoundedContinuousFunction.commRing, BoundedContinuousFunction.normedAddCommGroup with
-    -- Porting note: Added proof for `norm_mul`
+    -- Porting note (#10888): added proof for `norm_mul`
     norm_mul := norm_mul_le }
 
 end NormedCommRing
@@ -1578,7 +1578,7 @@ instance : NormedLatticeAddCommGroup (α →ᵇ β) :=
       have i1 : ∀ t, ‖f t‖ ≤ ‖g t‖ := fun t => HasSolidNorm.solid (h t)
       rw [norm_le (norm_nonneg _)]
       exact fun t => (i1 t).trans (norm_coe_le_norm g t)
-    -- Porting note: Added a proof for `eq_of_dist_eq_zero`
+    -- Porting note (#10888): added proof for `eq_of_dist_eq_zero`
     eq_of_dist_eq_zero }
 
 end NormedLatticeOrderedGroup

Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

@@ -442,7 +442,7 @@ def premetricOptimalGHDist : PseudoMetricSpace (X ⊕ Y) where
   dist_self x := candidates_refl (optimalGHDist_mem_candidatesB X Y)
   dist_comm x y := candidates_symm (optimalGHDist_mem_candidatesB X Y)
   dist_triangle x y z := candidates_triangle (optimalGHDist_mem_candidatesB X Y)
-  -- Porting note: Added a proof for `edist_dist`
+  -- Porting note (#10888): added proof for `edist_dist`
   edist_dist x y := by
     simp only
     congr