diff --git a/src/algebra/free_monoid/count.lean b/src/algebra/free_monoid/count.lean
index f526f01c6b861..ac642cb2e04ba 100644
--- a/src/algebra/free_monoid/count.lean
+++ b/src/algebra/free_monoid/count.lean
@@ -9,6 +9,9 @@ import data.list.count
 /-!
 # `list.count` as a bundled homomorphism
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `free_monoid.countp`, `free_monoid.count`, `free_add_monoid.countp`, and
 `free_add_monoid.count`. These are `list.countp` and `list.count` bundled as multiplicative and
 additive homomorphisms from `free_monoid` and `free_add_monoid`.
diff --git a/src/algebra/order/lattice_group.lean b/src/algebra/order/lattice_group.lean
index 2a18a28a237f6..3993c527055ea 100644
--- a/src/algebra/order/lattice_group.lean
+++ b/src/algebra/order/lattice_group.lean
@@ -10,6 +10,9 @@ import tactic.nth_rewrite
 /-!
 # Lattice ordered groups
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Lattice ordered groups were introduced by [Birkhoff][birkhoff1942].
 They form the algebraic underpinnings of vector lattices, Banach lattices, AL-space, AM-space etc.
 
diff --git a/src/data/fin/basic.lean b/src/data/fin/basic.lean
index 2be427042b554..a5ba4089bbf05 100644
--- a/src/data/fin/basic.lean
+++ b/src/data/fin/basic.lean
@@ -12,6 +12,9 @@ import order.hom.set
 /-!
 # The finite type with `n` elements
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 `fin n` is the type whose elements are natural numbers smaller than `n`.
 This file expands on the development in the core library.
 
diff --git a/src/data/int/range.lean b/src/data/int/range.lean
index 2bc2fa5cc67fa..9bde57f55dfcd 100644
--- a/src/data/int/range.lean
+++ b/src/data/int/range.lean
@@ -9,6 +9,9 @@ import data.int.order.basic
 /-!
 # Intervals in ℤ
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines integer ranges. `range m n` is the set of integers greater than `m` and strictly
 less than `n`.
 
diff --git a/src/data/list/destutter.lean b/src/data/list/destutter.lean
index 8a761a809ea43..b6a7de18ec97b 100644
--- a/src/data/list/destutter.lean
+++ b/src/data/list/destutter.lean
@@ -8,6 +8,9 @@ import data.list.chain
 /-!
 # Destuttering of Lists
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves theorems about `list.destutter` (in `data.list.defs`), which greedily removes all
 non-related items that are adjacent in a list, e.g. `[2, 2, 3, 3, 2].destutter (≠) = [2, 3, 2]`.
 Note that we make no guarantees of being the longest sublist with this property; e.g.,
diff --git a/src/data/list/nat_antidiagonal.lean b/src/data/list/nat_antidiagonal.lean
index de578eb557c0d..c33f04c354aba 100644
--- a/src/data/list/nat_antidiagonal.lean
+++ b/src/data/list/nat_antidiagonal.lean
@@ -9,6 +9,9 @@ import data.list.range
 /-!
 # Antidiagonals in ℕ × ℕ as lists
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the antidiagonals of ℕ × ℕ as lists: the `n`-th antidiagonal is the list of
 pairs `(i, j)` such that `i + j = n`. This is useful for polynomial multiplication and more
 generally for sums going from `0` to `n`.
diff --git a/src/data/list/perm.lean b/src/data/list/perm.lean
index 5064dbc38934e..d00606e913151 100644
--- a/src/data/list/perm.lean
+++ b/src/data/list/perm.lean
@@ -11,6 +11,9 @@ import data.nat.factorial.basic
 /-!
 # List Permutations
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file introduces the `list.perm` relation, which is true if two lists are permutations of one
 another.
 
diff --git a/src/data/list/prime.lean b/src/data/list/prime.lean
index 277c6e3743e4e..191bd08aa6ba3 100644
--- a/src/data/list/prime.lean
+++ b/src/data/list/prime.lean
@@ -11,6 +11,9 @@ import data.list.perm
 /-!
 # Products of lists of prime elements.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains some theorems relating `prime` and products of `list`s.
 
 -/
diff --git a/src/order/circular.lean b/src/order/circular.lean
index 5255e3f546214..e768116353649 100644
--- a/src/order/circular.lean
+++ b/src/order/circular.lean
@@ -8,6 +8,9 @@ import data.set.basic
 /-!
 # Circular order hierarchy
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines circular preorders, circular partial orders and circular orders.
 
 ## Hierarchy