diff --git a/archive/arithcc.lean b/archive/arithcc.lean
index 9de0770bbd8f2..f1feb07fa6173 100644
--- a/archive/arithcc.lean
+++ b/archive/arithcc.lean
@@ -9,6 +9,9 @@ import tactic.basic
 /-!
 # A compiler for arithmetic expressions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A formalization of the correctness of a compiler from arithmetic expressions to machine language
 described by McCarthy and Painter, which is considered the first proof of compiler correctness.
 
diff --git a/archive/examples/mersenne_primes.lean b/archive/examples/mersenne_primes.lean
index 2c5a28bdbea00..af4166ff31ebc 100644
--- a/archive/examples/mersenne_primes.lean
+++ b/archive/examples/mersenne_primes.lean
@@ -8,6 +8,9 @@ import number_theory.lucas_lehmer
 /-!
 # Explicit Mersenne primes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We run some Lucas-Lehmer tests to prove some Mersenne primes are prime.
 
 See the discussion at the end of [src/number_theory/lucas_lehmer.lean]
diff --git a/archive/examples/prop_encodable.lean b/archive/examples/prop_encodable.lean
index a877eeed41334..d2436fd06f034 100644
--- a/archive/examples/prop_encodable.lean
+++ b/archive/examples/prop_encodable.lean
@@ -9,6 +9,9 @@ import data.W.basic
 /-!
 # W types
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The file `data/W.lean` shows that if `α` is an an encodable fintype and for every `a : α`,
 `β a` is encodable, then `W β` is encodable.
 
diff --git a/archive/imo/imo1959_q1.lean b/archive/imo/imo1959_q1.lean
index bb0c5f8b63b36..fe34d1b143489 100644
--- a/archive/imo/imo1959_q1.lean
+++ b/archive/imo/imo1959_q1.lean
@@ -10,6 +10,9 @@ import data.nat.prime
 /-!
 # IMO 1959 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Prove that the fraction `(21n+4)/(14n+3)` is irreducible for every natural number `n`.
 
 Since Lean doesn't have a concept of "irreducible fractions" per se, we just formalize this
diff --git a/archive/imo/imo1960_q1.lean b/archive/imo/imo1960_q1.lean
index fa3ee7680092f..eccc3abb782e8 100644
--- a/archive/imo/imo1960_q1.lean
+++ b/archive/imo/imo1960_q1.lean
@@ -9,6 +9,9 @@ import data.nat.digits
 /-!
 # IMO 1960 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Determine all three-digit numbers $N$ having the property that $N$ is divisible by 11, and
 $\dfrac{N}{11}$ is equal to the sum of the squares of the digits of $N$.
 
diff --git a/archive/imo/imo1962_q1.lean b/archive/imo/imo1962_q1.lean
index 0afc5e6be6726..bd586605533fb 100644
--- a/archive/imo/imo1962_q1.lean
+++ b/archive/imo/imo1962_q1.lean
@@ -9,6 +9,9 @@ import data.nat.digits
 /-!
 # IMO 1962 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Find the smallest natural number $n$ which has the following properties:
 
 (a) Its decimal representation has 6 as the last digit.
diff --git a/archive/imo/imo1962_q4.lean b/archive/imo/imo1962_q4.lean
index 95b725d68beca..87996b4246960 100644
--- a/archive/imo/imo1962_q4.lean
+++ b/archive/imo/imo1962_q4.lean
@@ -9,6 +9,9 @@ import analysis.special_functions.trigonometric.complex
 /-!
 # IMO 1962 Q4
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Solve the equation `cos x ^ 2 + cos (2 * x) ^ 2 + cos (3 * x) ^ 2 = 1`.
 
 Since Lean does not have a concept of "simplest form", we just express what is
diff --git a/archive/imo/imo1964_q1.lean b/archive/imo/imo1964_q1.lean
index fd987ba4f5f10..f381845902b31 100644
--- a/archive/imo/imo1964_q1.lean
+++ b/archive/imo/imo1964_q1.lean
@@ -10,6 +10,9 @@ import data.nat.modeq
 /-!
 # IMO 1964 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 (a) Find all positive integers $n$ for which $2^n-1$ is divisible by $7$.
 
 (b) Prove that there is no positive integer $n$ for which $2^n+1$ is divisible by $7$.
diff --git a/archive/imo/imo1969_q1.lean b/archive/imo/imo1969_q1.lean
index 3eee264d353ca..b1e47a6bef7aa 100644
--- a/archive/imo/imo1969_q1.lean
+++ b/archive/imo/imo1969_q1.lean
@@ -11,6 +11,9 @@ import data.set.finite
 /-!
 # IMO 1969 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Prove that there are infinitely many natural numbers $a$ with the following property:
 the number $z = n^4 + a$ is not prime for any natural number $n$.
 -/
diff --git a/archive/imo/imo1972_q5.lean b/archive/imo/imo1972_q5.lean
index c796e589190f5..8dbb28ff56f04 100644
--- a/archive/imo/imo1972_q5.lean
+++ b/archive/imo/imo1972_q5.lean
@@ -10,6 +10,9 @@ import analysis.normed_space.basic
 /-!
 # IMO 1972 Q5
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Problem: `f` and `g` are real-valued functions defined on the real line. For all `x` and `y`,
 `f(x + y) + f(x - y) = 2f(x)g(y)`. `f` is not identically zero and `|f(x)| ≤ 1` for all `x`.
 Prove that `|g(x)| ≤ 1` for all `x`.
