mathlib3

c5bb320c - refactor(*): Random lemmas and modifications from the shifting refactor. (#10940)