chore(*): add mathlib4 synchronization comments (#18546)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.algebra.operations`
* `algebra.algebra.restrict_scalars`
* `algebra.lie.non_unital_non_assoc_algebra`
* `algebra.order.algebra`
* `algebra.star.module`
* `algebra.star.star_alg_hom`
* `category_theory.adjunction.evaluation`
* `category_theory.adjunction.limits`
* `category_theory.category.pairwise`
* `category_theory.concrete_category.basic`
* `category_theory.limits.constructions.binary_products`
* `category_theory.limits.constructions.epi_mono`
* `category_theory.limits.constructions.pullbacks`
* `category_theory.limits.creates`
* `category_theory.limits.exact_functor`
* `category_theory.limits.full_subcategory`
* `category_theory.limits.functor_category`
* `category_theory.limits.preserves.finite`
* `category_theory.limits.preserves.shapes.binary_products`
* `category_theory.limits.preserves.shapes.equalizers`
* `category_theory.limits.preserves.shapes.products`
* `category_theory.limits.preserves.shapes.pullbacks`
* `category_theory.limits.preserves.shapes.terminal`
* `category_theory.limits.shapes.binary_products`
* `category_theory.limits.shapes.disjoint_coproduct`
* `category_theory.limits.shapes.equalizers`
* `category_theory.limits.shapes.equivalence`
* `category_theory.limits.shapes.finite_limits`
* `category_theory.limits.shapes.images`
* `category_theory.limits.shapes.products`
* `category_theory.limits.shapes.pullbacks`
* `category_theory.limits.shapes.regular_mono`
* `category_theory.limits.shapes.split_coequalizer`
* `category_theory.limits.shapes.strict_initial`
* `category_theory.limits.shapes.terminal`
* `category_theory.limits.shapes.zero_objects`
* `category_theory.limits.unit`
* `category_theory.limits.yoneda`
* `category_theory.over`
* `category_theory.path_category`
* `category_theory.quotient`
* `category_theory.sites.sieves`
* `category_theory.structured_arrow`
* `combinatorics.simple_graph.hasse`
* `combinatorics.simple_graph.metric`
* `combinatorics.simple_graph.prod`
* `combinatorics.simple_graph.regularity.energy`
* `combinatorics.simple_graph.trails`
* `control.lawful_fix`
* `group_theory.solvable`
* `linear_algebra.affine_space.affine_map`
* `linear_algebra.dfinsupp`
* `topology.algebra.field`
* `topology.algebra.group_completion`
* `topology.algebra.infinite_sum.basic`
* `topology.algebra.infinite_sum.order`
* `topology.algebra.infinite_sum.real`
* `topology.algebra.infinite_sum.ring`
* `topology.algebra.order.field`
* `topology.algebra.order.upper_lower`
* `topology.algebra.ring.basic`
* `topology.algebra.uniform_mul_action`
* `topology.instances.int`
* `topology.instances.nat`
* `topology.instances.nnreal`
* `topology.instances.rat`
* `topology.instances.real`
* `topology.locally_constant.algebra`
* `topology.metric_space.algebra`
* `topology.metric_space.antilipschitz`
* `topology.metric_space.basic`
* `topology.metric_space.emetric_paracompact`
* `topology.metric_space.emetric_space`
* `topology.metric_space.equicontinuity`
* `topology.metric_space.infsep`
* `topology.metric_space.lipschitz`
* `topology.metric_space.metric_separated`
* `topology.metric_space.shrinking_lemma`
* `topology.sequences`