diff --git a/archive/imo/imo1975_q1.lean b/archive/imo/imo1975_q1.lean
index eaf260b9cdbac..b135b1806671d 100644
--- a/archive/imo/imo1975_q1.lean
+++ b/archive/imo/imo1975_q1.lean
@@ -11,6 +11,9 @@ import algebra.big_operators.ring
 /-!
 # IMO 1975 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `x₁, x₂, ... , xₙ` and `y₁, y₂, ... , yₙ` be two sequences of real numbers, such that
 `x₁ ≥ x₂ ≥ ... ≥ xₙ` and `y₁ ≥ y₂ ≥ ... ≥ yₙ`. Prove that if `z₁, z₂, ... , zₙ` is any permutation
 of `y₁, y₂, ... , yₙ`, then `∑ (xᵢ - yᵢ)^2 ≤ ∑ (xᵢ - zᵢ)^2`
diff --git a/archive/imo/imo1977_q6.lean b/archive/imo/imo1977_q6.lean
index 445644be7a341..8d3d44c050769 100644
--- a/archive/imo/imo1977_q6.lean
+++ b/archive/imo/imo1977_q6.lean
@@ -8,6 +8,9 @@ import data.pnat.basic
 /-!
 # IMO 1977 Q6
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Suppose `f : ℕ+ → ℕ+` satisfies `f(f(n)) < f(n + 1)` for all `n`.
 Prove that `f(n) = n` for all `n`.
 
diff --git a/archive/imo/imo1981_q3.lean b/archive/imo/imo1981_q3.lean
index 4b40612e5a873..10a40331f2eec 100644
--- a/archive/imo/imo1981_q3.lean
+++ b/archive/imo/imo1981_q3.lean
@@ -10,6 +10,9 @@ import tactic.linarith
 /-!
 # IMO 1981 Q3
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Determine the maximum value of `m ^ 2 + n ^ 2`, where `m` and `n` are integers in
 `{1, 2, ..., 1981}` and `(n ^ 2 - m * n - m ^ 2) ^ 2 = 1`.
 
diff --git a/archive/imo/imo1987_q1.lean b/archive/imo/imo1987_q1.lean
index b73054ddc9101..ffae4fbd202d7 100644
--- a/archive/imo/imo1987_q1.lean
+++ b/archive/imo/imo1987_q1.lean
@@ -11,6 +11,9 @@ import dynamics.fixed_points.basic
 /-!
 # Formalization of IMO 1987, Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let $p_{n, k}$ be the number of permutations of a set of cardinality `n ≥ 1` that fix exactly `k`
 elements. Prove that $∑_{k=0}^n k p_{n,k}=n!$.
 
diff --git a/archive/imo/imo1988_q6.lean b/archive/imo/imo1988_q6.lean
index d5cd3fa2020e3..4e2699c0f61d9 100644
--- a/archive/imo/imo1988_q6.lean
+++ b/archive/imo/imo1988_q6.lean
@@ -13,6 +13,9 @@ import tactic.wlog
 /-!
 # IMO 1988 Q6 and constant descent Vieta jumping
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Question 6 of IMO1988 is somewhat (in)famous. Several expert problem solvers
 could not tackle the question within the given time limit.
 The problem lead to the introduction of a new proof technique,
diff --git a/archive/imo/imo1994_q1.lean b/archive/imo/imo1994_q1.lean
index 289fdf3250ad2..89b584ee3ebce 100644
--- a/archive/imo/imo1994_q1.lean
+++ b/archive/imo/imo1994_q1.lean
@@ -14,6 +14,9 @@ import tactic.by_contra
 /-!
 # IMO 1994 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `m` and `n` be two positive integers.
 Let `a₁, a₂, ..., aₘ` be `m` different numbers from the set `{1, 2, ..., n}`
 such that for any two indices `i` and `j` with `1 ≤ i ≤ j ≤ m` and `aᵢ + aⱼ ≤ n`,
diff --git a/archive/imo/imo1998_q2.lean b/archive/imo/imo1998_q2.lean
index ab3cb7e1ccb35..7ce14e5cf3214 100644
--- a/archive/imo/imo1998_q2.lean
+++ b/archive/imo/imo1998_q2.lean
@@ -11,6 +11,9 @@ import tactic.noncomm_ring
 
 /-!
 # IMO 1998 Q2
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 In a competition, there are `a` contestants and `b` judges, where `b ≥ 3` is an odd integer. Each
 judge rates each contestant as either "pass" or "fail". Suppose `k` is a number such that, for any
 two judges, their ratings coincide for at most `k` contestants. Prove that `k / a ≥ (b - 1) / (2b)`.
diff --git a/archive/imo/imo2001_q2.lean b/archive/imo/imo2001_q2.lean
index fc2d5172f39e8..346adc3db71fd 100644
--- a/archive/imo/imo2001_q2.lean
+++ b/archive/imo/imo2001_q2.lean
@@ -9,6 +9,9 @@ import analysis.special_functions.pow.real
 /-!
 # IMO 2001 Q2
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let $a$, $b$, $c$ be positive reals. Prove that
 $$
 \frac{a}{\sqrt{a^2 + 8bc}} +
diff --git a/archive/imo/imo2001_q6.lean b/archive/imo/imo2001_q6.lean
index c2fa9f829a855..4b96c07090e1c 100644
--- a/archive/imo/imo2001_q6.lean
+++ b/archive/imo/imo2001_q6.lean
@@ -9,6 +9,9 @@ import tactic.linear_combination
 
 /-!
 # IMO 2001 Q6
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Let $a$, $b$, $c$, $d$ be integers with $a > b > c > d > 0$. Suppose that
 
 $$ a*c + b*d = (a + b - c + d) * (-a + b + c + d). $$
