chore: change 'Porting:' to 'Porting note:' (#6378)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Algebra/Category/GroupCat/EpiMono.lean

@@ -120,7 +120,7 @@ instance : SMul B X' where
     match x with
     | fromCoset y => fromCoset ⟨b *l y, by
           rw [← y.2.choose_spec, leftCoset_assoc]
-          -- Porting: should we make `Bundled.α` reducible?
+          -- Porting note: should we make `Bundled.α` reducible?
           let b' : B := y.2.choose
           use b * b'⟩
     | ∞ => ∞

Mathlib/CategoryTheory/Limits/Shapes/ZeroObjects.lean

@@ -51,7 +51,7 @@ namespace IsZero
 
 variable {X Y : C}
 
--- Porting: `to` is a reserved word, it was replaced by `to_`
+-- Porting note: `to` is a reserved word, it was replaced by `to_`
 /-- If `h : IsZero X`, then `h.to_ Y` is a choice of unique morphism `X → Y`. -/
 protected def to_ (h : IsZero X) (Y : C) : X ⟶ Y :=
   @default _ <| (h.unique_to Y).some.toInhabited
@@ -65,7 +65,7 @@ theorem to_eq (h : IsZero X) (f : X ⟶ Y) : h.to_ Y = f :=
   (h.eq_to f).symm
 #align category_theory.limits.is_zero.to_eq CategoryTheory.Limits.IsZero.to_eq
 
--- Porting: `from` is a reserved word, it was replaced by `from_`
+-- Porting note: `from` is a reserved word, it was replaced by `from_`
 /-- If `h : is_zero X`, then `h.from_ Y` is a choice of unique morphism `Y → X`. -/
 protected def from_ (h : IsZero X) (Y : C) : Y ⟶ X :=
   @default _ <| (h.unique_from Y).some.toInhabited

Mathlib/Data/Set/Basic.lean

@@ -179,12 +179,12 @@ theorem Set.coe_setOf (p : α → Prop) : ↥{ x | p x } = { x // p x } :=
   rfl
 #align set.coe_set_of Set.coe_setOf
 
--- Porting: removed `simp` because `simp` can prove it
+-- Porting note: removed `simp` because `simp` can prove it
 theorem SetCoe.forall {s : Set α} {p : s → Prop} : (∀ x : s, p x) ↔ ∀ (x) (h : x ∈ s), p ⟨x, h⟩ :=
   Subtype.forall
 #align set_coe.forall SetCoe.forall
 
--- Porting: removed `simp` because `simp` can prove it
+-- Porting note: removed `simp` because `simp` can prove it
 theorem SetCoe.exists {s : Set α} {p : s → Prop} :
     (∃ x : s, p x) ↔ ∃ (x : _) (h : x ∈ s), p ⟨x, h⟩ :=
   Subtype.exists
@@ -423,7 +423,7 @@ theorem not_mem_empty (x : α) : ¬x ∈ (∅ : Set α) :=
   id
 #align set.not_mem_empty Set.not_mem_empty
 
--- Porting: removed `simp` because `simp` can prove it
+-- Porting note: removed `simp` because `simp` can prove it
 theorem not_not_mem : ¬a ∉ s ↔ a ∈ s :=
   not_not
 #align set.not_not_mem Set.not_not_mem