chore(*): add mathlib4 synchronization comments (#18464)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.algebra.basic`
* `algebra.algebra.hom`
* `algebra.algebra.prod`
* `algebra.module.algebra`
* `category_theory.adjunction.basic`
* `category_theory.category.ulift`
* `category_theory.comm_sq`
* `category_theory.conj`
* `category_theory.core`
* `category_theory.discrete_category`
* `category_theory.monoidal.category`
* `category_theory.pempty`
* `category_theory.punit`
* `category_theory.sums.basic`
* `category_theory.yoneda`
* `combinatorics.hales_jewett`
* `computability.NFA`
* `computability.epsilon_NFA`
* `data.analysis.topology`
* `data.dfinsupp.multiset`
* `data.multiset.interval`
* `data.pfunctor.multivariate.M`
* `data.pfunctor.multivariate.W`
* `data.pfunctor.multivariate.basic`
* `data.pfunctor.univariate.M`
* `data.qpf.multivariate.basic`
* `data.qpf.multivariate.constructions.comp`
* `data.qpf.multivariate.constructions.const`
* `data.qpf.multivariate.constructions.prj`
* `data.qpf.multivariate.constructions.quot`
* `data.rat.nnrat`
* `data.real.nnreal`
* `deprecated.subfield`
* `deprecated.subring`
* `group_theory.commuting_probability`
* `linear_algebra.finsupp`
* `linear_algebra.prod`
* `linear_algebra.quotient`
* `number_theory.class_number.admissible_abs`
* `order.extension.well`
* `order.filter.filter_product`
* `order.pfilter`
* `order.prime_ideal`
* `ring_theory.ideal.basic`
* `set_theory.ordinal.exponential`
* `set_theory.ordinal.fixed_point`
* `set_theory.ordinal.natural_ops`
* `set_theory.ordinal.topology`
* `topology.algebra.group.basic`
* `topology.algebra.group.compact`
* `topology.is_locally_homeomorph`
* `topology.local_homeomorph`
* `topology.uniform_space.completion`
