refactor(Data/Finset): reverse Finset.Image <-> Finset.SymmDiff import (#23398)

I noticed while looking at the [long pole](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/The.20long.20pole.20in.20mathlib/near/508704797) that `Finset.SymmDiff` is not required anywhere on the pole, so if we reverse the import direction between it and `Finset.Image` we can make the import graph a little bit less tall.

Author: Vierkantor

Mathlib/Data/Finset/Image.lean

@@ -9,7 +9,7 @@ import Mathlib.Data.Finset.Disjoint
 import Mathlib.Data.Finset.Erase
 import Mathlib.Data.Finset.Filter
 import Mathlib.Data.Finset.Range
-import Mathlib.Data.Finset.SymmDiff
+import Mathlib.Data.Finset.SDiff
 
 /-! # Image and map operations on finite sets
 
@@ -454,11 +454,6 @@ lemma image_sdiff_of_injOn [DecidableEq α] {t : Finset α} (hf : Set.InjOn f s)
     (s \ t).image f = s.image f \ t.image f :=
   mod_cast Set.image_diff_of_injOn hf <| coe_subset.2 hts
 
-open scoped symmDiff in
-theorem image_symmDiff [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Injective f) :
-    (s ∆ t).image f = s.image f ∆ t.image f :=
-  mod_cast Set.image_symmDiff hf s t
-
 theorem _root_.Disjoint.of_image_finset {s t : Finset α} {f : α → β}
     (h : Disjoint (s.image f) (t.image f)) : Disjoint s t :=
   disjoint_iff_ne.2 fun _ ha _ hb =>

Mathlib/Data/Finset/SymmDiff.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, Minchao Wu, Mario Carneiro
 -/
-import Mathlib.Data.Finset.SDiff
+import Mathlib.Data.Finset.Image
 import Mathlib.Data.Set.SymmDiff
 
 /-!
@@ -48,6 +48,10 @@ theorem coe_symmDiff : (↑(s ∆ t) : Set α) = (s : Set α) ∆ t :=
 @[simp] lemma symmDiff_nonempty : (s ∆ t).Nonempty ↔ s ≠ t :=
   nonempty_iff_ne_empty.trans symmDiff_eq_empty.not
 
+theorem image_symmDiff [DecidableEq β] {f : α → β} (s t : Finset α) (hf : Injective f) :
+    (s ∆ t).image f = s.image f ∆ t.image f :=
+  mod_cast Set.image_symmDiff hf s t
+
 end SymmDiff
 
 end Finset

Mathlib/Data/Fintype/Sets.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.Finset.BooleanAlgebra
+import Mathlib.Data.Finset.SymmDiff
 import Mathlib.Data.Fintype.OfMap
 
 /-!