diff --git a/src/algebra/category/Mon/adjunctions.lean b/src/algebra/category/Mon/adjunctions.lean
index 54e756448f059..d3e500532d249 100644
--- a/src/algebra/category/Mon/adjunctions.lean
+++ b/src/algebra/category/Mon/adjunctions.lean
@@ -11,6 +11,9 @@ import algebra.free_monoid.basic
 /-!
 # Adjunctions regarding the category of monoids
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves the adjunction between adjoining a unit to a semigroup and the forgetful functor
 from monoids to semigroups.
 
diff --git a/src/algebra/category/Semigroup/basic.lean b/src/algebra/category/Semigroup/basic.lean
index 65bb2df05eb96..7e8666e59eda3 100644
--- a/src/algebra/category/Semigroup/basic.lean
+++ b/src/algebra/category/Semigroup/basic.lean
@@ -12,6 +12,9 @@ import category_theory.elementwise
 /-!
 # Category instances for has_mul, has_add, semigroup and add_semigroup
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We introduce the bundled categories:
 * `Magma`
 * `AddMagma`
diff --git a/src/algebraic_geometry/function_field.lean b/src/algebraic_geometry/function_field.lean
index 6e8f90ac361b0..628ccd684a434 100644
--- a/src/algebraic_geometry/function_field.lean
+++ b/src/algebraic_geometry/function_field.lean
@@ -8,6 +8,9 @@ import algebraic_geometry.properties
 /-!
 # Function field of integral schemes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the function field of an irreducible scheme as the stalk of the generic point.
 This is a field when the scheme is integral.
 
diff --git a/src/algebraic_geometry/morphisms/basic.lean b/src/algebraic_geometry/morphisms/basic.lean
index 322daeb6e9816..5ff036cda8b73 100644
--- a/src/algebraic_geometry/morphisms/basic.lean
+++ b/src/algebraic_geometry/morphisms/basic.lean
@@ -10,6 +10,9 @@ import category_theory.morphism_property
 /-!
 # Properties of morphisms between Schemes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We provide the basic framework for talking about properties of morphisms between Schemes.
 
 A `morphism_property Scheme` is a predicate on morphisms between schemes, and an
diff --git a/src/algebraic_geometry/morphisms/open_immersion.lean b/src/algebraic_geometry/morphisms/open_immersion.lean
index 62465fea56bb8..4ae87dfbdce6e 100644
--- a/src/algebraic_geometry/morphisms/open_immersion.lean
+++ b/src/algebraic_geometry/morphisms/open_immersion.lean
@@ -10,6 +10,9 @@ import algebraic_geometry.morphisms.basic
 
 # Open immersions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A morphism is an open immersions if the underlying map of spaces is an open embedding
 `f : X ⟶ U ⊆ Y`, and the sheaf map `Y(V) ⟶ f _* X(V)` is an iso for each `V ⊆ U`.
 
diff --git a/src/algebraic_geometry/morphisms/universally_closed.lean b/src/algebraic_geometry/morphisms/universally_closed.lean
index 036ff1844d1d9..1d53bcffeb4ca 100644
--- a/src/algebraic_geometry/morphisms/universally_closed.lean
+++ b/src/algebraic_geometry/morphisms/universally_closed.lean
@@ -9,6 +9,9 @@ import topology.local_at_target
 /-!
 # Universally closed morphism
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A morphism of schemes `f : X ⟶ Y` is universally closed if `X ×[Y] Y' ⟶ Y'` is a closed map
 for all base change `Y' ⟶ Y`.
 
diff --git a/src/analysis/complex/upper_half_plane/manifold.lean b/src/analysis/complex/upper_half_plane/manifold.lean
index b5a8b7ec6de4b..0c070195cc5dd 100644
--- a/src/analysis/complex/upper_half_plane/manifold.lean
+++ b/src/analysis/complex/upper_half_plane/manifold.lean
@@ -8,6 +8,9 @@ import geometry.manifold.cont_mdiff_mfderiv
 /-!
 # Manifold structure on the upper half plane.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define the complex manifold structure on the upper half-plane.
 -/
 
diff --git a/src/analysis/convex/cone/proper.lean b/src/analysis/convex/cone/proper.lean
index 9babbda4c6ef3..8a76a074f3ae9 100644
--- a/src/analysis/convex/cone/proper.lean
+++ b/src/analysis/convex/cone/proper.lean
@@ -9,6 +9,9 @@ import analysis.inner_product_space.adjoint
 /-!
 # Proper cones
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define a proper cone as a nonempty, closed, convex cone. Proper cones are used in defining conic
 programs which generalize linear programs. A linear program is a conic program for the positive
 cone. We then prove Farkas' lemma for conic programs following the proof in the reference below.
diff --git a/src/category_theory/limits/constructions/over/basic.lean b/src/category_theory/limits/constructions/over/basic.lean
index e4085355f2824..9e71f7f3ed156 100644
--- a/src/category_theory/limits/constructions/over/basic.lean
+++ b/src/category_theory/limits/constructions/over/basic.lean
@@ -12,6 +12,9 @@ import category_theory.limits.constructions.equalizers
 /-!
 # Limits in the over category
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Declare instances for limits in the over category: If `C` has finite wide pullbacks, `over B` has
 finite limits, and if `C` has arbitrary wide pullbacks then `over B` has limits.
 -/
