diff --git a/Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean b/Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
index 1ff1ef3340afb..e64312fad7ff5 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.CategoryTheory.Equivalence
 
-#align_import algebraic_topology.dold_kan.compatibility from "leanprover-community/mathlib"@"18ee599842a5d17f189fe572f0ed8cb1d064d772"
+#align_import algebraic_topology.dold_kan.compatibility from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-! Tools for compatibilities between Dold-Kan equivalences
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean b/Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean
index 501b129b5d212..ad53c8aa27a47 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.AlgebraicTopology.DoldKan.PInfty
 
-#align_import algebraic_topology.dold_kan.decomposition from "leanprover-community/mathlib"@"9af20344b24ef1801b599d296aaed8b9fffdc360"
+#align_import algebraic_topology.dold_kan.decomposition from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean b/Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean
index 7767b3d5e5fba..6ed3017c45980 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean
@@ -6,7 +6,7 @@ Authors: Joël Riou
 import Mathlib.AlgebraicTopology.DoldKan.Decomposition
 import Mathlib.Tactic.FinCases
 
-#align_import algebraic_topology.dold_kan.degeneracies from "leanprover-community/mathlib"@"ec1c7d810034d4202b0dd239112d1792be9f6fdc"
+#align_import algebraic_topology.dold_kan.degeneracies from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/EquivalenceAdditive.lean b/Mathlib/AlgebraicTopology/DoldKan/EquivalenceAdditive.lean
index 14cf98ec0561a..a0fd47f7a8fb0 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/EquivalenceAdditive.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/EquivalenceAdditive.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.AlgebraicTopology.DoldKan.NCompGamma
 
-#align_import algebraic_topology.dold_kan.equivalence_additive from "leanprover-community/mathlib"@"19d6240dcc5e5c8bd6e1e3c588b92e837af76f9e"
+#align_import algebraic_topology.dold_kan.equivalence_additive from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-! The Dold-Kan equivalence for additive categories.
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean b/Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean
index 43016a169b56f..9361f1afb2e68 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean
@@ -7,7 +7,7 @@ import Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
 import Mathlib.AlgebraicTopology.DoldKan.Compatibility
 import Mathlib.CategoryTheory.Idempotents.SimplicialObject
 
-#align_import algebraic_topology.dold_kan.equivalence_pseudoabelian from "leanprover-community/mathlib"@"63721b2c3eba6c325ecf8ae8cca27155a4f6306f"
+#align_import algebraic_topology.dold_kan.equivalence_pseudoabelian from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Faces.lean b/Mathlib/AlgebraicTopology/DoldKan/Faces.lean
index 65218421c57e0..7fdcdfc9fa43f 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/Faces.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/Faces.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.AlgebraicTopology.DoldKan.Homotopies
 
-#align_import algebraic_topology.dold_kan.faces from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
+#align_import algebraic_topology.dold_kan.faces from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean b/Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
index af165377bf768..7e85d31df611f 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
 
-#align_import algebraic_topology.dold_kan.functor_gamma from "leanprover-community/mathlib"@"5b8284148e8149728f4b90624888d98c36284454"
+#align_import algebraic_topology.dold_kan.functor_gamma from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/FunctorN.lean b/Mathlib/AlgebraicTopology/DoldKan/FunctorN.lean
index 41516157d8c93..e728fa265609b 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/FunctorN.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/FunctorN.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.AlgebraicTopology.DoldKan.PInfty
 
-#align_import algebraic_topology.dold_kan.functor_n from "leanprover-community/mathlib"@"1995c7bbdbb0adb1b6d5acdc654f6cf46ed96cfa"
+#align_import algebraic_topology.dold_kan.functor_n from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean b/Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean
index db3a28a6a5ade..82ef04695fa2d 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean
@@ -6,7 +6,7 @@ Authors: Joël Riou
 import Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
 import Mathlib.CategoryTheory.Idempotents.HomologicalComplex
 
-#align_import algebraic_topology.dold_kan.gamma_comp_n from "leanprover-community/mathlib"@"5f68029a863bdf76029fa0f7a519e6163c14152e"
+#align_import algebraic_topology.dold_kan.gamma_comp_n from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-! The counit isomorphism of the Dold-Kan equivalence
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean b/Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
index ce098e00e91a9..613ee2aabf79d 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
@@ -6,7 +6,7 @@ Authors: Joël Riou
 import Mathlib.AlgebraicTopology.DoldKan.GammaCompN
 import Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
 
