mathlib3

chore(*): add mathlib4 synchronization comments

#19240

Open