[Merged by Bors] - chore: Make Finset.preimage not depend on Finset.sum

[YaelDillies]

and Data.Finset.LocallyFinite not depend on Finset.sum too

---

[urkud]

This makes BigOperators/Basic depend on Set/Finite. What do you think about creating a new file?

[YaelDillies]

I really really don't think that matters since the main reason to avoid importing Set.Finite is to avoid importing... Finset!

[urkud]

Let me have a look at the import graph of Data.Set.Finite.
Here is the list of files in the import closure of Data.Set.Finite that aren't imported by Algebra.BigOperators.Basic:

"Mathlib.Control.Applicative"
"Mathlib.Control.Traversable.Basic"
"Mathlib.Data.Finite.Basic"
"Mathlib.Data.Fin.Tuple.Basic"
"Mathlib.Data.Fintype.Card"
"Mathlib.Data.Fintype.Powerset"
"Mathlib.Data.Fintype.Prod"
"Mathlib.Data.Fintype.Sigma"
"Mathlib.Data.Fintype.Sum"
"Mathlib.Data.Fintype.Vector"
"Mathlib.Data.List.Duplicate"
"Mathlib.Data.List.NodupEquivFin"
"Mathlib.Data.List.OfFn"
"Mathlib.Data.List.Sort"
"Mathlib.Data.Pi.Lex"
"Mathlib.Data.Set.Finite"
"Mathlib.Data.Set.Functor"
"Mathlib.Data.Setoid.Basic"
"Mathlib.Data.Sym.Basic"
"Mathlib.Data.Vector"
"Mathlib.Data.Vector.Basic"
"Mathlib.Logic.Embedding.Set"
"Mathlib.Order.WellFounded"

[YaelDillies]

Given that the imports of Algebra.BigOperators.Basic are

import Mathlib.Algebra.BigOperators.Multiset.Lemmas
import Mathlib.Algebra.Function.Indicator
import Mathlib.Algebra.Ring.Opposite
import Mathlib.Data.Finset.Powerset
import Mathlib.Data.Finset.Sigma
import Mathlib.Data.Finset.Sum
import Mathlib.Data.Fintype.Pi
import Mathlib.Data.Int.Cast.Lemmas
import Mathlib.Data.Set.Image

this doesn't stick out to me. I agree that we need to split Algebra.BigOperators.Basic, but I don't think splitting it as "preimage lemmas" vs "the rest" is pertinent. So I suggest we do it in a later PR.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style