mathlib

5e934cd9 - chore(*): cleanup imports, split off data/finset/preimage from data/set/finite (#4221)

chore(*): cleanup imports, split off data/finset/preimage from data/set/finite (#4221) Mostly this consists of moving some content from `data.set.finite` to `data.finset.preimage`, in order to reduce imports in `data.set.finite`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>