refactor(data/finset/image): split out of data/finset/basic (#17852)

This somewhat matches the split for `data/set/basic`, and makes the file shorter by a reasonable amount.

The proof of `bUnion_singleton_eq_self` was tweaked slightly so that it didn't need to move file.

Author: eric-wieser

src/data/finset/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad
 -/
-import data.finset.basic
+import data.finset.image
 import tactic.by_contra
 
 /-!

src/data/finset/card.lean

@@ -1,5 +1,6 @@
 import data.finset.basic
 import data.finset.fold
+import data.finset.image
 import data.finset.lattice
 import data.finset.locally_finite
 import data.finset.nat_antidiagonal

src/data/finset/default.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import algebra.order.monoid.with_top
-import data.finset.basic
+import data.finset.image
 import data.multiset.fold
 
 /-!

src/data/finset/fold.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import data.finset.basic
+import data.finset.image
 import data.multiset.pi
 
 /-!

src/data/finset/image.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import data.finset.basic
+import data.finset.image
 
 /-!
 # Finite types

src/data/finset/pi.lean

@@ -1,5 +1,5 @@
 import data.set.finite
-import data.finset.basic
+import data.finset.image
 
 def s : finset (fin 3) := {0, 1}