diff --git a/archive/imo/imo2005_q3.lean b/archive/imo/imo2005_q3.lean
index bfcb287444ded..9d4ef279453ea 100644
--- a/archive/imo/imo2005_q3.lean
+++ b/archive/imo/imo2005_q3.lean
@@ -8,6 +8,9 @@ import tactic.positivity
 
 /-!
 # IMO 2005 Q3
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Let `x`, `y` and `z` be positive real numbers such that `xyz ≥ 1`. Prove that:
 `(x^5 - x^2)/(x^5 + y^2 + z^2) + (y^5 - y^2)/(y^5 + z^2 + x^2) + (z^5 - z^2)/(z^5 + x^2 + y^2) ≥ 0`
 
diff --git a/archive/imo/imo2005_q4.lean b/archive/imo/imo2005_q4.lean
index 9caceeddf5abf..ac90ef53f0bcc 100644
--- a/archive/imo/imo2005_q4.lean
+++ b/archive/imo/imo2005_q4.lean
@@ -8,6 +8,9 @@ import field_theory.finite.basic
 /-!
 # IMO 2005 Q4
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Problem: Determine all positive integers relatively prime to all the terms of the infinite sequence
 `a n = 2 ^ n + 3 ^ n + 6 ^ n - 1`, for `n ≥ 1`.
 
diff --git a/archive/imo/imo2006_q3.lean b/archive/imo/imo2006_q3.lean
index 36a22e34bf2d0..8e3a0862d3ad4 100644
--- a/archive/imo/imo2006_q3.lean
+++ b/archive/imo/imo2006_q3.lean
@@ -9,6 +9,9 @@ import analysis.special_functions.sqrt
 /-!
 # IMO 2006 Q3
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Determine the least real number $M$ such that
 $$
 \left| ab(a^2 - b^2) + bc(b^2 - c^2) + ca(c^2 - a^2) \right|
diff --git a/archive/imo/imo2006_q5.lean b/archive/imo/imo2006_q5.lean
index 682b1994adb37..ec9929b2d4c1c 100644
--- a/archive/imo/imo2006_q5.lean
+++ b/archive/imo/imo2006_q5.lean
@@ -10,6 +10,9 @@ import dynamics.periodic_pts
 /-!
 # IMO 2006 Q5
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let $P(x)$ be a polynomial of degree $n>1$ with integer coefficients, and let $k$ be a positive
 integer. Consider the polynomial $Q(x) = P(P(\ldots P(P(x))\ldots))$, where $P$ occurs $k$ times.
 Prove that there are at most $n$ integers $t$ such that $Q(t)=t$.
diff --git a/archive/imo/imo2008_q2.lean b/archive/imo/imo2008_q2.lean
index eb4df1664207b..43c6b652cb127 100644
--- a/archive/imo/imo2008_q2.lean
+++ b/archive/imo/imo2008_q2.lean
@@ -8,6 +8,9 @@ import data.set.finite
 
 /-!
 # IMO 2008 Q2
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 (a) Prove that
           ```
           x^2 / (x-1)^2 + y^2 / (y-1)^2 + z^2 / (z-1)^2 ≥ 1
diff --git a/archive/imo/imo2008_q3.lean b/archive/imo/imo2008_q3.lean
index 16a937f43fce5..ce1470e753e1b 100644
--- a/archive/imo/imo2008_q3.lean
+++ b/archive/imo/imo2008_q3.lean
@@ -12,6 +12,9 @@ import tactic.linear_combination
 
 /-!
 # IMO 2008 Q3
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Prove that there exist infinitely many positive integers `n` such that `n^2 + 1` has a prime
 divisor which is greater than `2n + √(2n)`.
 
diff --git a/archive/imo/imo2008_q4.lean b/archive/imo/imo2008_q4.lean
index 70339914ed2d3..c1cae17f559fa 100644
--- a/archive/imo/imo2008_q4.lean
+++ b/archive/imo/imo2008_q4.lean
@@ -10,6 +10,9 @@ import tactic.linear_combination
 
 /-!
 # IMO 2008 Q4
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Find all functions `f : (0,∞) → (0,∞)` (so, `f` is a function from the positive real
 numbers to the positive real numbers) such that
       ```
diff --git a/archive/imo/imo2011_q3.lean b/archive/imo/imo2011_q3.lean
index c3e5dfc5d8361..67b4845b53018 100644
--- a/archive/imo/imo2011_q3.lean
+++ b/archive/imo/imo2011_q3.lean
@@ -9,6 +9,9 @@ import data.real.basic
 /-!
 # IMO 2011 Q3
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let f : ℝ → ℝ be a function that satisfies
 
    f(x + y) ≤ y * f(x) + f(f(x))
diff --git a/archive/imo/imo2011_q5.lean b/archive/imo/imo2011_q5.lean
index abf6897ad352d..5bb51b977d729 100644
--- a/archive/imo/imo2011_q5.lean
+++ b/archive/imo/imo2011_q5.lean
@@ -8,6 +8,9 @@ import data.int.dvd.basic
 /-!
 # IMO 2011 Q5
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `f` be a function from the set of integers to the set
 of positive integers.  Suppose that, for any two integers
 `m` and `n`, the difference `f(m) - f(n)` is divisible by
diff --git a/archive/imo/imo2013_q1.lean b/archive/imo/imo2013_q1.lean
index cf7c03ce84b00..842d2de4c36f5 100644
--- a/archive/imo/imo2013_q1.lean
+++ b/archive/imo/imo2013_q1.lean
@@ -13,6 +13,9 @@ import tactic.field_simp
 /-!
 # IMO 2013 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Prove that for any pair of positive integers k and n, there exist k positive integers
 m₁, m₂, ..., mₖ (not necessarily different) such that
 
