chore: classify porting notes about ext (#17809)

I checked all porting notes mentioning `ext` and either fixed them (see #17810), or classified them as
 * #5229 if it's a new `@[ext]` lemma
 * #11041 if it's a regression in `ext`
 * #11182 if `@[ext]` had to be removed

This PR should contain only modifications to comments.

Author: Vierkantor

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -369,7 +369,7 @@ def embeddingLiftIso (F : C ⥤ D) : embedding R C ⋙ lift R F ≅ F :=
 /-- Two `R`-linear functors out of the `R`-linear completion are isomorphic iff their
 compositions with the embedding functor are isomorphic.
 -/
--- Porting note: used to be @[ext]
+-- Porting note (#11182): used to be @[ext]
 def ext {F G : Free R C ⥤ D} [F.Additive] [F.Linear R] [G.Additive] [G.Linear R]
     (α : embedding R C ⋙ F ≅ embedding R C ⋙ G) : F ≅ G :=
   NatIso.ofComponents (fun X => α.app X)

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -244,7 +244,7 @@ instance : Category (HomologicalComplex V c) where
 
 end
 
--- Porting note: added because `Hom.ext` is not triggered automatically
+-- Porting note (#5229): added because `Hom.ext` is not triggered automatically
 @[ext]
 lemma hom_ext {C D : HomologicalComplex V c} (f g : C ⟶ D)
     (h : ∀ i, f.f i = g.f i) : f = g := by

Mathlib/Algebra/Lie/DirectSum.lean

@@ -43,13 +43,13 @@ variable [∀ i, LieRingModule L (M i)] [∀ i, LieModule R L (M i)]
 instance : LieRingModule L (⨁ i, M i) where
   bracket x m := m.mapRange (fun _ m' => ⁅x, m'⁆) fun _ => lie_zero x
   add_lie x y m := by
-    refine DFinsupp.ext fun _ => ?_ -- Porting note: Originally `ext`
+    refine DFinsupp.ext fun _ => ?_ -- Porting note (#11041): Originally `ext`
     simp only [mapRange_apply, add_apply, add_lie]
   lie_add x m n := by
-    refine DFinsupp.ext fun _ => ?_ -- Porting note: Originally `ext`
+    refine DFinsupp.ext fun _ => ?_ -- Porting note (#11041): Originally `ext`
     simp only [mapRange_apply, add_apply, lie_add]
   leibniz_lie x y m := by
-    refine DFinsupp.ext fun _ => ?_ -- Porting note: Originally `ext`
+    refine DFinsupp.ext fun _ => ?_ -- Porting note (#11041): Originally `ext`
     simp only [mapRange_apply, lie_lie, add_apply, sub_add_cancel]
 
 @[simp]
@@ -58,10 +58,10 @@ theorem lie_module_bracket_apply (x : L) (m : ⨁ i, M i) (i : ι) : ⁅x, m⁆
 
 instance : LieModule R L (⨁ i, M i) where
   smul_lie t x m := by
-    refine DFinsupp.ext fun _ => ?_ -- Porting note: Originally `ext i`
+    refine DFinsupp.ext fun _ => ?_ -- Porting note (#11041): Originally `ext i`
     simp only [smul_lie, lie_module_bracket_apply, smul_apply]
   lie_smul t x m := by
-    refine DFinsupp.ext fun _ => ?_ -- Porting note: Originally `ext i`
+    refine DFinsupp.ext fun _ => ?_ -- Porting note (#11041): Originally `ext i`
     simp only [lie_smul, lie_module_bracket_apply, smul_apply]
 
 variable (R ι L M)
@@ -70,7 +70,7 @@ variable (R ι L M)
 def lieModuleOf [DecidableEq ι] (j : ι) : M j →ₗ⁅R,L⁆ ⨁ i, M i :=
   { lof R ι M j with
     map_lie' := fun {x m} => by
-      refine DFinsupp.ext fun i => ?_ -- Porting note: Originally `ext i`
+      refine DFinsupp.ext fun i => ?_ -- Porting note (#11041): Originally `ext i`
       by_cases h : j = i
       · rw [← h]; simp
       · -- This used to be the end of the proof before leanprover/lean4#2644
@@ -98,16 +98,16 @@ instance lieRing : LieRing (⨁ i, L i) :=
   { (inferInstance : AddCommGroup _) with
     bracket := zipWith (fun _ => fun x y => ⁅x, y⁆) fun _ => lie_zero 0
     add_lie := fun x y z => by
-      refine DFinsupp.ext fun _ => ?_ -- Porting note: Originally `ext`
+      refine DFinsupp.ext fun _ => ?_ -- Porting note (#11041): Originally `ext`
       simp only [zipWith_apply, add_apply, add_lie]
     lie_add := fun x y z => by
-      refine DFinsupp.ext fun _ => ?_ -- Porting note: Originally `ext`
+      refine DFinsupp.ext fun _ => ?_ -- Porting note (#11041): Originally `ext`
       simp only [zipWith_apply, add_apply, lie_add]
     lie_self := fun x => by
-      refine DFinsupp.ext fun _ => ?_ -- Porting note: Originally `ext`
+      refine DFinsupp.ext fun _ => ?_ -- Porting note (#11041): Originally `ext`
       simp only [zipWith_apply, add_apply, lie_self, zero_apply]
     leibniz_lie := fun x y z => by
-      refine DFinsupp.ext fun _ => ?_ -- Porting note: Originally `ext`
+      refine DFinsupp.ext fun _ => ?_ -- Porting note (#11041): Originally `ext`
       simp only [sub_apply, zipWith_apply, add_apply, zero_apply]
       apply leibniz_lie }
 
@@ -137,7 +137,7 @@ theorem lie_of [DecidableEq ι] {i j : ι} (x : L i) (y : L j) :
 instance lieAlgebra : LieAlgebra R (⨁ i, L i) :=
   { (inferInstance : Module R _) with
     lie_smul := fun c x y => by
-      refine DFinsupp.ext fun _ => ?_ -- Porting note: Originally `ext`
+      refine DFinsupp.ext fun _ => ?_ -- Porting note (#11041): Originally `ext`
       simp only [zipWith_apply, smul_apply, bracket_apply, lie_smul] }
 
 variable (R ι)
@@ -148,7 +148,7 @@ def lieAlgebraOf [DecidableEq ι] (j : ι) : L j →ₗ⁅R⁆ ⨁ i, L i :=
   { lof R ι L j with
     toFun := of L j
     map_lie' := fun {x y} => by
-      refine DFinsupp.ext fun i => ?_ -- Porting note: Originally `ext i`
+      refine DFinsupp.ext fun i => ?_ -- Porting note (#11041): Originally `ext i`
       by_cases h : j = i
       · rw [← h]
         -- This used to be the end of the proof before leanprover/lean4#2644

Mathlib/Algebra/MonoidAlgebra/Basic.lean

@@ -90,7 +90,7 @@ def liftMagma [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] :
       sum_single_index, Function.comp_apply, one_smul, zero_smul, MulHom.coe_comp,
       NonUnitalAlgHom.coe_to_mulHom]
   right_inv F := by
-    -- Porting note: `ext` → `refine nonUnitalAlgHom_ext' k (MulHom.ext fun m => ?_)`
+    -- Porting note (#11041): `ext` → `refine nonUnitalAlgHom_ext' k (MulHom.ext fun m => ?_)`
     refine nonUnitalAlgHom_ext' k (MulHom.ext fun m => ?_)
     simp only [NonUnitalAlgHom.coe_mk, ofMagma_apply, NonUnitalAlgHom.toMulHom_eq_coe,
       sum_single_index, Function.comp_apply, one_smul, zero_smul, MulHom.coe_comp,
@@ -109,7 +109,7 @@ In particular this provides the instance `Algebra k (MonoidAlgebra k G)`.
 instance algebra {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] :
     Algebra k (MonoidAlgebra A G) :=
   { singleOneRingHom.comp (algebraMap k A) with
-    -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
+    -- Porting note (#11041): `ext` → `refine Finsupp.ext fun _ => ?_`
     smul_def' := fun r a => by
       refine Finsupp.ext fun _ => ?_
       -- Porting note: Newly required.
@@ -125,7 +125,7 @@ def singleOneAlgHom {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Mon
     A →ₐ[k] MonoidAlgebra A G :=
   { singleOneRingHom with
     commutes' := fun r => by
-      -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
+      -- Porting note (#11041): `ext` → `refine Finsupp.ext fun _ => ?_`
       refine Finsupp.ext fun _ => ?_
       simp
       rfl }
@@ -390,7 +390,7 @@ In particular this provides the instance `Algebra k k[G]`.
 instance algebra [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] :
     Algebra R k[G] :=
   { singleZeroRingHom.comp (algebraMap R k) with
-    -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
+    -- Porting note (#11041): `ext` → `refine Finsupp.ext fun _ => ?_`
     smul_def' := fun r a => by
       refine Finsupp.ext fun _ => ?_
       -- Porting note: Newly required.
@@ -405,7 +405,7 @@ instance algebra [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] :
 def singleZeroAlgHom [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : k →ₐ[R] k[G] :=
   { singleZeroRingHom with
     commutes' := fun r => by
-      -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
+      -- Porting note (#11041): `ext` → `refine Finsupp.ext fun _ => ?_`
       refine Finsupp.ext fun _ => ?_
       simp
       rfl }

Mathlib/Algebra/MonoidAlgebra/Defs.lean

@@ -563,7 +563,7 @@ theorem liftNC_smul [MulOneClass G] {R : Type*} [Semiring R] (f : k →+* R) (g
   suffices (liftNC (↑f) g).comp (smulAddHom k (MonoidAlgebra k G) c) =
       (AddMonoidHom.mulLeft (f c)).comp (liftNC (↑f) g) from
     DFunLike.congr_fun this φ
-  -- Porting note: `ext` couldn't a find appropriate theorem.
+  -- Porting note (#11041): `ext` couldn't a find appropriate theorem.
   refine addHom_ext' fun a => AddMonoidHom.ext fun b => ?_
   -- Porting note: `reducible` cannot be `local` so the proof gets more complex.
   unfold MonoidAlgebra
@@ -584,7 +584,7 @@ variable (k) [Semiring k] [DistribSMul R k] [Mul G]
 instance isScalarTower_self [IsScalarTower R k k] :
     IsScalarTower R (MonoidAlgebra k G) (MonoidAlgebra k G) :=
   ⟨fun t a b => by
-    -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
+    -- Porting note (#11041): `ext` → `refine Finsupp.ext fun _ => ?_`
     refine Finsupp.ext fun m => ?_
     -- Porting note: `refine` & `rw` are required because `simp` behaves differently.
     classical
@@ -600,7 +600,7 @@ also commute with the algebra multiplication. -/
 instance smulCommClass_self [SMulCommClass R k k] :
     SMulCommClass R (MonoidAlgebra k G) (MonoidAlgebra k G) :=
   ⟨fun t a b => by
-    -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
+    -- Porting note (#11041): `ext` → `refine Finsupp.ext fun _ => ?_`
     refine Finsupp.ext fun m => ?_
     -- Porting note: `refine` & `rw` are required because `simp` behaves differently.
     classical
@@ -742,7 +742,7 @@ protected noncomputable def opRingEquiv [Monoid G] :
       rw [← AddEquiv.coe_toAddMonoidHom]
       refine Iff.mpr (AddMonoidHom.map_mul_iff (R := (MonoidAlgebra k G)ᵐᵒᵖ)
         (S := MonoidAlgebra kᵐᵒᵖ Gᵐᵒᵖ) _) ?_
-      -- Porting note: Was `ext`.
+      -- Porting note (#11041): Was `ext`.
       refine AddMonoidHom.mul_op_ext _ _ <| addHom_ext' fun i₁ => AddMonoidHom.ext fun r₁ =>
         AddMonoidHom.mul_op_ext _ _ <| addHom_ext' fun i₂ => AddMonoidHom.ext fun r₂ => ?_
       -- Porting note: `reducible` cannot be `local` so proof gets long.
@@ -924,7 +924,7 @@ instance nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring k[G] :=
       simp only [mul_def]
       exact Eq.trans (congr_arg (sum f) (funext₂ fun a₁ b₁ => sum_zero_index)) sum_zero
     nsmul := fun n f => n • f
-    -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
+    -- Porting note (#11041): `ext` → `refine Finsupp.ext fun _ => ?_`
     nsmul_zero := by
       intros
       refine Finsupp.ext fun _ => ?_
@@ -1399,7 +1399,7 @@ protected noncomputable def opRingEquiv [AddCommMonoid G] :
       rw [Equiv.toFun_as_coe, AddEquiv.toEquiv_eq_coe]; erw [AddEquiv.coe_toEquiv]
       rw [← AddEquiv.coe_toAddMonoidHom]
       refine Iff.mpr (AddMonoidHom.map_mul_iff (R := k[G]ᵐᵒᵖ) (S := kᵐᵒᵖ[G]) _) ?_
-      -- Porting note: Was `ext`.
+      -- Porting note (#11041): Was `ext`.
       refine AddMonoidHom.mul_op_ext _ _ <| addHom_ext' fun i₁ => AddMonoidHom.ext fun r₁ =>
         AddMonoidHom.mul_op_ext _ _ <| addHom_ext' fun i₂ => AddMonoidHom.ext fun r₂ => ?_
       -- Porting note: `reducible` cannot be `local` so proof gets long.

Mathlib/Algebra/MonoidAlgebra/Division.lean

@@ -69,14 +69,14 @@ theorem zero_divOf (g : G) : (0 : k[G]) /ᵒᶠ g = 0 :=
 
 @[simp]
 theorem divOf_zero (x : k[G]) : x /ᵒᶠ 0 = x := by
-  refine Finsupp.ext fun _ => ?_  -- Porting note: `ext` doesn't work
+  refine Finsupp.ext fun _ => ?_  -- Porting note (#11041): `ext` doesn't work
   simp only [AddMonoidAlgebra.divOf_apply, zero_add]
 
 theorem add_divOf (x y : k[G]) (g : G) : (x + y) /ᵒᶠ g = x /ᵒᶠ g + y /ᵒᶠ g :=
   map_add (Finsupp.comapDomain.addMonoidHom _) _ _
 
 theorem divOf_add (x : k[G]) (a b : G) : x /ᵒᶠ (a + b) = x /ᵒᶠ a /ᵒᶠ b := by
-  refine Finsupp.ext fun _ => ?_  -- Porting note: `ext` doesn't work
+  refine Finsupp.ext fun _ => ?_  -- Porting note (#11041): `ext` doesn't work
   simp only [AddMonoidAlgebra.divOf_apply, add_assoc]
 
 /-- A bundled version of `AddMonoidAlgebra.divOf`. -/
@@ -93,13 +93,13 @@ noncomputable def divOfHom : Multiplicative G →* AddMonoid.End k[G] where
         (divOf_add _ _ _)
 
 theorem of'_mul_divOf (a : G) (x : k[G]) : of' k G a * x /ᵒᶠ a = x := by
-  refine Finsupp.ext fun _ => ?_  -- Porting note: `ext` doesn't work
+  refine Finsupp.ext fun _ => ?_  -- Porting note (#11041): `ext` doesn't work
   rw [AddMonoidAlgebra.divOf_apply, of'_apply, single_mul_apply_aux, one_mul]
   intro c
   exact add_right_inj _
 
 theorem mul_of'_divOf (x : k[G]) (a : G) : x * of' k G a /ᵒᶠ a = x := by
-  refine Finsupp.ext fun _ => ?_  -- Porting note: `ext` doesn't work
+  refine Finsupp.ext fun _ => ?_  -- Porting note (#11041): `ext` doesn't work
   rw [AddMonoidAlgebra.divOf_apply, of'_apply, mul_single_apply_aux, mul_one]
   intro c
   rw [add_comm]
@@ -134,14 +134,14 @@ theorem modOf_apply_self_add (x : k[G]) (g : G) (d : G) : (x %ᵒᶠ g) (g + d)
   modOf_apply_of_exists_add _ _ _ ⟨_, rfl⟩
 
 theorem of'_mul_modOf (g : G) (x : k[G]) : of' k G g * x %ᵒᶠ g = 0 := by
-  refine Finsupp.ext fun g' => ?_  -- Porting note: `ext g'` doesn't work
+  refine Finsupp.ext fun g' => ?_  -- Porting note (#11041): `ext g'` doesn't work
   rw [Finsupp.zero_apply]
   obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
   · rw [modOf_apply_self_add]
   · rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h]
 
 theorem mul_of'_modOf (x : k[G]) (g : G) : x * of' k G g %ᵒᶠ g = 0 := by
-  refine Finsupp.ext fun g' => ?_  -- Porting note: `ext g'` doesn't work
+  refine Finsupp.ext fun g' => ?_  -- Porting note (#11041): `ext g'` doesn't work
   rw [Finsupp.zero_apply]
   obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
   · rw [modOf_apply_self_add]
@@ -153,7 +153,7 @@ theorem of'_modOf (g : G) : of' k G g %ᵒᶠ g = 0 := by
 
 theorem divOf_add_modOf (x : k[G]) (g : G) :
     of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x := by
-  refine Finsupp.ext fun g' => ?_  -- Porting note: `ext` doesn't work
+  refine Finsupp.ext fun g' => ?_  -- Porting note (#11041): `ext` doesn't work
   rw [Finsupp.add_apply] -- Porting note: changed from `simp_rw` which can't see through the type
   obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
   swap

Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean

@@ -129,7 +129,7 @@ theorem toDirectSum_mul [DecidableEq ι] [AddMonoid ι] [Semiring M] (f g : AddM
   let _ : NonUnitalNonAssocSemiring (ι →₀ M) := AddMonoidAlgebra.nonUnitalNonAssocSemiring
   revert f g
   rw [AddMonoidHom.map_mul_iff]
-  -- Porting note: does not find `addHom_ext'`, was `ext (xi xv yi yv) : 4`
+  -- Porting note (#11041): does not find `addHom_ext'`, was `ext (xi xv yi yv) : 4`
   refine Finsupp.addHom_ext' fun xi => AddMonoidHom.ext fun xv => ?_
   refine Finsupp.addHom_ext' fun yi => AddMonoidHom.ext fun yv => ?_
   dsimp only [AddMonoidHom.comp_apply, AddMonoidHom.compl₂_apply, AddMonoidHom.compr₂_apply,

Mathlib/Algebra/MvPolynomial/Basic.lean

@@ -404,12 +404,12 @@ theorem induction_on {M : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (h
 theorem ringHom_ext {A : Type*} [Semiring A] {f g : MvPolynomial σ R →+* A}
     (hC : ∀ r, f (C r) = g (C r)) (hX : ∀ i, f (X i) = g (X i)) : f = g := by
   refine AddMonoidAlgebra.ringHom_ext' ?_ ?_
-  -- Porting note: this has high priority, but Lean still chooses `RingHom.ext`, why?
+  -- Porting note (#11041): this has high priority, but Lean still chooses `RingHom.ext`, why?
   -- probably because of the type synonym
   · ext x
     exact hC _
   · apply Finsupp.mulHom_ext'; intros x
-    -- Porting note: `Finsupp.mulHom_ext'` needs to have increased priority
+    -- Porting note (#11041): `Finsupp.mulHom_ext'` needs to have increased priority
     apply MonoidHom.ext_mnat
     exact hX _
 

Mathlib/Algebra/Polynomial/Laurent.lean

@@ -87,7 +87,7 @@ scoped[LaurentPolynomial] notation:9000 R "[T;T⁻¹]" => LaurentPolynomial R
 
 open LaurentPolynomial
 
--- Porting note: `ext` no longer applies `Finsupp.ext` automatically
+-- Porting note (#5229): `ext` no longer applies `Finsupp.ext` automatically
 @[ext]
 theorem LaurentPolynomial.ext [Semiring R] {p q : R[T;T⁻¹]} (h : ∀ a, p a = q a) : p = q :=
   Finsupp.ext h

Mathlib/AlgebraicGeometry/Restrict.lean

@@ -392,13 +392,13 @@ theorem image_morphismRestrict_preimage {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.
     -- Porting note: this rewrite was not necessary
     rw [SetLike.mem_coe]
     convert hx'
-    -- Porting note: `ext1` is not compiling
+    -- Porting note (#11041): `ext1` is not compiling
     refine Subtype.ext ?_
     exact (morphismRestrict_base_coe f U ⟨x, hx⟩).symm
   · rintro ⟨⟨x, hx⟩, hx' : _ ∈ V.1, rfl : x = _⟩
     refine ⟨⟨_, hx⟩, (?_ : (f ∣_ U).base ⟨x, hx⟩ ∈ V.1), rfl⟩
     convert hx'
-    -- Porting note: `ext1` is compiling
+    -- Porting note (#11041): `ext1` is compiling
     refine Subtype.ext ?_
     exact morphismRestrict_base_coe f U ⟨x, hx⟩
 

Mathlib/AlgebraicGeometry/Spec.lean

@@ -287,7 +287,7 @@ instance isIso_toSpecΓ (R : CommRingCat.{u}) : IsIso (toSpecΓ R) := by
 @[reassoc]
 theorem Spec_Γ_naturality {R S : CommRingCat.{u}} (f : R ⟶ S) :
     f ≫ toSpecΓ S = toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op := by
-  -- Porting note: `ext` failed to pick up one of the three lemmas
+  -- Porting note (#11041): `ext` failed to pick up one of the three lemmas
   refine RingHom.ext fun x => Subtype.ext <| funext fun x' => ?_; symm
   apply Localization.localRingHom_to_map
 

Mathlib/AlgebraicTopology/SimplexCategory.lean

@@ -142,7 +142,7 @@ lemma id_toOrderHom (a : SimplexCategory) :
 lemma comp_toOrderHom {a b c : SimplexCategory} (f : a ⟶ b) (g : b ⟶ c) :
     (f ≫ g).toOrderHom = g.toOrderHom.comp f.toOrderHom := rfl
 
--- Porting note: added because `Hom.ext'` is not triggered automatically
+-- Porting note (#5229): added because `Hom.ext'` is not triggered automatically
 @[ext]
 theorem Hom.ext {a b : SimplexCategory} (f g : a ⟶ b) :
     f.toOrderHom = g.toOrderHom → f = g :=

Mathlib/AlgebraicTopology/SplitSimplicialObject.lean

@@ -351,7 +351,7 @@ variable {C}
 
 namespace Split
 
--- Porting note: added as `Hom.ext` is not triggered automatically
+-- Porting note (#5229): added as `Hom.ext` is not triggered automatically
 @[ext]
 theorem hom_ext {S₁ S₂ : Split C} (Φ₁ Φ₂ : S₁ ⟶ S₂) (h : ∀ n : ℕ, Φ₁.f n = Φ₂.f n) : Φ₁ = Φ₂ :=
   Hom.ext _ _ h

Mathlib/CategoryTheory/Abelian/Pseudoelements.lean

@@ -258,7 +258,7 @@ theorem zero_morphism_ext {P Q : C} (f : P ⟶ Q) : (∀ a, f a = 0) → f = 0 :
 theorem zero_morphism_ext' {P Q : C} (f : P ⟶ Q) : (∀ a, f a = 0) → 0 = f :=
   Eq.symm ∘ zero_morphism_ext f
 
--- Porting note: these are no longer valid as `ext` lemmas.
+-- Porting note (#11182): these are no longer valid as `ext` lemmas.
 -- scoped[Pseudoelement]
 --   attribute [ext]
 --     CategoryTheory.Abelian.Pseudoelement.zero_morphism_ext

Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean

@@ -245,7 +245,7 @@ instance category (F G : OplaxFunctor B C) : Category (F ⟶ G) where
   id := Modification.id
   comp := Modification.vcomp
 
--- Porting note: duplicating the `ext` lemma.
+-- Porting note (#5229): duplicating the `ext` lemma.
 @[ext]
 lemma ext {F G : OplaxFunctor B C} {α β : F ⟶ G} {m n : α ⟶ β} (w : ∀ b, m.app b = n.app b) :
     m = n := by

Mathlib/CategoryTheory/Closed/Functor.lean

@@ -79,14 +79,14 @@ theorem expComparison_ev (A B : C) :
     Limits.prod.map (𝟙 (F.obj A)) ((expComparison F A).app B) ≫ (exp.ev (F.obj A)).app (F.obj B) =
       inv (prodComparison F _ _) ≫ F.map ((exp.ev _).app _) := by
   convert mateEquiv_counit _ _ (prodComparisonNatIso F A).inv B using 2
-  apply IsIso.inv_eq_of_hom_inv_id -- Porting note: was `ext`
+  apply IsIso.inv_eq_of_hom_inv_id -- Porting note (#11041): was `ext`
   simp only [Limits.prodComparisonNatIso_inv, asIso_inv, NatIso.isIso_inv_app, IsIso.hom_inv_id]
 
 theorem coev_expComparison (A B : C) :
     F.map ((exp.coev A).app B) ≫ (expComparison F A).app (A ⨯ B) =
       (exp.coev _).app (F.obj B) ≫ (exp (F.obj A)).map (inv (prodComparison F A B)) := by
   convert unit_mateEquiv _ _ (prodComparisonNatIso F A).inv B using 3
-  apply IsIso.inv_eq_of_hom_inv_id -- Porting note: was `ext`
+  apply IsIso.inv_eq_of_hom_inv_id -- Porting note (#11041): was `ext`
   dsimp
   simp
 

Mathlib/CategoryTheory/Comma/Basic.lean

@@ -106,7 +106,7 @@ section
 
 variable {X Y Z : Comma L R} {f : X ⟶ Y} {g : Y ⟶ Z}
 
--- Porting note: this lemma was added because `CommaMorphism.ext`
+-- Porting note (#5229): this lemma was added because `CommaMorphism.ext`
 -- was not triggered automatically
 @[ext]
 lemma hom_ext (f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) : f = g :=