leanprover-community · pitmonticone · Feb 18, 2024 · Feb 18, 2024 · Feb 21, 2024 · Feb 21, 2024
diff --git a/Mathlib/Algebra/PUnitInstances.lean b/Mathlib/Algebra/PUnitInstances.lean
@@ -97,12 +97,12 @@ instance normalizedGCDMonoid : NormalizedGCDMonoid PUnit where
   normalize_gcd := by intros; rfl
   normalize_lcm := by intros; rfl
 
--- Porting notes (#10618): simpNF lint: simp can prove this @[simp]
+-- Porting note (#10618): simpNF lint: simp can prove this @[simp]
 theorem gcd_eq : gcd x y = unit :=
   rfl
 #align punit.gcd_eq PUnit.gcd_eq
 
--- Porting notes (#10618): simpNF lint: simp can prove this @[simp]
+-- Porting note (#10618): simpNF lint: simp can prove this @[simp]
 theorem lcm_eq : lcm x y = unit :=
   rfl
 #align punit.lcm_eq PUnit.lcm_eq

diff --git a/Mathlib/AlgebraicGeometry/Scheme.lean b/Mathlib/AlgebraicGeometry/Scheme.lean
@@ -59,7 +59,7 @@ def Hom (X Y : Scheme) : Type* :=
 instance : Category Scheme :=
   { InducedCategory.category Scheme.toLocallyRingedSpace with Hom := Hom }
 
--- porting note: added to ease automation
+-- porting note (#10688): added to ease automation
 @[continuity]
 lemma Hom.continuous {X Y : Scheme} (f : X ⟶ Y) : Continuous f.1.base := f.1.base.2
 

diff --git a/Mathlib/AlgebraicTopology/SimplicialObject.lean b/Mathlib/AlgebraicTopology/SimplicialObject.lean
@@ -76,7 +76,7 @@ instance [HasColimits C] : HasColimits (SimplicialObject C) :=
 
 variable {C}
 
--- porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[ext]
 lemma hom_ext {X Y : SimplicialObject C} (f g : X ⟶ Y)
     (h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n) : f = g :=
@@ -300,7 +300,7 @@ variable {C}
 
 namespace Augmented
 
--- porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[ext]
 lemma hom_ext {X Y : Augmented C} (f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
     f = g :=
@@ -446,7 +446,7 @@ instance [HasColimits C] : HasColimits (CosimplicialObject C) :=
 
 variable {C}
 
--- porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[ext]
 lemma hom_ext {X Y : CosimplicialObject C} (f g : X ⟶ Y)
     (h : ∀ (n : SimplexCategory), f.app n = g.app n) : f = g :=
@@ -672,7 +672,7 @@ variable {C}
 
 namespace Augmented
 
--- porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[ext]
 lemma hom_ext {X Y : Augmented C} (f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) :
     f = g :=

diff --git a/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean b/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean
@@ -67,7 +67,7 @@ instance toAddMonoidHomClass {V W : SemiNormedGroupCat} : AddMonoidHomClass (V
   map_add f := f.map_add'
   map_zero f := (AddMonoidHom.mk' f.toFun f.map_add').map_zero
 
--- Porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[ext]
 lemma ext {M N : SemiNormedGroupCat} {f₁ f₂ : M ⟶ N} (h : ∀ (x : M), f₁ x = f₂ x) : f₁ = f₂ :=
   DFunLike.ext _ _ h

diff --git a/Mathlib/CategoryTheory/Comma/Arrow.lean b/Mathlib/CategoryTheory/Comma/Arrow.lean
@@ -64,12 +64,12 @@ theorem id_right (f : Arrow T) : CommaMorphism.right (𝟙 f) = 𝟙 f.right :=
   rfl
 #align category_theory.arrow.id_right CategoryTheory.Arrow.id_right
 
--- porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[simp, reassoc]
 theorem comp_left {X Y Z : Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) :
     (f ≫ g).left = f.left ≫ g.left := rfl
 
--- porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[simp, reassoc]
 theorem comp_right {X Y Z : Arrow T} (f : X ⟶ Y) (g : Y ⟶ Z) :
     (f ≫ g).right = f.right ≫ g.right := rfl

diff --git a/Mathlib/CategoryTheory/FintypeCat.lean b/Mathlib/CategoryTheory/FintypeCat.lean
@@ -92,7 +92,7 @@ lemma hom_inv_id_apply {X Y : FintypeCat} (f : X ≅ Y) (x : X) : f.inv (f.hom x
 lemma inv_hom_id_apply {X Y : FintypeCat} (f : X ≅ Y) (y : Y) : f.hom (f.inv y) = y :=
   congr_fun f.inv_hom_id y
 
--- porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[ext]
 lemma hom_ext {X Y : FintypeCat} (f g : X ⟶ Y) (h : ∀ x, f x = g x) : f = g := by
   funext

diff --git a/Mathlib/CategoryTheory/GradedObject.lean b/Mathlib/CategoryTheory/GradedObject.lean
@@ -70,7 +70,7 @@ instance categoryOfGradedObjects (β : Type w) : Category.{max w v} (GradedObjec
   CategoryTheory.pi fun _ => C
 #align category_theory.graded_object.category_of_graded_objects CategoryTheory.GradedObject.categoryOfGradedObjects
 
--- porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[ext]
 lemma hom_ext {X Y : GradedObject β C} (f g : X ⟶ Y) (h : ∀ x, f x = g x) : f = g := by
   funext

diff --git a/Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean b/Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean
@@ -28,7 +28,7 @@ namespace KaroubiKaroubi
 
 variable (C : Type*) [Category C]
 
--- porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[reassoc (attr := simp)]
 lemma idem_f (P : Karoubi (Karoubi C)) : P.p.f ≫ P.p.f = P.p.f := by
   simpa only [hom_ext_iff, comp_f] using P.idem

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
@@ -203,7 +203,7 @@ abbrev Sigma.ι (f : β → C) [HasCoproduct f] (b : β) : f b ⟶ ∐ f :=
   colimit.ι (Discrete.functor f) (Discrete.mk b)
 #align category_theory.limits.sigma.ι CategoryTheory.Limits.Sigma.ι
 
--- porting note: added the next two lemmas to ease automation; without these lemmas,
+-- porting note (#10688): added the next two lemmas to ease automation; without these lemmas,
 -- `limit.hom_ext` would be applied, but the goal would involve terms
 -- in `Discrete β` rather than `β` itself
 @[ext 1050]

diff --git a/Mathlib/CategoryTheory/Monad/Basic.lean b/Mathlib/CategoryTheory/Monad/Basic.lean
@@ -203,12 +203,12 @@ instance : Quiver (Monad C) where
 instance : Quiver (Comonad C) where
   Hom := ComonadHom
 
--- porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[ext]
 lemma MonadHom.ext' {T₁ T₂ : Monad C} (f g : T₁ ⟶ T₂) (h : f.app = g.app) : f = g :=
   MonadHom.ext f g h
 
--- porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[ext]
 lemma ComonadHom.ext' {T₁ T₂ : Comonad C} (f g : T₁ ⟶ T₂) (h : f.app = g.app) : f = g :=
   ComonadHom.ext f g h

diff --git a/Mathlib/CategoryTheory/Monoidal/CommMon_.lean b/Mathlib/CategoryTheory/Monoidal/CommMon_.lean
@@ -67,7 +67,8 @@ set_option linter.uppercaseLean3 false in
 lemma hom_ext {A B : CommMon_ C} (f g : A ⟶ B) (h : f.hom = g.hom) : f = g :=
   Mon_.Hom.ext _ _ h
 
--- porting note: the following two lemmas `id'` and `comp'` have been added to ease automation;
+-- Porting note (#10688): the following two lemmas `id'` and `comp'`
+-- have been added to ease automation;
 @[simp]
 lemma id' (A : CommMon_ C) : (𝟙 A : A.toMon_ ⟶ A.toMon_) = 𝟙 (A.toMon_) := rfl
 
@@ -144,7 +145,7 @@ set_option linter.uppercaseLean3 false in
 
 variable (C) (D)
 
--- porting note: added @[simps] to ease automation
+-- Porting note (#10688): added @[simps] to ease automation
 /-- `mapCommMon` is functorial in the lax braided functor. -/
 @[simps]
 def mapCommMonFunctor : LaxBraidedFunctor C D ⥤ CommMon_ C ⥤ CommMon_ D where

diff --git a/Mathlib/CategoryTheory/Preadditive/Mat.lean b/Mathlib/CategoryTheory/Preadditive/Mat.lean
@@ -666,7 +666,7 @@ instance (X Y : Mat R) : AddCommGroup (X ⟶ Y) := by
 
 variable {R}
 
--- porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[simp]
 theorem add_apply {M N : Mat R} (f g : M ⟶ N) (i j) : (f + g) i j = f i j + g i j :=
   rfl

diff --git a/Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean b/Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
@@ -55,7 +55,7 @@ def FirstObj : Type max v u :=
 
 variable {P R}
 
--- porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[ext]
 lemma FirstObj.ext (z₁ z₂ : FirstObj P R) (h : ∀ (Y : C) (f : Y ⟶ X)
     (hf : R f), (Pi.π _ ⟨Y, f, hf⟩ : FirstObj P R ⟶ _) z₁ =
@@ -105,7 +105,7 @@ def SecondObj : Type max v u :=
 
 variable {P S}
 
--- porting note: added to ease automation
+-- Porting note (#10688): added to ease automation
 @[ext]
 lemma SecondObj.ext (z₁ z₂ : SecondObj P S) (h : ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X)
     (hf : S.arrows f), (Pi.π _ ⟨Y, Z, g, f, hf⟩ : SecondObj P S ⟶ _) z₁ =

diff --git a/Mathlib/Data/List/Defs.lean b/Mathlib/Data/List/Defs.lean
@@ -21,7 +21,7 @@ proofs about these definitions, those are contained in other files in `Data.List
 
 set_option autoImplicit true
 
--- Porting notes
+-- Porting note
 -- Many of the definitions in `Data.List.Defs` were already defined upstream in `Std4`
 -- These have been annotated with `#align`s
 -- To make this easier for review, the `#align`s have been placed in order of occurrence
@@ -500,7 +500,7 @@ def map₂Right (f : Option α → β → γ) (as : List α) (bs : List β) : Li
 #align list.to_chunks_aux List.toChunksAux
 #align list.to_chunks List.toChunks
 
--- porting notes -- was `unsafe` but removed for Lean 4 port
+-- porting note -- was `unsafe` but removed for Lean 4 port
 -- TODO: naming is awkward...
 /-- Asynchronous version of `List.map`.
 -/

diff --git a/Mathlib/RepresentationTheory/Action/Limits.lean b/Mathlib/RepresentationTheory/Action/Limits.lean
@@ -205,7 +205,7 @@ section HasZeroMorphisms
 
 variable [HasZeroMorphisms V]
 
--- porting note: in order to ease automation, the `Zero` instance is introduced separately,
+-- porting note (#10688): in order to ease automation, the `Zero` instance is introduced separately,
 -- and the lemma `zero_hom` was moved just below
 instance {X Y : Action V G} : Zero (X ⟶ Y) := ⟨0, by aesop_cat⟩
 

diff --git a/Mathlib/SetTheory/Lists.lean b/Mathlib/SetTheory/Lists.lean
@@ -83,7 +83,7 @@ def toList : ∀ {b}, Lists' α b → List (Lists α)
   | _, cons' a l => ⟨_, a⟩ :: l.toList
 #align lists'.to_list Lists'.toList
 
--- Porting notes (#10618): removed @[simp]
+-- Porting note (#10618): removed @[simp]
 -- simp can prove this: by simp only [@Lists'.toList, @Sigma.eta]
 theorem toList_cons (a : Lists α) (l) : toList (cons a l) = a :: l.toList := by simp
 #align lists'.to_list_cons Lists'.toList_cons