refactor(data/set/basic): move image, preimage, and range to a new fi…

…le (#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>

src/algebra/hom/ring.lean

@@ -8,7 +8,7 @@ import algebra.ring.basic
 import algebra.divisibility.basic
 import data.pi.algebra
 import algebra.hom.units
-import data.set.basic
+import data.set.image
 
 /-!
 # Homomorphisms of semirings and rings

src/data/bool/set.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
 import data.bool.basic
-import data.set.basic
+import data.set.image
 
 /-!
 # Booleans and set operations

src/data/nat/set.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 
-import data.set.basic
+import data.set.image
 
 /-!
 ### Recursion on the natural numbers and `set.range`