chore(*): add mathlib4 synchronization comments (#17838)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.divisibility.units`: https://github.com/leanprover-community/mathlib4/pull/848
* `algebra.group.type_tags`: https://github.com/leanprover-community/mathlib4/pull/832
* `algebra.group_with_zero.divisibility`: https://github.com/leanprover-community/mathlib4/pull/870
* `algebra.hom.equiv.basic`: https://github.com/leanprover-community/mathlib4/pull/835
* `algebra.order.group.defs`: https://github.com/leanprover-community/mathlib4/pull/869
* `algebra.order.monoid.basic`: https://github.com/leanprover-community/mathlib4/pull/872
* `algebra.order.monoid.cancel.basic`: https://github.com/leanprover-community/mathlib4/pull/883
* `algebra.order.monoid.with_zero.defs`: https://github.com/leanprover-community/mathlib4/pull/851
* `algebra.order.monoid.with_zero.basic`: https://github.com/leanprover-community/mathlib4/pull/851
* `algebra.ring.divisibility`: https://github.com/leanprover-community/mathlib4/pull/864
* `data.list.defs`: https://github.com/leanprover-community/mathlib4/pull/803
* `data.sigma.order`: https://github.com/leanprover-community/mathlib4/pull/887
* `group_theory.group_action.defs`: https://github.com/leanprover-community/mathlib4/pull/854
* `order.heyting.boundary`: https://github.com/leanprover-community/mathlib4/pull/844
* `order.hom.basic`: https://github.com/leanprover-community/mathlib4/pull/804
* `order.symm_diff`: https://github.com/leanprover-community/mathlib4/pull/842
Co-authored-by: Johan Commelin <johan@commelin.net>
