chore: classify added instance porting notes (#10925)

Classifies by adding issue number (#10754) to porting notes claiming `added instance`.
leanprover-community · Apr 15, 2024 · 3ca0c05 · 3ca0c05
1 parent 29aef57
commit 3ca0c05
Show file tree

Hide file tree

Showing 15 changed files with 23 additions and 22 deletions.
diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean
@@ -40,11 +40,11 @@ def DirectSum [∀ i, AddCommMonoid (β i)] : Type _ :=
   Π₀ i, β i
 #align direct_sum DirectSum
 
--- Porting note: Added inhabited instance manually
+-- Porting note (#10754): Added inhabited instance manually
 instance [∀ i, AddCommMonoid (β i)] : Inhabited (DirectSum ι β) :=
   inferInstanceAs (Inhabited (Π₀ i, β i))
 
--- Porting note: Added addCommMonoid instance manually
+-- Porting note (#10754): Added addCommMonoid instance manually
 instance [∀ i, AddCommMonoid (β i)] : AddCommMonoid (DirectSum ι β) :=
   inferInstanceAs (AddCommMonoid (Π₀ i, β i))
 

diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean b/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
@@ -132,7 +132,7 @@ theorem targetAffineLocally_respectsIso {P : AffineTargetMorphismProperty}
     (hP : P.toProperty.RespectsIso) : (targetAffineLocally P).RespectsIso := by
   constructor
   · introv H U
-    -- Porting note: added this instance
+    -- Porting note (#10754): added this instance
     haveI : IsAffine _ := U.prop
     rw [morphismRestrict_comp, affine_cancel_left_isIso hP]
     exact H U
@@ -265,7 +265,7 @@ theorem AffineTargetMorphismProperty.IsLocal.affine_openCover_TFAE
     refine' ⟨Y.openCoverOfSuprEqTop U hU, hU', _⟩
     intro i
     specialize H i
-    -- Porting note: added these two instances manually
+    -- Porting note (#10754): added these two instances manually
     haveI i2 : IsAffine (Scheme.OpenCover.obj (Scheme.openCoverOfSuprEqTop Y U hU) i) := hU' i
     haveI i3 : IsAffine (Y.restrict (U i).openEmbedding) := hU' i
     rw [← P.toProperty_apply, ← hP.1.arrow_mk_iso_iff (morphismRestrictOpensRange f _)]

diff --git a/Mathlib/Analysis/NormedSpace/Extend.lean b/Mathlib/Analysis/NormedSpace/Extend.lean
@@ -141,7 +141,7 @@ theorem norm_extendTo𝕜' (fr : F →L[ℝ] ℝ) : ‖(fr.extendTo𝕜' : F →
 
 end ContinuousLinearMap
 
--- Porting note: Added a new instance. This instance is needed for the rest of the file.
+-- Porting note (#10754): Added a new instance. This instance is needed for the rest of the file.
 instance : NormedSpace 𝕜 (RestrictScalars ℝ 𝕜 F) := by
   unfold RestrictScalars
   infer_instance

diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
@@ -32,15 +32,15 @@ def Angle : Type :=
 
 namespace Angle
 
--- Porting note: added due to missing instances due to no deriving
+-- Porting note (#10754): added due to missing instances due to no deriving
 instance : NormedAddCommGroup Angle :=
   inferInstanceAs (NormedAddCommGroup (AddCircle (2 * π)))
 
--- Porting note: added due to missing instances due to no deriving
+-- Porting note (#10754): added due to missing instances due to no deriving
 instance : Inhabited Angle :=
   inferInstanceAs (Inhabited (AddCircle (2 * π)))
 
--- Porting note: added due to missing instances due to no deriving
+-- Porting note (#10754): added due to missing instances due to no deriving
 -- also, without this, a plain `QuotientAddGroup.mk`
 -- causes coerced terms to be of type `ℝ ⧸ AddSubgroup.zmultiples (2 * π)`
 /-- The canonical map from `ℝ` to the quotient `Angle`. -/

diff --git a/Mathlib/CategoryTheory/Closed/Ideal.lean b/Mathlib/CategoryTheory/Closed/Ideal.lean
@@ -149,7 +149,7 @@ variable [ExponentialIdeal i]
 itself cartesian closed.
 -/
 def cartesianClosedOfReflective : CartesianClosed D :=
-  { monoidalOfHasFiniteProducts D with -- Porting note: Added this instance
+  { monoidalOfHasFiniteProducts D with -- Porting note (#10754): added this instance
     closed := fun B =>
       { isAdj :=
           { right := i ⋙ exp (i.obj B) ⋙ leftAdjoint i

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
@@ -1123,7 +1123,7 @@ end
 
 section
 
--- Porting note: added category instance as it did not propagate
+-- Porting note (#10754): added category instance as it did not propagate
 variable {C} [Category.{v} C] [HasBinaryCoproducts C]
 
 /-- The braiding isomorphism which swaps a binary coproduct. -/
@@ -1196,7 +1196,7 @@ end
 
 section ProdFunctor
 
--- Porting note: added category instance as it did not propagate
+-- Porting note (#10754): added category instance as it did not propagate
 variable {C} [Category.{v} C] [HasBinaryProducts C]
 
 /-- The binary product functor. -/
@@ -1219,7 +1219,7 @@ end ProdFunctor
 
 section CoprodFunctor
 
--- Porting note: added category instance as it did not propagate
+-- Porting note (#10754): added category instance as it did not propagate
 variable {C} [Category.{v} C] [HasBinaryCoproducts C]
 
 /-- The binary coproduct functor. -/

diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean
@@ -35,7 +35,7 @@ def NNRat := { q : ℚ // 0 ≤ q } deriving
   CanonicallyOrderedCommSemiring, CanonicallyLinearOrderedAddCommMonoid, Sub, Inhabited
 #align nnrat NNRat
 
--- Porting note: Added these instances to get `OrderedSub, DenselyOrdered, Archimedean`
+-- Porting note (#10754): Added these instances to get `OrderedSub, DenselyOrdered, Archimedean`
 -- instead of `deriving` them
 instance : OrderedSub NNRat := Nonneg.orderedSub
 

diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean
@@ -317,7 +317,7 @@ variable [Algebra R L] [NoZeroSMulDivisors R L] [IsAlgClosure R L]
 
 /-- A (random) isomorphism between two algebraic closures of `R`. -/
 noncomputable def equiv : L ≃ₐ[R] M :=
-  -- Porting note: added to replace local instance above
+  -- Porting note (#10754): added to replace local instance above
   haveI : IsAlgClosed L := IsAlgClosure.alg_closed R
   haveI : IsAlgClosed M := IsAlgClosure.alg_closed R
   AlgEquiv.ofBijective _ (IsAlgClosure.algebraic.algHom_bijective₂

diff --git a/Mathlib/FieldTheory/IsSepClosed.lean b/Mathlib/FieldTheory/IsSepClosed.lean
@@ -267,7 +267,7 @@ variable [Algebra K L] [IsSepClosure K L]
 
 /-- A (random) isomorphism between two separable closures of `K`. -/
 noncomputable def equiv : L ≃ₐ[K] M :=
-  -- Porting note: added to replace local instance above
+  -- Porting note (#10754): added to replace local instance above
   haveI : IsSepClosed L := IsSepClosure.sep_closed K
   haveI : IsSepClosed M := IsSepClosure.sep_closed K
   AlgEquiv.ofBijective _ (Normal.isAlgebraic'.algHom_bijective₂

diff --git a/Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean b/Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@@ -99,8 +99,8 @@ noncomputable def stalk (X : LocallyRingedSpace) (x : X) : CommRingCat :=
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.LocallyRingedSpace.stalk AlgebraicGeometry.LocallyRingedSpace.stalk
 
--- Porting note: added this instance to help Lean realize stalks are local (so that `0 ≠ 1`
--- works below)
+-- Porting note (#10754): added this instance to help Lean realize stalks are local
+-- (so that `0 ≠ 1` works below)
 instance stalkLocal (x : X) : LocalRing <| X.stalk x := X.localRing x
 
 /-- A morphism of locally ringed spaces `f : X ⟶ Y` induces

diff --git a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean
@@ -425,7 +425,8 @@ theorem unifIntegrable_fin (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) {n : ℕ} {f
   revert f
   induction' n with n h
   · intro f hf
-    have : Subsingleton (Fin Nat.zero) := subsingleton_fin_zero -- Porting note: Added this instance
+  -- Porting note (#10754): added this instance
+    have : Subsingleton (Fin Nat.zero) := subsingleton_fin_zero
     exact unifIntegrable_subsingleton hp_one hp_top hf
   intro f hfLp ε hε
   let g : Fin n → α → β := fun k => f k

diff --git a/Mathlib/ModelTheory/DirectLimit.lean b/Mathlib/ModelTheory/DirectLimit.lean
@@ -166,7 +166,7 @@ def DirectLimit [DirectedSystem G fun i j h => f i j h] [IsDirected ι (· ≤
 
 attribute [local instance] DirectLimit.setoid
 
--- Porting note: Added local instance
+-- Porting note (#10754): Added local instance
 attribute [local instance] DirectLimit.sigmaStructure
 
 

diff --git a/Mathlib/Topology/Category/UniformSpace.lean b/Mathlib/Topology/Category/UniformSpace.lean
@@ -194,7 +194,7 @@ noncomputable def extensionHom {X : UniformSpaceCat} {Y : CpltSepUniformSpace}
   property := Completion.uniformContinuous_extension
 #align UniformSpace.extension_hom UniformSpaceCat.extensionHom
 
--- Porting note: added this instance to make things compile
+-- Porting note (#10754): added this instance to make things compile
 instance (X : UniformSpaceCat) : UniformSpace ((forget _).obj X) :=
   show UniformSpace X from inferInstance
 

diff --git a/Mathlib/Topology/Connected/PathConnected.lean b/Mathlib/Topology/Connected/PathConnected.lean
@@ -84,7 +84,7 @@ instance Path.funLike : FunLike (Path x y) I X where
     simp only [DFunLike.coe_fn_eq] at h
     cases γ₁; cases γ₂; congr
 
--- porting note: added this instance so that we can use `FunLike.coe` for `CoeFun`
+-- Porting note (#10754): added this instance so that we can use `FunLike.coe` for `CoeFun`
 -- this also fixed very strange `simp` timeout issues
 instance Path.continuousMapClass : ContinuousMapClass (Path x y) I X where
   map_continuous := fun γ => show Continuous γ.toContinuousMap by continuity

diff --git a/Mathlib/Topology/FiberBundle/Constructions.lean b/Mathlib/Topology/FiberBundle/Constructions.lean
@@ -41,7 +41,7 @@ namespace Trivial
 
 variable (B : Type*) (F : Type*)
 
--- Porting note: Added name for this instance.
+-- Porting note (#10754): Added name for this instance.
 -- TODO: use `TotalSpace.toProd`
 instance topologicalSpace [t₁ : TopologicalSpace B]
     [t₂ : TopologicalSpace F] : TopologicalSpace (TotalSpace F (Trivial B F)) :=