diff --git a/archive/imo/imo2013_q5.lean b/archive/imo/imo2013_q5.lean
index d30c32da64014..16f7cdf6c6ab6 100644
--- a/archive/imo/imo2013_q5.lean
+++ b/archive/imo/imo2013_q5.lean
@@ -12,6 +12,9 @@ import tactic.positivity
 /-!
 # IMO 2013 Q5
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `ℚ>₀` be the positive rational numbers. Let `f : ℚ>₀ → ℝ` be a function satisfying
 the conditions
 
diff --git a/archive/imo/imo2019_q1.lean b/archive/imo/imo2019_q1.lean
index 4e4772456a2ee..0226474656c48 100644
--- a/archive/imo/imo2019_q1.lean
+++ b/archive/imo/imo2019_q1.lean
@@ -8,6 +8,9 @@ import tactic.linarith
 /-!
 # IMO 2019 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Determine all functions `f : ℤ → ℤ` such that, for all integers `a` and `b`,
 `f(2a) + 2f(b) = f(f(a+b))`.
 
diff --git a/archive/imo/imo2019_q2.lean b/archive/imo/imo2019_q2.lean
index 7be26dade77e2..b93b1046604ed 100644
--- a/archive/imo/imo2019_q2.lean
+++ b/archive/imo/imo2019_q2.lean
@@ -9,6 +9,9 @@ import geometry.euclidean.sphere.second_inter
 /-!
 # IMO 2019 Q2
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In triangle `ABC`, point `A₁` lies on side `BC` and point `B₁` lies on side `AC`. Let `P` and
 `Q` be points on segments `AA₁` and `BB₁`, respectively, such that `PQ` is parallel to `AB`.
 Let `P₁` be a point on line `PB₁`, such that `B₁` lies strictly between `P` and `P₁`, and
diff --git a/archive/imo/imo2019_q4.lean b/archive/imo/imo2019_q4.lean
index 3465674493c60..05af48d4acb6e 100644
--- a/archive/imo/imo2019_q4.lean
+++ b/archive/imo/imo2019_q4.lean
@@ -10,6 +10,9 @@ import data.nat.multiplicity
 /-!
 # IMO 2019 Q4
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Find all pairs `(k, n)` of positive integers such that
 ```
   k! = (2 ^ n - 1)(2 ^ n - 2)(2 ^ n - 4)···(2 ^ n - 2 ^ (n - 1))
diff --git a/archive/imo/imo2020_q2.lean b/archive/imo/imo2020_q2.lean
index beea58a78ff17..54938a0afb1ec 100644
--- a/archive/imo/imo2020_q2.lean
+++ b/archive/imo/imo2020_q2.lean
@@ -9,6 +9,9 @@ import analysis.mean_inequalities
 /-!
 # IMO 2020 Q2
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The real numbers `a`, `b`, `c`, `d` are such that `a ≥ b ≥ c ≥ d > 0` and `a + b + c + d = 1`.
 Prove that `(a + 2b + 3c + 4d) a^a b^b c^c d^d < 1`.
 
diff --git a/archive/imo/imo2021_q1.lean b/archive/imo/imo2021_q1.lean
index 85abc0654bd36..397823fa856e1 100644
--- a/archive/imo/imo2021_q1.lean
+++ b/archive/imo/imo2021_q1.lean
@@ -14,6 +14,9 @@ import tactic.ring_exp
 /-!
 # IMO 2021 Q1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `n≥100` be an integer. Ivan writes the numbers `n, n+1,..., 2n` each on different cards.
 He then shuffles these `n+1` cards, and divides them into two piles. Prove that at least one
 of the piles contains two cards such that the sum of their numbers is a perfect square.
diff --git a/archive/miu_language/basic.lean b/archive/miu_language/basic.lean
index f4ca4329c312d..ad139d96ffe3b 100644
--- a/archive/miu_language/basic.lean
+++ b/archive/miu_language/basic.lean
@@ -8,6 +8,9 @@ import tactic.linarith
 /-!
 # An MIU Decision Procedure in Lean
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The [MIU formal system](https://en.wikipedia.org/wiki/MU_puzzle) was introduced by Douglas
 Hofstadter in the first chapter of his 1979 book,
 [Gödel, Escher, Bach](https://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach).
diff --git a/archive/miu_language/decision_nec.lean b/archive/miu_language/decision_nec.lean
index d70116a20b054..c6c5b287d1d28 100644
--- a/archive/miu_language/decision_nec.lean
+++ b/archive/miu_language/decision_nec.lean
@@ -11,6 +11,9 @@ import tactic.ring
 /-!
 # Decision procedure: necessary condition
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We introduce a condition `decstr` and show that if a string `en` is `derivable`, then `decstr en`
 holds.
 
diff --git a/archive/miu_language/decision_suf.lean b/archive/miu_language/decision_suf.lean
index 257bea77baa2e..8625a706de47b 100644
--- a/archive/miu_language/decision_suf.lean
+++ b/archive/miu_language/decision_suf.lean
@@ -9,6 +9,9 @@ import tactic.linarith
 /-!
 # Decision procedure - sufficient condition and decidability
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We give a sufficient condition for a string to be derivable in the MIU language. Together with the
 necessary condition, we use this to prove that `derivable` is an instance of `decidable_pred`.
 
diff --git a/archive/oxford_invariants/2021summer/week3_p1.lean b/archive/oxford_invariants/2021summer/week3_p1.lean
index eb30161c3a81c..cf1d4fe0e3ed0 100644
--- a/archive/oxford_invariants/2021summer/week3_p1.lean
+++ b/archive/oxford_invariants/2021summer/week3_p1.lean
@@ -11,6 +11,9 @@ import data.rat.cast
 /-!
 # The Oxford Invariants Puzzle Challenges - Summer 2021, Week 3, Problem 1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Original statement
 
 Let `n ≥ 3`, `a₁, ..., aₙ` be strictly positive integers such that `aᵢ ∣ aᵢ₋₁ + aᵢ₊₁` for
diff --git a/archive/sensitivity.lean b/archive/sensitivity.lean
index 995ff612ae9c3..1bd54993a14c4 100644
--- a/archive/sensitivity.lean
+++ b/archive/sensitivity.lean
@@ -15,6 +15,9 @@ import data.real.sqrt
 /-!
 # Huang's sensitivity theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A formalization of Hao Huang's sensitivity theorem: in the hypercube of
 dimension n ≥ 1, if one colors more than half the vertices then at least one
 vertex has at least √n colored neighbors.
diff --git a/archive/wiedijk_100_theorems/abel_ruffini.lean b/archive/wiedijk_100_theorems/abel_ruffini.lean
index 02b6bb4a7d250..16e3595a8dbf8 100644
--- a/archive/wiedijk_100_theorems/abel_ruffini.lean
+++ b/archive/wiedijk_100_theorems/abel_ruffini.lean
@@ -12,6 +12,9 @@ import ring_theory.eisenstein_criterion
 /-!
 # Construction of an algebraic number that is not solvable by radicals.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The main ingredients are:
  * `solvable_by_rad.is_solvable'` in `field_theory/abel_ruffini` :
   an irreducible polynomial with an `is_solvable_by_rad` root has solvable Galois group
