[Merged by Bors] - chore: classify lemma was not necessary porting notes (category theory)

Mathlib/Algebra/Category/GroupCat/Preadditive.lean

@@ -22,7 +22,7 @@ namespace AddCommGroupCat
 instance (P Q : AddCommGroupCat) : AddCommGroup (P ⟶ Q) :=
   (inferInstance : AddCommGroup (AddMonoidHom P Q))
 
--- porting note: this lemma was not necessary in mathlib
+-- porting note (#10688): this lemma was not necessary in mathlib
 @[simp]
 lemma hom_add_apply {P Q : AddCommGroupCat} (f g : P ⟶ Q) (x : P) : (f + g) x = f x + g x := rfl
 

Mathlib/CategoryTheory/Types.lean

@@ -52,7 +52,7 @@ theorem types_hom {α β : Type u} : (α ⟶ β) = (α → β) :=
   rfl
 #align category_theory.types_hom CategoryTheory.types_hom
 
--- porting note: this lemma was not here in Lean 3. Lean 3 `ext` would solve this goal
+-- porting note (#10688): this lemma was not here in Lean 3. Lean 3 `ext` would solve this goal
 -- because of its "if all else fails, apply all `ext` lemmas" policy,
 -- which apparently we want to move away from.
 @[ext] theorem types_ext {α β : Type u} (f g : α ⟶ β) (h : ∀ a : α, f a = g a) : f = g := by

Mathlib/Topology/Category/Profinite/Basic.lean

@@ -79,7 +79,7 @@ instance hasForget₂ : HasForget₂ Profinite TopCat :=
 instance : CoeSort Profinite (Type*) :=
   ⟨fun X => X.toCompHaus⟩
 
--- Porting note: This lemma was not needed in mathlib3
+-- Porting note (#10688): This lemma was not needed in mathlib3
 @[simp]
 lemma forget_ContinuousMap_mk {X Y : Profinite} (f : X → Y) (hf : Continuous f) :
     (forget Profinite).map (ContinuousMap.mk f hf) = f :=