mathlib

1b36dabc - refactor(data/set/basic): move image, preimage, and range to a new file (#17842)

refactor(data/set/basic): move image, preimage, and range to a new file (#17842) This means `data.set.basic` is mainly about lattice operations. Only one proof is modified (to avoid it needing to move between files). All other lemmas are copied verbatim. Co-authored-by: Chris Hughes <chrishughes24@gmail.com>