diff --git a/archive/wiedijk_100_theorems/area_of_a_circle.lean b/archive/wiedijk_100_theorems/area_of_a_circle.lean
index e3c8d7a0daf6f..e22a6274e698f 100644
--- a/archive/wiedijk_100_theorems/area_of_a_circle.lean
+++ b/archive/wiedijk_100_theorems/area_of_a_circle.lean
@@ -11,6 +11,9 @@ import measure_theory.measure.lebesgue.integral
 /-!
 # Freek № 9: The Area of a Circle
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we show that the area of a disc with nonnegative radius `r` is `π * r^2`. The main
 tools our proof uses are `volume_region_between_eq_integral`, which allows us to represent the area
 of the disc as an integral, and `interval_integral.integral_eq_sub_of_has_deriv_at'_of_le`, the
diff --git a/archive/wiedijk_100_theorems/ascending_descending_sequences.lean b/archive/wiedijk_100_theorems/ascending_descending_sequences.lean
index a0d947a8089a5..14232f57243c4 100644
--- a/archive/wiedijk_100_theorems/ascending_descending_sequences.lean
+++ b/archive/wiedijk_100_theorems/ascending_descending_sequences.lean
@@ -8,6 +8,9 @@ import data.fintype.powerset
 /-!
 # Erdős–Szekeres theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves Theorem 73 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/), also
 known as the Erdős–Szekeres theorem: given a sequence of more than `r * s` distinct
 values, there is an increasing sequence of length longer than `r` or a decreasing sequence of length
diff --git a/archive/wiedijk_100_theorems/ballot_problem.lean b/archive/wiedijk_100_theorems/ballot_problem.lean
index a72c2e62f322e..f539b407b87e4 100644
--- a/archive/wiedijk_100_theorems/ballot_problem.lean
+++ b/archive/wiedijk_100_theorems/ballot_problem.lean
@@ -8,6 +8,9 @@ import probability.cond_count
 /-!
 # Ballot problem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves Theorem 30 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/).
 
 The ballot problem asks, if in an election, candidate A receives `p` votes whereas candidate B
diff --git a/archive/wiedijk_100_theorems/birthday_problem.lean b/archive/wiedijk_100_theorems/birthday_problem.lean
index d4544a61f7f70..4c0ee761bc19f 100644
--- a/archive/wiedijk_100_theorems/birthday_problem.lean
+++ b/archive/wiedijk_100_theorems/birthday_problem.lean
@@ -10,6 +10,9 @@ import probability.notation
 /-!
 # Birthday Problem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves Theorem 93 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/).
 
 As opposed to the standard probabilistic statement, we instead state the birthday problem
diff --git a/archive/wiedijk_100_theorems/cubing_a_cube.lean b/archive/wiedijk_100_theorems/cubing_a_cube.lean
index ab4b567df3ac4..f26ce9402eb3d 100644
--- a/archive/wiedijk_100_theorems/cubing_a_cube.lean
+++ b/archive/wiedijk_100_theorems/cubing_a_cube.lean
@@ -8,6 +8,9 @@ import data.set.finite
 import data.set.intervals.disjoint
 
 /-!
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Proof that a cube (in dimension n ≥ 3) cannot be cubed:
 There does not exist a partition of a cube into finitely many smaller cubes (at least two)
 of different sizes.
diff --git a/archive/wiedijk_100_theorems/friendship_graphs.lean b/archive/wiedijk_100_theorems/friendship_graphs.lean
index adf5f345655a9..222ca67a633ba 100644
--- a/archive/wiedijk_100_theorems/friendship_graphs.lean
+++ b/archive/wiedijk_100_theorems/friendship_graphs.lean
@@ -12,6 +12,9 @@ import tactic.interval_cases
 /-!
 # The Friendship Theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Definitions and Statement
 - A `friendship` graph is one in which any two distinct vertices have exactly one neighbor in common
 - A `politician`, at least in the context of this problem, is a vertex in a graph which is adjacent
