chore: add issue number to instance was not necessary porting notes (…

…#10671)

Adds issue number (#10670) to porting notes claiming `instance was not necessary`.

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -59,7 +59,7 @@ instance : CoeSort GroupCat (Type*) where
 @[to_additive]
 instance (X : GroupCat) : Group X := X.str
 
--- porting note: this instance was not necessary in mathlib
+-- porting note (#10670): this instance was not necessary in mathlib
 @[to_additive]
 instance {X Y : GroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
   coe (f : X →* Y) := f
@@ -121,7 +121,7 @@ set_option linter.uppercaseLean3 false in
 @[to_additive]
 instance : Coe GroupCat.{u} MonCat.{u} where coe := (forget₂ GroupCat MonCat).obj
 
--- porting note: this instance was not necessary in mathlib
+-- porting note (#10670): this instance was not necessary in mathlib
 @[to_additive]
 instance (G H : GroupCat) : One (G ⟶ H) := (inferInstance : One (MonoidHom G H))
 
@@ -208,7 +208,7 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddCommGroup.add_comm_group_instance AddCommGroupCat.addCommGroupInstance
 
--- porting note: this instance was not necessary in mathlib
+-- porting note (#10670): this instance was not necessary in mathlib
 @[to_additive]
 instance {X Y : CommGroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
   coe (f : X →* Y) := f
@@ -295,7 +295,7 @@ set_option linter.uppercaseLean3 false in
 @[to_additive]
 instance : Coe CommGroupCat.{u} CommMonCat.{u} where coe := (forget₂ CommGroupCat CommMonCat).obj
 
--- porting note: this instance was not necessary in mathlib
+-- porting note (#10670): this instance was not necessary in mathlib
 @[to_additive]
 instance (G H : CommGroupCat) : One (G ⟶ H) := (inferInstance : One (MonoidHom G H))
 

Mathlib/Algebra/Category/GroupCat/Preadditive.lean

@@ -18,7 +18,7 @@ universe u
 
 namespace AddCommGroupCat
 
--- porting note: this instance was not necessary in mathlib
+-- porting note (#10670): this instance was not necessary in mathlib
 instance (P Q : AddCommGroupCat) : AddCommGroup (P ⟶ Q) :=
   (inferInstance : AddCommGroup (AddMonoidHom P Q))
 

Mathlib/Algebra/Category/MonCat/Basic.lean

@@ -80,7 +80,7 @@ instance : CoeSort MonCat (Type*) where
 @[to_additive]
 instance (X : MonCat) : Monoid X := X.str
 
--- porting note: this instance was not necessary in mathlib
+-- porting note (#10670): this instance was not necessary in mathlib
 @[to_additive]
 instance {X Y : MonCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
   coe (f : X →* Y) := f
@@ -206,7 +206,7 @@ instance : CoeSort CommMonCat (Type*) where
 @[to_additive]
 instance (X : CommMonCat) : CommMonoid X := X.str
 
--- porting note: this instance was not necessary in mathlib
+-- porting note (#10670): this instance was not necessary in mathlib
 @[to_additive]
 instance {X Y : CommMonCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
   coe (f : X →* Y) := f

Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

@@ -182,7 +182,7 @@ theorem targetAffineLocallyOfOpenCover {P : AffineTargetMorphismProperty} (hP :
     haveI : IsAffine _ := U.2
     have := hP.2 (f ∣_ U.1)
     replace this := this (Y.presheaf.map (eqToHom U.1.openEmbedding_obj_top).op r) h
-    -- Porting note : the following 2 instances was not necessary
+    -- Porting note (#10670): the following 2 instances was not necessary
     haveI i1 : IsAffine (Y.restrict (Scheme.affineBasicOpen Y r).1.openEmbedding) :=
       (Scheme.affineBasicOpen Y r).2
     haveI i2 : IsAffine
@@ -210,7 +210,7 @@ theorem targetAffineLocallyOfOpenCover {P : AffineTargetMorphismProperty} (hP :
     · rintro ⟨r, hr⟩
       obtain ⟨r, hr', rfl⟩ := Finset.mem_image.mp hr
       specialize H ⟨r, hr'⟩
-      -- Porting note : the following 2 instances was not necessary
+      -- Porting note (#10670): the following 2 instances was not necessary
       haveI i1 : IsAffine (Y.restrict (Scheme.affineBasicOpen Y r).1.openEmbedding) :=
         (Scheme.affineBasicOpen Y r).2
       haveI i2 : IsAffine
@@ -226,7 +226,7 @@ theorem targetAffineLocallyOfOpenCover {P : AffineTargetMorphismProperty} (hP :
     exact ⟨⟨_, ⟨𝒰.f x, rfl⟩⟩, 𝒰.Covers x⟩
   · rintro ⟨_, i, rfl⟩
     specialize h𝒰 i
-    -- Porting note : the next instance was not necessary
+    -- Porting note (#10670): the next instance was not necessary
     haveI i1 : IsAffine (Y.restrict (S i).1.openEmbedding) := (S i).2
     rw [← P.toProperty_apply] at h𝒰 ⊢
     exact (hP.1.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr h𝒰

Mathlib/Geometry/RingedSpace/Basic.lean

@@ -47,7 +47,7 @@ open SheafedSpace
 
 variable (X : RingedSpace)
 
--- Porting note : this was not necessary in mathlib3
+-- Porting note (#10670): this was not necessary in mathlib3
 instance : CoeSort RingedSpace (Type*) where
   coe X := X.carrier
 

Mathlib/Order/Category/NonemptyFinLinOrd.lean

@@ -143,7 +143,7 @@ instance {A B : NonemptyFinLinOrd.{u}} : FunLike (A ⟶ B) A B where
     ext x
     exact congr_fun h x
 
--- porting note: this instance was not necessary in mathlib
+-- porting note (#10670): this instance was not necessary in mathlib
 instance {A B : NonemptyFinLinOrd.{u}} : OrderHomClass (A ⟶ B) A B where
   map_rel f _ _ h := f.monotone h