chore(*): add mathlib4 synchronization comments (#18566)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.algebra.subalgebra.basic`
* `algebra.algebra.subalgebra.tower`
* `algebra.free_non_unital_non_assoc_algebra`
* `algebra.monoid_algebra.basic`
* `algebra.monoid_algebra.support`
* `algebra.polynomial.big_operators`
* `algebra.star.subalgebra`
* `analysis.normed.group.ball_sphere`
* `analysis.normed.group.basic`
* `analysis.normed.group.completion`
* `analysis.normed.group.hom`
* `analysis.normed.group.hom_completion`
* `analysis.normed.group.infinite_sum`
* `analysis.normed.group.seminorm`
* `analysis.normed_space.indicator_function`
* `analysis.subadditive`
* `category_theory.abelian.images`
* `category_theory.abelian.non_preadditive`
* `category_theory.adjunction.comma`
* `category_theory.concrete_category.reflects_isomorphisms`
* `category_theory.is_connected`
* `category_theory.limits.bicones`
* `category_theory.limits.comma`
* `category_theory.limits.cone_category`
* `category_theory.limits.constructions.equalizers`
* `category_theory.limits.constructions.finite_products_of_binary_products`
* `category_theory.limits.constructions.limits_of_products_and_equalizers`
* `category_theory.limits.essentially_small`
* `category_theory.limits.kan_extension`
* `category_theory.limits.lattice`
* `category_theory.limits.mono_coprod`
* `category_theory.limits.opposites`
* `category_theory.limits.preserves.filtered`
* `category_theory.limits.preserves.shapes.biproducts`
* `category_theory.limits.preserves.shapes.zero`
* `category_theory.limits.shapes.biproducts`
* `category_theory.limits.shapes.finite_products`
* `category_theory.limits.shapes.functor_category`
* `category_theory.limits.shapes.kernels`
* `category_theory.limits.shapes.normal_mono.basic`
* `category_theory.limits.shapes.normal_mono.equalizers`
* `category_theory.limits.shapes.zero_morphisms`
* `category_theory.limits.small_complete`
* `category_theory.limits.types`
* `category_theory.linear.basic`
* `category_theory.linear.functor_category`
* `category_theory.monoidal.End`
* `category_theory.preadditive.additive_functor`
* `category_theory.preadditive.basic`
* `category_theory.preadditive.biproducts`
* `category_theory.preadditive.functor_category`
* `combinatorics.hindman`
* `control.bifunctor`
* `control.bitraversable.basic`
* `data.complex.basic`
* `data.nat.choose.cast`
* `data.nat.choose.vandermonde`
* `data.nat.factorial.cast`
* `data.polynomial.basic`
* `data.polynomial.cardinal`
* `data.polynomial.coeff`
* `data.polynomial.degree.definitions`
* `data.polynomial.degree.lemmas`
* `data.polynomial.degree.trailing_degree`
* `data.polynomial.derivative`
* `data.polynomial.erase_lead`
* `data.polynomial.eval`
* `data.polynomial.induction`
* `data.polynomial.inductions`
* `data.polynomial.monic`
* `data.polynomial.monomial`
* `data.polynomial.reverse`
* `data.real.sqrt`
* `data.tree`
* `linear_algebra.affine_space.slope`
* `logic.equiv.functor`
* `number_theory.basic`
* `order.jordan_holder`
* `ring_theory.adjoin.basic`
* `ring_theory.ideal.operations`
* `ring_theory.ideal.quotient`
* `ring_theory.localization.basic`
* `ring_theory.nilpotent`
* `ring_theory.polynomial.pochhammer`
* `topology.algebra.affine`
* `topology.algebra.localization`
* `topology.algebra.ring.ideal`
* `topology.fiber_bundle.trivialization`
* `topology.instances.ennreal`
* `topology.metric_space.completion`
* `topology.metric_space.gluing`
* `topology.metric_space.isometric_smul`
* `topology.metric_space.isometry`
* `topology.uniform_space.compare_reals`
* `topology.unit_interval`
