chore: classify added to speed up elaboration porting notes (#10695)

Classifies by adding issue number (#10694) to porting notes claiming `added to speed up elaboration`.
leanprover-community · Feb 20, 2024 · d2a67d6 · d2a67d6
1 parent b82dd45
commit d2a67d6
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean b/Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean
@@ -117,7 +117,7 @@ theorem N₁Γ₀_inv_app_f_f (K : ChainComplex C ℕ) (n : ℕ) :
 set_option linter.uppercaseLean3 false in
 #align algebraic_topology.dold_kan.N₁Γ₀_inv_app_f_f AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f
 
--- Porting note: added to speed up elaboration
+-- Porting note (#10694): added to speed up elaboration
 attribute [irreducible] N₁Γ₀
 
 /-- Compatibility isomorphism between `toKaroubi _ ⋙ Γ₂ ⋙ N₂` and `Γ₀ ⋙ N₁` which
@@ -160,7 +160,7 @@ lemma N₂Γ₂ToKaroubiIso_inv_app (X : ChainComplex C ℕ) :
   rw [Splitting.ι_desc]
   erw [comp_id, id_comp]
 
--- Porting note: added to speed up elaboration
+-- Porting note (#10694): added to speed up elaboration
 attribute [irreducible] N₂Γ₂ToKaroubiIso
 
 /-- The counit isomorphism of the Dold-Kan equivalence for additive categories. -/
@@ -195,7 +195,7 @@ lemma whiskerLeft_toKaroubi_N₂Γ₂_hom :
   dsimp only [whiskeringLeft, N₂Γ₂, Functor.preimageIso] at h ⊢
   exact h
 
--- Porting note: added to speed up elaboration
+-- Porting note (#10694): added to speed up elaboration
 attribute [irreducible] N₂Γ₂
 
 theorem N₂Γ₂_compatible_with_N₁Γ₀ (K : ChainComplex C ℕ) :

diff --git a/Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean b/Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
@@ -165,7 +165,7 @@ def natTrans : (N₁ : SimplicialObject C ⥤ _) ⋙ Γ₂ ⟶ toKaroubi _ where
 set_option linter.uppercaseLean3 false in
 #align algebraic_topology.dold_kan.Γ₂N₁.nat_trans AlgebraicTopology.DoldKan.Γ₂N₁.natTrans
 
--- Porting note: added to speed up elaboration
+-- Porting note (#10694): added to speed up elaboration
 attribute [irreducible] natTrans
 
 end Γ₂N₁
@@ -187,7 +187,7 @@ lemma Γ₂N₂ToKaroubiIso_inv_app (X : SimplicialObject C) :
     Γ₂N₂ToKaroubiIso.inv.app X = Γ₂.map (toKaroubiCompN₂IsoN₁.inv.app X) := by
   simp [Γ₂N₂ToKaroubiIso]
 
--- Porting note: added to speed up elaboration
+-- Porting note (#10694): added to speed up elaboration
 attribute [irreducible] Γ₂N₂ToKaroubiIso
 
 namespace Γ₂N₂
@@ -208,7 +208,7 @@ theorem natTrans_app_f_app (P : Karoubi (SimplicialObject C)) :
 set_option linter.uppercaseLean3 false in
 #align algebraic_topology.dold_kan.Γ₂N₂.nat_trans_app_f_app AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app
 
--- Porting note: added to speed up elaboration
+-- Porting note (#10694): added to speed up elaboration
 attribute [irreducible] natTrans
 
 end Γ₂N₂