From 45fab6c6c4c307196408a1b61c69f1ae8178b3a2 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Fri, 23 Feb 2024 18:09:26 +0000
Subject: [PATCH] chore: classify `added instance` porting notes (#10884)

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.
---
 Mathlib/Geometry/RingedSpace/OpenImmersion.lean     | 6 +++---
 Mathlib/GroupTheory/SpecificGroups/Alternating.lean | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
index ccb7c8267fed6..6a3d81fb6fb19 100644
--- a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
+++ b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
@@ -1147,14 +1147,14 @@ image is contained in the image of `f`, we can lift this morphism to a unique `Y
 commutes with these maps.
 -/
 def lift (H' : Set.range g.1.base ⊆ Set.range f.1.base) : Y ⟶ X :=
-  -- Porting note: added instance manually
+  -- Porting note (#10754): added instance manually
   have := pullback_snd_isIso_of_range_subset f g H'
   inv (pullback.snd : pullback f g ⟶ _) ≫ pullback.fst
 #align algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift
 
 @[simp, reassoc]
 theorem lift_fac (H' : Set.range g.1.base ⊆ Set.range f.1.base) : lift f g H' ≫ f = g := by
-  -- Porting note: added instance manually
+  -- Porting note (#10754): added instance manually
   haveI := pullback_snd_isIso_of_range_subset f g H'
   erw [Category.assoc]; rw [IsIso.inv_comp_eq]; exact pullback.condition
 #align algebraic_geometry.LocallyRingedSpace.is_open_immersion.lift_fac AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_fac
@@ -1165,7 +1165,7 @@ theorem lift_uniq (H' : Set.range g.1.base ⊆ Set.range f.1.base) (l : Y ⟶ X)
 
 theorem lift_range (H' : Set.range g.1.base ⊆ Set.range f.1.base) :
     Set.range (lift f g H').1.base = f.1.base ⁻¹' Set.range g.1.base := by
-  -- Porting note: added instance manually
+  -- Porting note (#10754): added instance manually
   have := pullback_snd_isIso_of_range_subset f g H'
   dsimp only [lift]
   have : _ = (pullback.fst : pullback f g ⟶ _).val.base :=
diff --git a/Mathlib/GroupTheory/SpecificGroups/Alternating.lean b/Mathlib/GroupTheory/SpecificGroups/Alternating.lean
index 74556f7c6f5e7..fc9356256243f 100644
--- a/Mathlib/GroupTheory/SpecificGroups/Alternating.lean
+++ b/Mathlib/GroupTheory/SpecificGroups/Alternating.lean
@@ -51,7 +51,7 @@ def alternatingGroup : Subgroup (Perm α) :=
   sign.ker
 #align alternating_group alternatingGroup
 
--- Porting note: manually added instance
+-- Porting note (#10754): manually added instance
 instance fta : Fintype (alternatingGroup α) :=
   @Subtype.fintype _ _ sign.decidableMemKer _