chore(*): add mathlib4 synchronization comments (#18139)

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.free_monoid.count`
* `algebra.order.lattice_group`
* `data.fin.basic`
* `data.int.range`
* `data.list.destutter`
* `data.list.nat_antidiagonal`
* `data.list.perm`
* `data.list.prime`
* `order.circular`

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`.

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.
 

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.
 

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`.
 

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.,

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`.

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.
 

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.
 
 -/

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