diff --git a/archive/wiedijk_100_theorems/herons_formula.lean b/archive/wiedijk_100_theorems/herons_formula.lean
index 100102469b88c..0fb04262d0fe8 100644
--- a/archive/wiedijk_100_theorems/herons_formula.lean
+++ b/archive/wiedijk_100_theorems/herons_formula.lean
@@ -8,6 +8,9 @@ import geometry.euclidean.triangle
 /-!
 # Freek № 57: Heron's Formula
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves Theorem 57 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/),
 also known as Heron's formula, which gives the area of a triangle based only on its three sides'
 lengths.
diff --git a/archive/wiedijk_100_theorems/inverse_triangle_sum.lean b/archive/wiedijk_100_theorems/inverse_triangle_sum.lean
index 0b12999fbf3d8..b2a77cc1c4be9 100644
--- a/archive/wiedijk_100_theorems/inverse_triangle_sum.lean
+++ b/archive/wiedijk_100_theorems/inverse_triangle_sum.lean
@@ -9,6 +9,9 @@ import data.real.basic
 /-!
 # Sum of the Reciprocals of the Triangular Numbers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves Theorem 42 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/).
 
 We interpret “triangular numbers” as naturals of the form $\frac{k(k+1)}{2}$ for natural `k`.
diff --git a/archive/wiedijk_100_theorems/konigsberg.lean b/archive/wiedijk_100_theorems/konigsberg.lean
index 683d7314664db..fe5abdbe02a38 100644
--- a/archive/wiedijk_100_theorems/konigsberg.lean
+++ b/archive/wiedijk_100_theorems/konigsberg.lean
@@ -9,6 +9,9 @@ import tactic.derive_fintype
 /-!
 # The Königsberg bridges problem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We show that a graph that represents the islands and mainlands of Königsberg and seven bridges
 between them has no Eulerian trail.
 -/
diff --git a/archive/wiedijk_100_theorems/partition.lean b/archive/wiedijk_100_theorems/partition.lean
index 8796e3b3c2a4d..ac3d5f6c41d05 100644
--- a/archive/wiedijk_100_theorems/partition.lean
+++ b/archive/wiedijk_100_theorems/partition.lean
@@ -15,6 +15,9 @@ import tactic.congrm
 /-!
 # Euler's Partition Theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves Theorem 45 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/).
 
 The theorem concerns the counting of integer partitions -- ways of
diff --git a/archive/wiedijk_100_theorems/perfect_numbers.lean b/archive/wiedijk_100_theorems/perfect_numbers.lean
index 7d1cbd45655a7..191b9bd62c36e 100644
--- a/archive/wiedijk_100_theorems/perfect_numbers.lean
+++ b/archive/wiedijk_100_theorems/perfect_numbers.lean
@@ -12,6 +12,9 @@ import ring_theory.multiplicity
 /-!
 # Perfect Numbers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves Theorem 70 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/).
 
 The theorem characterizes even perfect numbers.
diff --git a/archive/wiedijk_100_theorems/solution_of_cubic.lean b/archive/wiedijk_100_theorems/solution_of_cubic.lean
index 95b58db873e73..57e17a74e712f 100644
--- a/archive/wiedijk_100_theorems/solution_of_cubic.lean
+++ b/archive/wiedijk_100_theorems/solution_of_cubic.lean
@@ -9,6 +9,9 @@ import ring_theory.polynomial.cyclotomic.roots
 /-!
 # The Solution of a Cubic
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves Theorem 37 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/).
 
 In this file, we give the solutions to the cubic equation `a * x^3 + b * x^2 + c * x + d = 0`
diff --git a/archive/wiedijk_100_theorems/sum_of_prime_reciprocals_diverges.lean b/archive/wiedijk_100_theorems/sum_of_prime_reciprocals_diverges.lean
index 062c3d870d2d6..f52c458f2a87a 100644
--- a/archive/wiedijk_100_theorems/sum_of_prime_reciprocals_diverges.lean
+++ b/archive/wiedijk_100_theorems/sum_of_prime_reciprocals_diverges.lean
@@ -9,6 +9,9 @@ import data.nat.squarefree
 /-!
 # Divergence of the Prime Reciprocal Series
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves Theorem 81 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/).
 The theorem states that the sum of the reciprocals of all prime numbers diverges.
 The formalization follows Erdős's proof by upper and lower estimates.
diff --git a/counterexamples/canonically_ordered_comm_semiring_two_mul.lean b/counterexamples/canonically_ordered_comm_semiring_two_mul.lean
index 012d49af2dcee..624471d03aeb5 100644
--- a/counterexamples/canonically_ordered_comm_semiring_two_mul.lean
+++ b/counterexamples/canonically_ordered_comm_semiring_two_mul.lean
@@ -21,6 +21,9 @@ multiplication cannot be strengthened to **strict** monotonicity.
 
 Reference:
 https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/canonically_ordered.20pathology
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 namespace counterexample
diff --git a/counterexamples/char_p_zero_ne_char_zero.lean b/counterexamples/char_p_zero_ne_char_zero.lean
index a6b9cecde95cc..a567d155f59ec 100644
--- a/counterexamples/char_p_zero_ne_char_zero.lean
+++ b/counterexamples/char_p_zero_ne_char_zero.lean
@@ -7,6 +7,9 @@ import algebra.char_p.basic
 
 /-! # `char_p R 0` and `char_zero R` need not coincide for semirings
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 For rings, the two notions coincide.
 
 In fact, `char_p.of_char_zero` shows that `char_zero R` implies `char_p R 0` for any `char_zero`
