chore(*): add mathlib4 synchronization comments (#19238)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.expr`
* `algebraic_geometry.morphisms.finite_type`
* `algebraic_geometry.morphisms.ring_hom_properties`
* `arithcc`
* `canonically_ordered_comm_semiring_two_mul`
* `char_p_zero_ne_char_zero`
* `cyclotomic_105`
* `data.matrix.auto`
* `direct_sum_is_internal`
* `examples.mersenne_primes`
* `examples.prop_encodable`
* `geometry.manifold.instances.sphere`
* `girard`
* `homogeneous_prime_not_prime`
* `imo.imo1959_q1`
* `imo.imo1960_q1`
* `imo.imo1962_q1`
* `imo.imo1962_q4`
* `imo.imo1964_q1`
* `imo.imo1969_q1`
* `imo.imo1972_q5`
* `imo.imo1975_q1`
* `imo.imo1977_q6`
* `imo.imo1981_q3`
* `imo.imo1987_q1`
* `imo.imo1988_q6`
* `imo.imo1994_q1`
* `imo.imo1998_q2`
* `imo.imo2001_q2`
* `imo.imo2001_q6`
* `imo.imo2005_q3`
* `imo.imo2005_q4`
* `imo.imo2006_q3`
* `imo.imo2006_q5`
* `imo.imo2008_q2`
* `imo.imo2008_q3`
* `imo.imo2008_q4`
* `imo.imo2011_q3`
* `imo.imo2011_q5`
* `imo.imo2013_q1`
* `imo.imo2013_q5`
* `imo.imo2019_q1`
* `imo.imo2019_q2`
* `imo.imo2019_q4`
* `imo.imo2020_q2`
* `imo.imo2021_q1`
* `linear_order_with_pos_mul_pos_eq_zero`
* `map_floor`
* `miu_language.basic`
* `miu_language.decision_nec`
* `miu_language.decision_suf`
* `oxford_invariants.2021summer.week3_p1`
* `phillips`
* `pseudoelement`
* `quadratic_form`
* `seminorm_lattice_not_distrib`
* `sensitivity`
* `sorgenfrey_line`
* `wiedijk_100_theorems.abel_ruffini`
* `wiedijk_100_theorems.area_of_a_circle`
* `wiedijk_100_theorems.ascending_descending_sequences`
* `wiedijk_100_theorems.ballot_problem`
* `wiedijk_100_theorems.birthday_problem`
* `wiedijk_100_theorems.cubing_a_cube`
* `wiedijk_100_theorems.friendship_graphs`
* `wiedijk_100_theorems.herons_formula`
* `wiedijk_100_theorems.inverse_triangle_sum`
* `wiedijk_100_theorems.konigsberg`
* `wiedijk_100_theorems.partition`
* `wiedijk_100_theorems.perfect_numbers`
* `wiedijk_100_theorems.solution_of_cubic`
* `wiedijk_100_theorems.sum_of_prime_reciprocals_diverges`
* `zero_divisors_in_add_monoid_algebras`
