chore(Data/Set): split some chunks off large file Data/Set/Lattice.lean (#23098)

This PR tries to split some meaningful chunks off of `Mathlib.Data.Set.Lattice`:
* The new file `Mathlib.Data.Set.BooleanAlgebra` contains the `CompleteAtomicBooleanAlgebra (Set ɑ)` instance (and nothing more)
* The new file `Mathlib.Data.Set.Lattice.Image` contains results on the interaction between the complete lattice structure and `image`, `preimage`, `image2`, `MapsTo`, `InjOn`, ...

This leaves `Mathlib.Data.Set.Lattice` focussed on interactions between the lattice operators themselves, more or less. (Although there is a bit that doesn't really fit with lattice theory and might move to `Data.Set.Sigma` except it would screw up the import direction...)

I first tried designing this split by following the import structure but found nothing useful to guide us there: the lemmas that could be upstreamed or at least moved to another file seem to follow no real pattern. So I went instead by looking at the lemma contents entirely and hoped for `lake exe shake` to catch some import improvements (we get a few tens of files with a few import reductions, and it happens that one of those, `Mathlib.Data.Finset.Lattice.Fold` is on the long pole).

Author: Vierkantor

Mathlib.lean

@@ -3199,6 +3199,7 @@ import Mathlib.Data.Seq.WSeq
 import Mathlib.Data.Set.Accumulate
 import Mathlib.Data.Set.Basic
 import Mathlib.Data.Set.BoolIndicator
+import Mathlib.Data.Set.BooleanAlgebra
 import Mathlib.Data.Set.Card
 import Mathlib.Data.Set.Card.Arithmetic
 import Mathlib.Data.Set.CoeSort
@@ -3222,6 +3223,7 @@ import Mathlib.Data.Set.Image
 import Mathlib.Data.Set.Inclusion
 import Mathlib.Data.Set.Insert
 import Mathlib.Data.Set.Lattice
+import Mathlib.Data.Set.Lattice.Image
 import Mathlib.Data.Set.List
 import Mathlib.Data.Set.MemPartition
 import Mathlib.Data.Set.Monotone

Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

@@ -6,7 +6,7 @@ Authors: Johan Commelin, Floris van Doorn, Yaël Dillies
 import Mathlib.Algebra.Group.Equiv.Basic
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
-import Mathlib.Data.Set.Lattice
+import Mathlib.Data.Set.Lattice.Image
 import Mathlib.Tactic.MinImports
 
 /-!

Mathlib/Algebra/Group/Subsemigroup/Basic.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzza
 Amelia Livingston, Yury Kudryashov, Yakov Pechersky
 -/
 import Mathlib.Algebra.Group.Subsemigroup.Defs
-import Mathlib.Data.Set.Lattice
+import Mathlib.Data.Set.Lattice.Image
 
 /-!
 # Subsemigroups: `CompleteLattice` structure

Mathlib/Algebra/Order/Group/Action.lean

@@ -6,6 +6,7 @@ Authors: Eric Wieser
 import Mathlib.Algebra.Group.Action.Defs
 import Mathlib.Algebra.Order.Monoid.Unbundled.Defs
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
+import Mathlib.Tactic.Cases
 
 /-!
 # Results about `CovariantClass G α HSMul.hSMul LE.le`

Mathlib/CategoryTheory/Sites/Sieves.lean

@@ -3,8 +3,8 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Edward Ayers
 -/
-import Mathlib.Data.Set.Lattice
 import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
+import Mathlib.Data.Set.BooleanAlgebra
 
 /-!
 # Theory of sieves

Mathlib/CategoryTheory/Subpresheaf/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang, Joël Riou
 -/
 import Mathlib.CategoryTheory.Elementwise
-import Mathlib.Data.Set.Lattice
+import Mathlib.Data.Set.Lattice.Image
 
 /-!
 

Mathlib/Data/Finset/Lattice/Fold.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Data.Finset.Fold
 import Mathlib.Data.Multiset.Lattice
-import Mathlib.Data.Set.Lattice
+import Mathlib.Data.Set.BooleanAlgebra
 import Mathlib.Order.Hom.Lattice
 import Mathlib.Order.Nat
 

Mathlib/Data/Finset/NAry.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Data.Finset.Lattice.Prod
 import Mathlib.Data.Finite.Prod
+import Mathlib.Data.Set.Lattice.Image
 
 /-!
 # N-ary images of finsets

Mathlib/Data/Nat/Pairing.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 -/
 import Mathlib.Algebra.Notation.Prod
 import Mathlib.Data.Nat.Sqrt
-import Mathlib.Data.Set.Lattice
+import Mathlib.Data.Set.Lattice.Image
 
 /-!
 # Naturals pairing function

Mathlib/Data/Rel.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
-import Mathlib.Data.Set.Lattice
+import Mathlib.Data.Set.BooleanAlgebra
 import Mathlib.Tactic.AdaptationNote
 
 /-!