chore(*): add mathlib4 synchronization comments (#18430)
Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebra.order.module`
* `algebra.order.nonneg.field`
* `algebra.order.nonneg.ring`
* `category_theory.bicategory.strict`
* `category_theory.eq_to_hom`
* `category_theory.equivalence`
* `category_theory.functor.const`
* `category_theory.opposites`
* `data.analysis.filter`
* `data.dfinsupp.lex`
* `data.fin.tuple.nat_antidiagonal`
* `data.finite.card`
* `data.finset.mul_antidiagonal`
* `data.list.indexes`
* `data.rat.denumerable`
* `data.real.pointwise`
* `group_theory.abelianization`
* `group_theory.commutator`
* `group_theory.finiteness`
* `group_theory.group_action.quotient`
* `measure_theory.measurable_space`
* `measure_theory.pi_system`
* `ring_theory.subring.basic`
* `set_theory.cardinal.basic`
* `set_theory.cardinal.finite`
* `topology.algebra.semigroup`
* `topology.compact_open`
* `topology.continuous_function.t0_sierpinski`
* `topology.discrete_quotient`
* `topology.noetherian_space`
* `topology.order.lower_topology`
* `topology.partial`
* `topology.sets.closeds`
* `topology.sets.opens`
* `topology.spectral.hom`
* `topology.uniform_space.abstract_completion`
* `topology.uniform_space.equiv`
