mathlib3

3fcc5a49 - refactor(data/list/sublists): move lemmas to remove as import (#17694)

refactor(data/list/sublists): move lemmas to remove as import (#17694) Material on sublists is not used until later, so can be concentrated into one file. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>