chore(*): add mathlib4 synchronization comments (#17849)
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.defs`: https://github.com/leanprover-community/mathlib4/pull/871
* `algebra.group.ext`: https://github.com/leanprover-community/mathlib4/pull/850
* `algebra.group_power.basic`: https://github.com/leanprover-community/mathlib4/pull/874
* `algebra.hom.equiv.units.basic`: https://github.com/leanprover-community/mathlib4/pull/895
* `algebra.hom.equiv.units.group_with_zero`: https://github.com/leanprover-community/mathlib4/pull/901
* `algebra.order.group.instances`: https://github.com/leanprover-community/mathlib4/pull/890
* `algebra.order.group.order_iso`: https://github.com/leanprover-community/mathlib4/pull/895
* `algebra.order.group.units`: https://github.com/leanprover-community/mathlib4/pull/898
* `algebra.order.monoid.nat_cast`: https://github.com/leanprover-community/mathlib4/pull/893
* `algebra.order.monoid.type_tags`: https://github.com/leanprover-community/mathlib4/pull/873
* `algebra.order.monoid.units`: https://github.com/leanprover-community/mathlib4/pull/873
* `algebra.order.zero_le_one`: https://github.com/leanprover-community/mathlib4/pull/893
* `combinatorics.quiver.push`: https://github.com/leanprover-community/mathlib4/pull/868
* `control.traversable.basic`: https://github.com/leanprover-community/mathlib4/pull/788
* `data.sum.order`: https://github.com/leanprover-community/mathlib4/pull/880
* `group_theory.group_action.option`: https://github.com/leanprover-community/mathlib4/pull/884
* `group_theory.group_action.sigma`: https://github.com/leanprover-community/mathlib4/pull/885
* `group_theory.group_action.sum`: https://github.com/leanprover-community/mathlib4/pull/882
* `group_theory.group_action.units`: https://github.com/leanprover-community/mathlib4/pull/878
* `order.antisymmetrization`: https://github.com/leanprover-community/mathlib4/pull/876