-#align_import algebraic_topology.dold_kan.n_comp_gamma from "leanprover-community/mathlib"@"19d6240dcc5e5c8bd6e1e3c588b92e837af76f9e"
+#align_import algebraic_topology.dold_kan.n_comp_gamma from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-! The unit isomorphism of the Dold-Kan equivalence
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean b/Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean
index 6b0cbe932ea78..25f486dc08c1f 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean
@@ -8,7 +8,7 @@ import Mathlib.AlgebraicTopology.DoldKan.Decomposition
 import Mathlib.CategoryTheory.Idempotents.HomologicalComplex
 import Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
 
-#align_import algebraic_topology.dold_kan.n_reflects_iso from "leanprover-community/mathlib"@"88bca0ce5d22ebfd9e73e682e51d60ea13b48347"
+#align_import algebraic_topology.dold_kan.n_reflects_iso from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Normalized.lean b/Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
index b2eeb7743a924..5ca926ffda2a1 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.AlgebraicTopology.DoldKan.FunctorN
 
-#align_import algebraic_topology.dold_kan.normalized from "leanprover-community/mathlib"@"d1d69e99ed34c95266668af4e288fc1c598b9a7f"
+#align_import algebraic_topology.dold_kan.normalized from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Notations.lean b/Mathlib/AlgebraicTopology/DoldKan/Notations.lean
index 10da97e674b63..d90b0949a7f51 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/Notations.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/Notations.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
 
-#align_import algebraic_topology.dold_kan.notations from "leanprover-community/mathlib"@"3d7987cda72abc473c7cdbbb075170e9ac620042"
+#align_import algebraic_topology.dold_kan.notations from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/PInfty.lean b/Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
index 76f1fe367aa14..60bd2573b1fe3 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
@@ -7,7 +7,7 @@ import Mathlib.AlgebraicTopology.DoldKan.Projections
 import Mathlib.CategoryTheory.Idempotents.FunctorCategories
 import Mathlib.CategoryTheory.Idempotents.FunctorExtension
 
-#align_import algebraic_topology.dold_kan.p_infty from "leanprover-community/mathlib"@"31019c2504b17f85af7e0577585fad996935a317"
+#align_import algebraic_topology.dold_kan.p_infty from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Projections.lean b/Mathlib/AlgebraicTopology/DoldKan/Projections.lean
index 8dc270f9aa686..520c32332f351 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/Projections.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/Projections.lean
@@ -6,7 +6,7 @@ Authors: Joël Riou
 import Mathlib.AlgebraicTopology.DoldKan.Faces
 import Mathlib.CategoryTheory.Idempotents.Basic
 
-#align_import algebraic_topology.dold_kan.projections from "leanprover-community/mathlib"@"ed98c07faf6d9de3e52771d5b00394c4294ccb4d"
+#align_import algebraic_topology.dold_kan.projections from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 
diff --git a/Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean b/Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean
index 242186269936a..7b48a3bbd4146 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean
@@ -7,7 +7,7 @@ import Mathlib.AlgebraicTopology.SplitSimplicialObject
 import Mathlib.AlgebraicTopology.DoldKan.Degeneracies
 import Mathlib.AlgebraicTopology.DoldKan.FunctorN
 
-#align_import algebraic_topology.dold_kan.split_simplicial_object from "leanprover-community/mathlib"@"31019c2504b17f85af7e0577585fad996935a317"
+#align_import algebraic_topology.dold_kan.split_simplicial_object from "leanprover-community/mathlib"@"32a7e535287f9c73f2e4d2aef306a39190f0b504"
 
 /-!
 
diff --git a/Mathlib/CategoryTheory/Functor/Category.lean b/Mathlib/CategoryTheory/Functor/Category.lean
index cdd38a6e40500..1c71c587947cf 100644
--- a/Mathlib/CategoryTheory/Functor/Category.lean
+++ b/Mathlib/CategoryTheory/Functor/Category.lean
@@ -6,7 +6,7 @@ Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
 import Mathlib.CategoryTheory.NatTrans
 import Mathlib.CategoryTheory.Iso
 
-#align_import category_theory.functor.category from "leanprover-community/mathlib"@"8350c34a64b9bc3fc64335df8006bffcadc7baa6"
+#align_import category_theory.functor.category from "leanprover-community/mathlib"@"63721b2c3eba6c325ecf8ae8cca27155a4f6306f"
 
 /-!
 # The category of functors and natural transformations between two fixed categories.