chore(*): add mathlib4 synchronization comments (#17943)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.euclidean_domain.basic`: https://github.com/leanprover-community/mathlib4/pull/919
* `algebra.field.basic`: https://github.com/leanprover-community/mathlib4/pull/975
* `algebra.group.opposite`: https://github.com/leanprover-community/mathlib4/pull/912
* `algebra.group.prod`: https://github.com/leanprover-community/mathlib4/pull/968
* `algebra.group.with_one.units`: https://github.com/leanprover-community/mathlib4/pull/955
* `algebra.group_power.ring`: https://github.com/leanprover-community/mathlib4/pull/979
* `algebra.hom.equiv.type_tags`: https://github.com/leanprover-community/mathlib4/pull/943
* `algebra.hom.ring`: https://github.com/leanprover-community/mathlib4/pull/958
* `algebra.invertible`: https://github.com/leanprover-community/mathlib4/pull/930
* `algebra.order.field.canonical.basic`: https://github.com/leanprover-community/mathlib4/pull/1018
* `algebra.order.field.canonical.defs`: https://github.com/leanprover-community/mathlib4/pull/985
* `algebra.order.field.inj_surj`: https://github.com/leanprover-community/mathlib4/pull/1017
* `algebra.order.group.densely_ordered`: https://github.com/leanprover-community/mathlib4/pull/956
* `algebra.order.group.min_max`: https://github.com/leanprover-community/mathlib4/pull/933
* `algebra.order.group.prod`: https://github.com/leanprover-community/mathlib4/pull/1026
* `algebra.order.group.with_top`: https://github.com/leanprover-community/mathlib4/pull/946
* `algebra.order.hom.monoid`: https://github.com/leanprover-community/mathlib4/pull/944
* `algebra.order.monoid.prod`: https://github.com/leanprover-community/mathlib4/pull/987
* `algebra.order.monoid.to_mul_bot`: https://github.com/leanprover-community/mathlib4/pull/1024
* `algebra.order.ring.abs`: https://github.com/leanprover-community/mathlib4/pull/929
* `algebra.order.ring.cone`: https://github.com/leanprover-community/mathlib4/pull/935
* `algebra.order.sub.basic`: https://github.com/leanprover-community/mathlib4/pull/936
* `algebra.order.sub.with_top`: https://github.com/leanprover-community/mathlib4/pull/932
* `algebra.order.with_zero`: https://github.com/leanprover-community/mathlib4/pull/903
* `combinatorics.quiver.arborescence`: https://github.com/leanprover-community/mathlib4/pull/997
* `combinatorics.quiver.cast`: https://github.com/leanprover-community/mathlib4/pull/990
* `control.traversable.lemmas`: https://github.com/leanprover-community/mathlib4/pull/948
* `data.bool.set`: https://github.com/leanprover-community/mathlib4/pull/960
* `data.int.cast.field`: https://github.com/leanprover-community/mathlib4/pull/1016
* `data.int.cast.lemmas`: https://github.com/leanprover-community/mathlib4/pull/995
* `data.int.cast.prod`: https://github.com/leanprover-community/mathlib4/pull/1015
* `data.int.div`: https://github.com/leanprover-community/mathlib4/pull/1011
* `data.int.dvd.basic`: https://github.com/leanprover-community/mathlib4/pull/996
* `data.int.order.basic`: https://github.com/leanprover-community/mathlib4/pull/938
* `data.nat.cast.basic`: https://github.com/leanprover-community/mathlib4/pull/980
* `data.nat.cast.prod`: https://github.com/leanprover-community/mathlib4/pull/1010
* `data.nat.cast.with_top`: https://github.com/leanprover-community/mathlib4/pull/1019
* `data.nat.gcd.basic`: https://github.com/leanprover-community/mathlib4/pull/965
* `data.nat.order.basic`: https://github.com/leanprover-community/mathlib4/pull/907
* `data.nat.order.lemmas`: https://github.com/leanprover-community/mathlib4/pull/927
* `data.nat.set`: https://github.com/leanprover-community/mathlib4/pull/961
* `data.nat.upto`: https://github.com/leanprover-community/mathlib4/pull/1020
* `data.pequiv`: https://github.com/leanprover-community/mathlib4/pull/1008
* `data.set.basic`: https://github.com/leanprover-community/mathlib4/pull/892
* `data.set.bool_indicator`: https://github.com/leanprover-community/mathlib4/pull/988
* `data.set.image`: https://github.com/leanprover-community/mathlib4/pull/949
* `data.set.n_ary`: https://github.com/leanprover-community/mathlib4/pull/969
* `data.set.opposite`: https://github.com/leanprover-community/mathlib4/pull/983
* `data.set.prod`: https://github.com/leanprover-community/mathlib4/pull/1004
* `data.set.sigma`: https://github.com/leanprover-community/mathlib4/pull/982
* `data.set_like.basic`: https://github.com/leanprover-community/mathlib4/pull/993
* `data.two_pointing`: https://github.com/leanprover-community/mathlib4/pull/984
* `logic.embedding.set`: https://github.com/leanprover-community/mathlib4/pull/986
* `logic.equiv.embedding`: https://github.com/leanprover-community/mathlib4/pull/1021
* `order.directed`: https://github.com/leanprover-community/mathlib4/pull/963
* `order.rel_iso.set`: https://github.com/leanprover-community/mathlib4/pull/1005
* `order.well_founded`: https://github.com/leanprover-community/mathlib4/pull/970
* `ring_theory.coprime.basic`: https://github.com/leanprover-community/mathlib4/pull/899
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