diff --git a/counterexamples/cyclotomic_105.lean b/counterexamples/cyclotomic_105.lean
index cfbb5aa23bb94..9499e39f118ac 100644
--- a/counterexamples/cyclotomic_105.lean
+++ b/counterexamples/cyclotomic_105.lean
@@ -9,6 +9,9 @@ import ring_theory.polynomial.cyclotomic.basic
 /-!
 # Not all coefficients of cyclotomic polynomials are -1, 0, or 1
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We show that not all coefficients of cyclotomic polynomials are equal to `0`, `-1` or `1`, in the
 theorem `not_forall_coeff_cyclotomic_neg_one_zero_one`. We prove this with the counterexample
 `coeff_cyclotomic_105 : coeff (cyclotomic 105 ℤ) 7 = -2`.
diff --git a/counterexamples/direct_sum_is_internal.lean b/counterexamples/direct_sum_is_internal.lean
index 9a4b75ece1807..08d293d5e7eb4 100644
--- a/counterexamples/direct_sum_is_internal.lean
+++ b/counterexamples/direct_sum_is_internal.lean
@@ -11,6 +11,9 @@ import tactic.fin_cases
 /-!
 # Not all complementary decompositions of a module over a semiring make up a direct sum
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This shows that while `ℤ≤0` and `ℤ≥0` are complementary `ℕ`-submodules of `ℤ`, which in turn
 implies as a collection they are `complete_lattice.independent` and that they span all of `ℤ`, they
 do not form a decomposition into a direct sum.
diff --git a/counterexamples/girard.lean b/counterexamples/girard.lean
index 090551161b38a..de764493e7027 100644
--- a/counterexamples/girard.lean
+++ b/counterexamples/girard.lean
@@ -8,6 +8,9 @@ import logic.basic
 /-!
 # Girard's paradox
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Girard's paradox is a proof that `Type : Type` entails a contradiction. We can't say this directly
 in Lean because `Type : Type 1` and it's not possible to give `Type` a different type via an axiom,
 so instead we axiomatize the behavior of the Pi type and application if the typing rule for Pi was
diff --git a/counterexamples/homogeneous_prime_not_prime.lean b/counterexamples/homogeneous_prime_not_prime.lean
index 1e895db644e53..41e0b98c88cdc 100644
--- a/counterexamples/homogeneous_prime_not_prime.lean
+++ b/counterexamples/homogeneous_prime_not_prime.lean
@@ -10,6 +10,9 @@ import tactic.derive_fintype
 /-!
 # A homogeneous prime that is homogeneously prime but not prime
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In `src/ring_theory/graded_algebra/radical.lean`,  we assumed that the underline grading is indexed
 by a `linear_ordered_cancel_add_comm_monoid` to prove that a homogeneous ideal is prime if and only
 if it is homogeneously prime. This file is aimed to show that even if this assumption isn't strictly
diff --git a/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean b/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean
index 0fac502d4e5e3..b83f9dca5525b 100644
--- a/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean
+++ b/counterexamples/linear_order_with_pos_mul_pos_eq_zero.lean
@@ -16,6 +16,9 @@ The order is `0 < ε < 1`.  Since `ε ^ 2 = 0`, the product of strictly positive
 
 Relevant Zulip chat:
 https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/mul_pos
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 namespace counterexample
diff --git a/counterexamples/map_floor.lean b/counterexamples/map_floor.lean
index 2fd1b31c7cedc..105a24f6e9574 100644
--- a/counterexamples/map_floor.lean
+++ b/counterexamples/map_floor.lean
@@ -9,6 +9,9 @@ import data.polynomial.reverse
 /-!
 # Floors and ceils aren't preserved under ordered ring homomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Intuitively, if `f : α → β` is an ordered ring homomorphism, then floors and ceils should be
 preserved by `f` because:
 * `f` preserves the naturals/integers in `α` and `β` because it's a ring hom.
diff --git a/counterexamples/phillips.lean b/counterexamples/phillips.lean
index eafafd6d169bd..9ef4b12c2300f 100644
--- a/counterexamples/phillips.lean
+++ b/counterexamples/phillips.lean
@@ -11,6 +11,9 @@ import topology.continuous_function.bounded
 /-!
 # A counterexample on Pettis integrability
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 There are several theories of integration for functions taking values in Banach spaces. Bochner
 integration, requiring approximation by simple functions, is the analogue of the one-dimensional
 theory. It is very well behaved, but only works for functions with second-countable range.
diff --git a/counterexamples/pseudoelement.lean b/counterexamples/pseudoelement.lean
index 0e2ddaf8cc23b..a05f885f332ae 100644
--- a/counterexamples/pseudoelement.lean
+++ b/counterexamples/pseudoelement.lean
@@ -9,6 +9,9 @@ import algebra.category.Module.biproducts
 
 /-!
 # Pseudoelements and pullbacks
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 Borceux claims in Proposition 1.9.5 that the pseudoelement constructed in
 `category_theory.abelian.pseudoelement.pseudo_pullback` is unique. We show here that this claim is
 false. This means in particular that we cannot have an extensionality principle for pullbacks in
