chore: classify added lemma porting notes (#10958)

Classifies by adding issue number #10756 to porting notes claiming `added lemma`.
leanprover-community · Feb 27, 2024 · 1ea8344 · 1ea8344
1 parent 51d070d
commit 1ea8344
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet.lean b/Mathlib/AlgebraicTopology/SimplicialSet.lean
@@ -64,7 +64,7 @@ instance hasColimits : HasColimits SSet := by
   dsimp only [SSet]
   infer_instance
 
--- Porting note: added an `ext` lemma.
+-- Porting note (#10756): added an `ext` lemma.
 -- See https://github.com/leanprover-community/mathlib4/issues/5229
 @[ext]
 lemma hom_ext {X Y : SSet} {f g : X ⟶ Y} (w : ∀ n, f.app n = g.app n) : f = g :=
@@ -360,7 +360,7 @@ instance Truncated.hasColimits : HasColimits (Truncated n) := by
   dsimp only [Truncated]
   infer_instance
 
--- Porting note: added an `ext` lemma.
+-- Porting note (#10756): added an `ext` lemma.
 -- See https://github.com/leanprover-community/mathlib4/issues/5229
 @[ext]
 lemma Truncated.hom_ext {X Y : Truncated n} {f g : X ⟶ Y} (w : ∀ n, f.app n = g.app n) : f = g :=

diff --git a/Mathlib/Topology/Sheaves/Presheaf.lean b/Mathlib/Topology/Sheaves/Presheaf.lean
@@ -58,7 +58,7 @@ namespace Presheaf
 @[simp] theorem comp_app {P Q R : Presheaf C X} (f : P ⟶ Q) (g : Q ⟶ R) :
     (f ≫ g).app U = f.app U ≫ g.app U := rfl
 
--- Porting note: added an `ext` lemma,
+-- Porting note (#10756): added an `ext` lemma,
 -- since `NatTrans.ext` can not see through the definition of `Presheaf`.
 -- See https://github.com/leanprover-community/mathlib4/issues/5229
 @[ext]