chore(*): add mathlib4 synchronization comments (#19115)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.category.Group.biproducts`
* `algebra.category.Module.monoidal.basic`
* `algebra.category.Ring.adjunctions`
* `algebra.monoid_algebra.grading`
* `analysis.calculus.deriv.add`
* `analysis.calculus.deriv.basic`
* `analysis.calculus.deriv.comp`
* `analysis.calculus.deriv.inverse`
* `analysis.calculus.deriv.linear`
* `analysis.calculus.deriv.mul`
* `analysis.calculus.deriv.polynomial`
* `analysis.calculus.deriv.pow`
* `analysis.calculus.deriv.prod`
* `analysis.calculus.deriv.slope`
* `analysis.calculus.deriv.star`
* `analysis.calculus.deriv.support`
* `analysis.calculus.fderiv_measurable`
* `analysis.calculus.local_extr`
* `analysis.convex.cone.dual`
* `analysis.inner_product_space.lax_milgram`
* `analysis.inner_product_space.pi_L2`
* `category_theory.bicategory.coherence`
* `category_theory.limits.fubini`
* `category_theory.monoidal.coherence_lemmas`
* `geometry.euclidean.sphere.basic`
* `geometry.euclidean.sphere.power`
* `geometry.euclidean.sphere.second_inter`
* `group_theory.complement`
* `group_theory.sylow`
* `linear_algebra.matrix.hermitian`
* `measure_theory.constructions.prod.basic`
* `measure_theory.function.lp_order`
* `measure_theory.function.lp_seminorm`
* `measure_theory.function.lp_space`
* `measure_theory.measure.complex`
* `measure_theory.measure.vector_measure`
* `number_theory.padics.ring_homs`
* `ring_theory.ideal.cotangent`
* `topology.metric_space.metrizable_uniformity`
* `topology.sheaves.forget`
* `topology.sheaves.sheaf_condition.unique_gluing`
* `topology.sheaves.sheaf_of_functions`
