chore(*): add mathlib4 synchronization comments (#17754)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following PRs:
* `algebra.field.defs`: https://github.com/leanprover-community/mathlib4/pull/668
* `algebra.group.commute`: https://github.com/leanprover-community/mathlib4/pull/750
* `algebra.group_with_zero.commute`: https://github.com/leanprover-community/mathlib4/pull/762
* `algebra.group_with_zero.semiconj`: https://github.com/leanprover-community/mathlib4/pull/757
* `algebra.group_with_zero.units.basic`: https://github.com/leanprover-community/mathlib4/pull/735
* `algebra.hom.embedding`: https://github.com/leanprover-community/mathlib4/pull/764
* `algebra.order.monoid.cancel.defs`: https://github.com/leanprover-community/mathlib4/pull/774
* `algebra.order.monoid.canonical.defs`: https://github.com/leanprover-community/mathlib4/pull/778
* `algebra.order.monoid.defs`: https://github.com/leanprover-community/mathlib4/pull/771
* `algebra.order.monoid.min_max`: https://github.com/leanprover-community/mathlib4/pull/763
* `algebra.order.monoid.order_dual`: https://github.com/leanprover-community/mathlib4/pull/786
* `algebra.order.sub.defs`: https://github.com/leanprover-community/mathlib4/pull/732
* `algebra.regular.basic`: https://github.com/leanprover-community/mathlib4/pull/758
* `algebra.ring.commute`: https://github.com/leanprover-community/mathlib4/pull/759
* `algebra.ring.regular`: https://github.com/leanprover-community/mathlib4/pull/795
* `algebra.ring.semiconj`: https://github.com/leanprover-community/mathlib4/pull/751
* `control.applicative`: https://github.com/leanprover-community/mathlib4/pull/798
* `control.functor`: https://github.com/leanprover-community/mathlib4/pull/612
* `control.monad.basic`: https://github.com/leanprover-community/mathlib4/pull/752
* `data.countable.defs`: https://github.com/leanprover-community/mathlib4/pull/736
* `data.int.units`: https://github.com/leanprover-community/mathlib4/pull/807
* `data.nat.basic`: https://github.com/leanprover-community/mathlib4/pull/729
* `data.nat.psub`: https://github.com/leanprover-community/mathlib4/pull/806
* `data.nat.units`: https://github.com/leanprover-community/mathlib4/pull/805
* `data.pi.algebra`: https://github.com/leanprover-community/mathlib4/pull/564
* `data.prod.lex`: https://github.com/leanprover-community/mathlib4/pull/783
* `logic.embedding.basic`: https://github.com/leanprover-community/mathlib4/pull/700
* `logic.equiv.option`: https://github.com/leanprover-community/mathlib4/pull/674
* `order.bounded_order`: https://github.com/leanprover-community/mathlib4/pull/697
* `order.with_bot`: https://github.com/leanprover-community/mathlib4/pull/776
* `order.disjoint`: https://github.com/leanprover-community/mathlib4/pull/773
* `order.min_max`: https://github.com/leanprover-community/mathlib4/pull/728
* `order.prop_instances`: https://github.com/leanprover-community/mathlib4/pull/792
* `order.rel_iso.basic`: https://github.com/leanprover-community/mathlib4/pull/772
