mathlib

527e406f - chore(data/list): golf, merge 2 files (#18120)

chore(data/list): golf, merge 2 files (#18120) - merge `data.list.modeq` into `data.list.rotate`; - mark `list.rotate_eq_rotate` as `@[simp]`; - golf some proofs.