chore(*): add mathlib4 synchronization comments (#17979)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.associated`
* `algebra.char_zero.lemmas`
* `algebra.euclidean_domain.instances`
* `algebra.field.opposite`
* `algebra.field.power`
* `algebra.group.conj`
* `algebra.group.pi`
* `algebra.group_power.lemmas`
* `algebra.group_power.order`
* `algebra.group_ring_action.basic`
* `algebra.group_with_zero.power`
* `algebra.hom.aut`
* `algebra.hom.group_instances`
* `algebra.hom.iterate`
* `algebra.module.basic`
* `algebra.module.prod`
* `algebra.order.absolute_value`
* `algebra.order.euclidean_absolute_value`
* `algebra.order.field.basic`
* `algebra.order.field.power`
* `algebra.order.group.bounds`
* `algebra.order.invertible`
* `algebra.order.pi`
* `algebra.order.positive.field`
* `algebra.parity`
* `algebra.regular.pow`
* `algebra.regular.smul`
* `algebra.ring.add_aut`
* `algebra.ring.aut`
* `algebra.ring.comp_typeclasses`
* `algebra.ring.equiv`
* `algebra.ring.opposite`
* `algebra.ring.pi`
* `algebra.ring.prod`
* `algebra.ring.ulift`
* `algebra.smul_with_zero`
* `category_theory.category.Kleisli`
* `category_theory.essential_image`
* `category_theory.full_subcategory`
* `category_theory.functor.fully_faithful`
* `category_theory.whiskering`
* `combinatorics.quiver.symmetric`
* `control.fix`
* `control.traversable.equiv`
* `data.countable.small`
* `data.erased`
* `data.int.absolute_value`
* `data.int.associated`
* `data.int.bitwise`
* `data.int.char_zero`
* `data.int.conditionally_complete_order`
* `data.int.dvd.pow`
* `data.int.gcd`
* `data.int.least_greatest`
* `data.int.lemmas`
* `data.int.modeq`
* `data.int.nat_prime`
* `data.int.order.lemmas`
* `data.int.order.units`
* `data.int.sqrt`
* `data.list.func`
* `data.nat.bits`
* `data.nat.cast.field`
* `data.nat.choose.basic`
* `data.nat.choose.bounds`
* `data.nat.choose.dvd`
* `data.nat.dist`
* `data.nat.even_odd_rec`
* `data.nat.factorial.basic`
* `data.nat.log`
* `data.nat.modeq`
* `data.nat.pairing`
* `data.nat.pow`
* `data.nat.prime`
* `data.nat.size`
* `data.nat.sqrt`
* `data.nat.with_bot`
* `data.part`
* `data.pi.lex`
* `data.pnat.basic`
* `data.pnat.find`
* `data.rat.basic`
* `data.rat.defs`
* `data.rat.lemmas`
* `data.rat.order`
* `data.rat.sqrt`
* `data.rel`
* `data.semiquot`
* `data.set.Union_lift`
* `data.set.accumulate`
* `data.set.enumerate`
* `data.set.function`
* `data.set.functor`
* `data.set.intervals.basic`
* `data.set.intervals.disjoint`
* `data.set.intervals.group`
* `data.set.intervals.monoid`
* `data.set.intervals.ord_connected`
* `data.set.intervals.order_iso`
* `data.set.intervals.pi`
* `data.set.intervals.proj_Icc`
* `data.set.intervals.surj_on`
* `data.set.intervals.unordered_interval`
* `data.set.intervals.with_bot_top`
* `data.set.lattice`
* `data.set.pairwise`
* `data.setoid.basic`
* `data.stream.init`
* `dynamics.fixed_points.basic`
* `group_theory.group_action.group`
* `group_theory.group_action.opposite`
* `group_theory.group_action.pi`
* `group_theory.group_action.prod`
* `group_theory.perm.basic`
* `group_theory.perm.via_embedding`
* `group_theory.submonoid.basic`
* `group_theory.subsemigroup.basic`
* `group_theory.subsemigroup.center`
* `group_theory.subsemigroup.centralizer`
* `group_theory.subsemigroup.operations`
* `logic.equiv.nat`
* `logic.equiv.set`
* `logic.small.basic`
* `order.antichain`
* `order.atoms`
* `order.bounded`
* `order.bounds.basic`
* `order.bounds.order_iso`
* `order.chain`
* `order.closure`
* `order.complete_boolean_algebra`
* `order.complete_lattice`
* `order.complete_lattice_intervals`
* `order.conditionally_complete_lattice.basic`
* `order.conditionally_complete_lattice.group`
* `order.copy`
* `order.cover`
* `order.fixed_points`
* `order.galois_connection`
* `order.heyting.regular`
* `order.hom.order`
* `order.hom.set`
* `order.initial_seg`
* `order.lattice_intervals`
* `order.modular_lattice`
* `order.monotone.extension`
* `order.monotone.odd`
* `order.monotone.union`
* `order.ord_continuous`
* `order.semiconj_Sup`
* `order.succ_pred.basic`
* `order.succ_pred.interval_succ`
* `order.succ_pred.relation`
* `order.zorn`
* `order.zorn_atoms`
* `ring_theory.ore_localization.ore_set`
* `set_theory.cardinal.schroeder_bernstein`
