From 92a78924051bfc7c64d6d322b68830f8c0f2eff1 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 5 Mar 2024 22:19:28 +0000
Subject: [PATCH] chore: classify `removed @[ext]` porting notes (#11183)

Classifies by adding issue number #11182 to porting notes claiming:

> removed `@[ext]`
---
 Mathlib/CategoryTheory/Limits/Types.lean    | 2 +-
 Mathlib/CategoryTheory/Preadditive/Mat.lean | 2 +-
 Mathlib/CategoryTheory/Subobject/Basic.lean | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Mathlib/CategoryTheory/Limits/Types.lean b/Mathlib/CategoryTheory/Limits/Types.lean
index d3195c098e255..745d99f8a9613 100644
--- a/Mathlib/CategoryTheory/Limits/Types.lean
+++ b/Mathlib/CategoryTheory/Limits/Types.lean
@@ -226,7 +226,7 @@ theorem limitEquivSections_symm_apply (F : J ⥤ Type u) (x : F.sections) (j : J
 --  isLimitEquivSections_symm_apply _ _ _
 --#align category_theory.limits.types.limit_equiv_sections_symm_apply' CategoryTheory.Limits.Types.limitEquivSections_symm_apply'
 
--- Porting note: removed @[ext]
+-- Porting note (#11182): removed @[ext]
 /-- Construct a term of `limit F : Type u` from a family of terms `x : Π j, F.obj j`
 which are "coherent": `∀ (j j') (f : j ⟶ j'), F.map f (x j) = x j'`.
 -/
diff --git a/Mathlib/CategoryTheory/Preadditive/Mat.lean b/Mathlib/CategoryTheory/Preadditive/Mat.lean
index 77a4a3cd57d5a..9c1e061dd7743 100644
--- a/Mathlib/CategoryTheory/Preadditive/Mat.lean
+++ b/Mathlib/CategoryTheory/Preadditive/Mat.lean
@@ -484,7 +484,7 @@ def liftUnique (F : C ⥤ D) [Functor.Additive F] (L : Mat_ C ⥤ D) [Functor.Ad
 set_option linter.uppercaseLean3 false in
 #align category_theory.Mat_.lift_unique CategoryTheory.Mat_.liftUnique
 
--- Porting note: removed @[ext] as the statement is not an equality
+-- Porting note (#11182): removed @[ext] as the statement is not an equality
 -- TODO is there some uniqueness statement for the natural isomorphism in `liftUnique`?
 /-- Two additive functors `Mat_ C ⥤ D` are naturally isomorphic if
 their precompositions with `embedding C` are naturally isomorphic as functors `C ⥤ D`. -/
diff --git a/Mathlib/CategoryTheory/Subobject/Basic.lean b/Mathlib/CategoryTheory/Subobject/Basic.lean
index 7ee3dacf94294..5a7db5db1be46 100644
--- a/Mathlib/CategoryTheory/Subobject/Basic.lean
+++ b/Mathlib/CategoryTheory/Subobject/Basic.lean
@@ -285,7 +285,7 @@ theorem eq_of_comm {B : C} {X Y : Subobject B} (f : (X : C) ≅ (Y : C))
   le_antisymm (le_of_comm f.hom w) <| le_of_comm f.inv <| f.inv_comp_eq.2 w.symm
 #align category_theory.subobject.eq_of_comm CategoryTheory.Subobject.eq_of_comm
 
--- Porting note: removed @[ext]
+-- Porting note (#11182): removed @[ext]
 /-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
     the arrows. -/
 theorem eq_mk_of_comm {B A : C} {X : Subobject B} (f : A ⟶ B) [Mono f] (i : (X : C) ≅ A)
@@ -293,7 +293,7 @@ theorem eq_mk_of_comm {B A : C} {X : Subobject B} (f : A ⟶ B) [Mono f] (i : (X
   eq_of_comm (i.trans (underlyingIso f).symm) <| by simp [w]
 #align category_theory.subobject.eq_mk_of_comm CategoryTheory.Subobject.eq_mk_of_comm
 
--- Porting note: removed @[ext]
+-- Porting note (#11182): removed @[ext]
 /-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
     the arrows. -/
 theorem mk_eq_of_comm {B A : C} {X : Subobject B} (f : A ⟶ B) [Mono f] (i : A ≅ (X : C))
@@ -301,7 +301,7 @@ theorem mk_eq_of_comm {B A : C} {X : Subobject B} (f : A ⟶ B) [Mono f] (i : A
   Eq.symm <| eq_mk_of_comm _ i.symm <| by rw [Iso.symm_hom, Iso.inv_comp_eq, w]
 #align category_theory.subobject.mk_eq_of_comm CategoryTheory.Subobject.mk_eq_of_comm
 
--- Porting note: removed @[ext]
+-- Porting note (#11182): removed @[ext]
 /-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
     the arrows. -/
 theorem mk_eq_mk_of_comm {B A₁ A₂ : C} (f : A₁ ⟶ B) (g : A₂ ⟶ B) [Mono f] [Mono g] (i : A₁ ≅ A₂)