diff --git a/src/geometry/manifold/algebra/smooth_functions.lean b/src/geometry/manifold/algebra/smooth_functions.lean
index 932b3e776ebf1..47e08e8c88e99 100644
--- a/src/geometry/manifold/algebra/smooth_functions.lean
+++ b/src/geometry/manifold/algebra/smooth_functions.lean
@@ -9,6 +9,9 @@ import geometry.manifold.algebra.structures
 /-!
 # Algebraic structures over smooth functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we define instances of algebraic structures over smooth functions.
 -/
 
diff --git a/src/geometry/manifold/derivation_bundle.lean b/src/geometry/manifold/derivation_bundle.lean
index 71f103747b268..d4ad6affb65b6 100644
--- a/src/geometry/manifold/derivation_bundle.lean
+++ b/src/geometry/manifold/derivation_bundle.lean
@@ -11,6 +11,9 @@ import ring_theory.derivation.basic
 
 # Derivation bundle
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define the derivations at a point of a manifold on the algebra of smooth fuctions.
 Moreover, we define the differential of a function in terms of derivations.
 
diff --git a/src/number_theory/modular_forms/jacobi_theta/manifold.lean b/src/number_theory/modular_forms/jacobi_theta/manifold.lean
index 67094c9757bca..81a9584cd7556 100644
--- a/src/number_theory/modular_forms/jacobi_theta/manifold.lean
+++ b/src/number_theory/modular_forms/jacobi_theta/manifold.lean
@@ -9,6 +9,9 @@ import analysis.complex.upper_half_plane.manifold
 /-!
 # Manifold differentiability of the Jacobi's theta function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we reformulate differentiability of the Jacobi's theta function in terms of manifold
 differentiability.
 
diff --git a/src/representation_theory/fdRep.lean b/src/representation_theory/fdRep.lean
index 213f589b738dd..70cef6ac6b148 100644
--- a/src/representation_theory/fdRep.lean
+++ b/src/representation_theory/fdRep.lean
@@ -11,6 +11,9 @@ import representation_theory.basic
 /-!
 # `fdRep k G` is the category of finite dimensional `k`-linear representations of `G`.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If `V : fdRep k G`, there is a coercion that allows you to treat `V` as a type,
 and this type comes equipped with `module k V` and `finite_dimensional k V` instances.
 Also `V.ρ` gives the homomorphism `G →* (V →ₗ[k] V)`.
diff --git a/src/representation_theory/invariants.lean b/src/representation_theory/invariants.lean
index 465fc5df768ae..5a9380d2cc6c3 100644
--- a/src/representation_theory/invariants.lean
+++ b/src/representation_theory/invariants.lean
@@ -9,6 +9,9 @@ import representation_theory.fdRep
 /-!
 # Subspace of invariants a group representation
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file introduces the subspace of invariants of a group representation
 and proves basic results about it.
 The main tool used is the average of all elements of the group, seen as an element of
diff --git a/src/ring_theory/witt_vector/isocrystal.lean b/src/ring_theory/witt_vector/isocrystal.lean
index bc06cef87421a..02374a808e1f4 100644
--- a/src/ring_theory/witt_vector/isocrystal.lean
+++ b/src/ring_theory/witt_vector/isocrystal.lean
@@ -10,6 +10,9 @@ import ring_theory.witt_vector.frobenius_fraction_field
 
 ## F-isocrystals over a perfect field
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 When `k` is an integral domain, so is `𝕎 k`, and we can consider its field of fractions `K(p, k)`.
 The endomorphism `witt_vector.frobenius` lifts to `φ : K(p, k) → K(p, k)`; if `k` is perfect, `φ` is
 an automorphism.
diff --git a/src/set_theory/game/domineering.lean b/src/set_theory/game/domineering.lean
index 3190d0fa99854..43958be820b70 100644
--- a/src/set_theory/game/domineering.lean
+++ b/src/set_theory/game/domineering.lean
@@ -8,6 +8,9 @@ import set_theory.game.state
 /-!
 # Domineering as a combinatorial game.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the game of Domineering, played on a chessboard of arbitrary shape
 (possibly even disconnected).
 Left moves by placing a domino vertically, while Right moves by placing a domino horizontally.
diff --git a/src/set_theory/game/short.lean b/src/set_theory/game/short.lean
index 8d2bb319530e5..6b5867a25770c 100644
--- a/src/set_theory/game/short.lean
+++ b/src/set_theory/game/short.lean
@@ -10,6 +10,9 @@ import set_theory.game.birthday
 /-!
 # Short games
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A combinatorial game is `short` [Conway, ch.9][conway2001] if it has only finitely many positions.
 In particular, this means there is a finite set of moves at every point.
 
diff --git a/src/set_theory/game/state.lean b/src/set_theory/game/state.lean
index 14f118bc5685d..27f9ca055dce5 100644
--- a/src/set_theory/game/state.lean
+++ b/src/set_theory/game/state.lean
@@ -8,6 +8,9 @@ import set_theory.game.short
 /-!
 # Games described via "the state of the board".
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We provide a simple mechanism for constructing combinatorial (pre-)games, by describing
 "the state of the board", and providing an upper bound on the number of turns remaining.
 
diff --git a/src/topology/homotopy/product.lean b/src/topology/homotopy/product.lean
index 06b9d0449ed71..bc5ccd0df73f3 100644
--- a/src/topology/homotopy/product.lean
+++ b/src/topology/homotopy/product.lean
@@ -9,6 +9,9 @@ import topology.homotopy.path
 /-!
 # Product of homotopies
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we introduce definitions for the product of
 homotopies. We show that the products of relative homotopies
 are still relative homotopies. Finally, we specialize to the case