diff --git a/src/algebraic_topology/dold_kan/equivalence.lean b/src/algebraic_topology/dold_kan/equivalence.lean
index dc025a7938b2b..960d5589d5a72 100644
--- a/src/algebraic_topology/dold_kan/equivalence.lean
+++ b/src/algebraic_topology/dold_kan/equivalence.lean
@@ -11,6 +11,9 @@ import algebraic_topology.dold_kan.normalized
 
 # The Dold-Kan correspondence
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The Dold-Kan correspondence states that for any abelian category `A`, there is
 an equivalence between the category of simplicial objects in `A` and the
 category of chain complexes in `A` (with degrees indexed by `ℕ` and the
diff --git a/src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean b/src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean
index 4d6fff16434a8..5514db73f68eb 100644
--- a/src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean
+++ b/src/algebraic_topology/dold_kan/equivalence_pseudoabelian.lean
@@ -12,6 +12,9 @@ import category_theory.idempotents.simplicial_object
 
 # The Dold-Kan correspondence for pseudoabelian categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, for any idempotent complete additive category `C`,
 the Dold-Kan equivalence
 `idempotents.dold_kan.equivalence C : simplicial_object C ≌ chain_complex C ℕ`
diff --git a/src/combinatorics/quiver/covering.lean b/src/combinatorics/quiver/covering.lean
index 18c98970d2cfd..4430c0d1b7e84 100644
--- a/src/combinatorics/quiver/covering.lean
+++ b/src/combinatorics/quiver/covering.lean
@@ -11,6 +11,9 @@ import logic.equiv.basic
 /-!
 # Covering
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines coverings of quivers as prefunctors that are bijective on the
 so-called stars and costars at each vertex of the domain.