diff --git a/counterexamples/quadratic_form.lean b/counterexamples/quadratic_form.lean
index d9f029822dce1..50214d8f685dd 100644
--- a/counterexamples/quadratic_form.lean
+++ b/counterexamples/quadratic_form.lean
@@ -10,6 +10,9 @@ import data.zmod.basic
 /-!
 # `quadratic_form R M` and `subtype bilin_form.is_symm` are distinct notions in characteristic 2
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The main result of this file is `bilin_form.not_inj_on_to_quadratic_form_is_symm`.
 
 The counterexample we use is $B (x, y) (x', y') ↦ xy' + x'y$ where `x y x' y' : zmod 2`.
diff --git a/counterexamples/seminorm_lattice_not_distrib.lean b/counterexamples/seminorm_lattice_not_distrib.lean
index 95b4e997ea397..ca9b74e8f6934 100644
--- a/counterexamples/seminorm_lattice_not_distrib.lean
+++ b/counterexamples/seminorm_lattice_not_distrib.lean
@@ -7,6 +7,9 @@ import analysis.seminorm
 /-!
 # The lattice of seminorms is not distributive
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We provide an example of three seminorms over the ℝ-vector space ℝ×ℝ which don't satisfy the lattice
 distributivity property `(p ⊔ q1) ⊓ (p ⊔ q2) ≤ p ⊔ (q1 ⊓ q2)`.
 
diff --git a/counterexamples/sorgenfrey_line.lean b/counterexamples/sorgenfrey_line.lean
index 065ecbecd57b5..ac740f1bb34da 100644
--- a/counterexamples/sorgenfrey_line.lean
+++ b/counterexamples/sorgenfrey_line.lean
@@ -13,6 +13,9 @@ import data.set.intervals.monotone
 /-!
 # Sorgenfrey line
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `sorgenfrey_line` (notation: `ℝₗ`) to be the Sorgenfrey line. It is the real
 line with the topology space structure generated by half-open intervals `set.Ico a b`.
 
diff --git a/counterexamples/zero_divisors_in_add_monoid_algebras.lean b/counterexamples/zero_divisors_in_add_monoid_algebras.lean
index 88e430e411b30..8b52293f1958d 100644
--- a/counterexamples/zero_divisors_in_add_monoid_algebras.lean
+++ b/counterexamples/zero_divisors_in_add_monoid_algebras.lean
@@ -12,6 +12,9 @@ import data.zmod.basic
 /-!
 # Examples of zero-divisors in `add_monoid_algebra`s
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains an easy source of zero-divisors in an `add_monoid_algebra`.
 If `k` is a field and `G` is an additive group containing a non-zero torsion element, then
 `add_monoid_algebra k G` contains non-zero zero-divisors: this is lemma `zero_divisors_of_torsion`.
diff --git a/src/algebra/expr.lean b/src/algebra/expr.lean
index 7c6a862f0abfc..89641583e33bd 100644
--- a/src/algebra/expr.lean
+++ b/src/algebra/expr.lean
@@ -7,6 +7,9 @@ import tactic.core
 
 /-! ### Helpers to invoke functions involving algebra at tactic time
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 It's not clear whether using `instance_cache` is a sensible choice here.
 In particular, we need to use these tactics below when the algebraic instances are local variables
 that aren't in the "real" instance cache (the one used by `tactic.reset_instance_cache`).
diff --git a/src/algebraic_geometry/morphisms/finite_type.lean b/src/algebraic_geometry/morphisms/finite_type.lean
index 65ab36ddc83ec..ce417476ad834 100644
--- a/src/algebraic_geometry/morphisms/finite_type.lean
+++ b/src/algebraic_geometry/morphisms/finite_type.lean
@@ -9,6 +9,9 @@ import ring_theory.ring_hom.finite_type
 /-!
 # Morphisms of finite type
 
+> 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 locally of finite type if for each affine `U ⊆ Y` and
 `V ⊆ f ⁻¹' U`, The induced map `Γ(Y, U) ⟶ Γ(X, V)` is of finite type.
 
diff --git a/src/algebraic_geometry/morphisms/ring_hom_properties.lean b/src/algebraic_geometry/morphisms/ring_hom_properties.lean
index e389bdb008d2d..d30f2f44c77ec 100644
--- a/src/algebraic_geometry/morphisms/ring_hom_properties.lean
+++ b/src/algebraic_geometry/morphisms/ring_hom_properties.lean
@@ -10,6 +10,9 @@ import ring_theory.local_properties
 
 # Properties of morphisms from properties of ring homs.
 
+> 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 that come from properties
 of ring homs. For `P` a property of ring homs, we have two ways of defining a property of scheme
 morphisms:
diff --git a/src/data/matrix/auto.lean b/src/data/matrix/auto.lean
index 1a351ef13828c..0d75a92737462 100644
--- a/src/data/matrix/auto.lean
+++ b/src/data/matrix/auto.lean
@@ -8,6 +8,9 @@ import data.matrix.reflection
 
 /-! # Automatically generated lemmas for working with concrete matrices
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains "magic" lemmas which autogenerate to the correct size of matrix. For instance,
 `matrix.of_mul_of_fin` can be used as:
 ```lean
diff --git a/src/geometry/manifold/instances/sphere.lean b/src/geometry/manifold/instances/sphere.lean
index e274632af5e28..71158b59e4aa9 100644
--- a/src/geometry/manifold/instances/sphere.lean
+++ b/src/geometry/manifold/instances/sphere.lean
@@ -15,6 +15,9 @@ import geometry.manifold.cont_mdiff_mfderiv
 /-!
 # Manifold structure on the sphere
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines stereographic projection from the sphere in an inner product space `E`, and uses
 it to put a smooth manifold structure on the sphere.