chore(Data/Finset): don't import algebra in Finset.Lattice.Fold (#21883)

We don't need to know what a monoid is in order to define the maximum of a finset. This PR replaces the approach of #21874 (reversing the `Finset.Max` -> `Finset.Sort` import) with cleaning up `Finset.Max`'s dependencies.

In particular, we reverse the import direction for `Multiset.Bind` and `Multiset.Fold` (the former imports a lot anyway), and split some results off from `Finset.Lattice.Fold` based on dependencies: `Finset.{Pi,Prod,Union}` mapping to `Finset.Lattice.{Pi,Prod,Union}`.

Author: Vierkantor

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
 import Mathlib.Data.Finset.Max
+import Mathlib.Data.Finset.Prod
 import Mathlib.Data.Fintype.Powerset
 
 /-!

Mathlib.lean

@@ -2651,6 +2651,9 @@ import Mathlib.Data.Finset.Interval
 import Mathlib.Data.Finset.Lattice.Basic
 import Mathlib.Data.Finset.Lattice.Fold
 import Mathlib.Data.Finset.Lattice.Lemmas
+import Mathlib.Data.Finset.Lattice.Pi
+import Mathlib.Data.Finset.Lattice.Prod
+import Mathlib.Data.Finset.Lattice.Union
 import Mathlib.Data.Finset.Max
 import Mathlib.Data.Finset.MulAntidiagonal
 import Mathlib.Data.Finset.NAry

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -9,6 +9,7 @@ import Mathlib.Algebra.Group.Even
 import Mathlib.Data.Finset.Piecewise
 import Mathlib.Data.Finset.Powerset
 import Mathlib.Data.Finset.Preimage
+import Mathlib.Data.Finset.Prod
 import Mathlib.Data.Fintype.Pi
 
 /-!

Mathlib/Algebra/GCDMonoid/Multiset.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
 import Mathlib.Algebra.GCDMonoid.Basic
+import Mathlib.Algebra.Order.Group.Multiset
 import Mathlib.Data.Multiset.FinsetOps
 import Mathlib.Data.Multiset.Fold
 

Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean

@@ -3,12 +3,12 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import Mathlib.Algebra.BigOperators.Group.Multiset.Basic
+import Mathlib.Algebra.BigOperators.Group.Multiset.Defs
 import Mathlib.Algebra.Order.BigOperators.Group.List
 import Mathlib.Algebra.Order.Group.Abs
+import Mathlib.Algebra.Order.Monoid.OrderDual
 import Mathlib.Data.List.MinMax
 import Mathlib.Data.Multiset.Fold
-import Mathlib.Algebra.Order.Monoid.OrderDual
 
 /-!
 # Big operators on a multiset in ordered groups

Mathlib/Algebra/Order/Field/Pi.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.Order.Monoid.Defs
+import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
 import Mathlib.Data.Finset.Lattice.Fold
 import Mathlib.Data.Fintype.Basic
 

Mathlib/Algebra/Order/Group/Finset.lean

@@ -8,7 +8,7 @@ import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
 import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
 import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
-import Mathlib.Data.Finset.Lattice.Fold
+import Mathlib.Data.Finset.Lattice.Prod
 
 /-!
 # `Finset.sup` in a group

Mathlib/Algebra/Order/Group/Multiset.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.Group.Hom.Defs
 import Mathlib.Algebra.Group.Nat.Defs
 import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
 import Mathlib.Algebra.Order.Sub.Defs
-import Mathlib.Data.Multiset.Dedup
+import Mathlib.Data.Multiset.Fold
 
 /-!
 # Multisets form an ordered monoid
@@ -182,4 +182,17 @@ lemma addHom_ext [AddZeroClass β] ⦃f g : Multiset α →+ β⦄ (h : ∀ x, f
   · simp only [_root_.map_zero]
   · simp only [← singleton_add, _root_.map_add, ih, h]
 
+open Nat
+
+theorem le_smul_dedup [DecidableEq α] (s : Multiset α) : ∃ n : ℕ, s ≤ n • dedup s :=
+  ⟨(s.map fun a => count a s).fold max 0,
+    le_iff_count.2 fun a => by
+      rw [count_nsmul]; by_cases h : a ∈ s
+      · refine le_trans ?_ (Nat.mul_le_mul_left _ <| count_pos.2 <| mem_dedup.2 h)
+        have : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a)) := by
+          simp [le_max_left]
+        rw [cons_erase h] at this
+        simpa [mul_succ] using this
+      · simp [count_eq_zero.2 h, Nat.zero_le]⟩
+
 end Multiset

Mathlib/Combinatorics/SetFamily/Compression/Down.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import Mathlib.Data.Finset.Card
 import Mathlib.Data.Finset.Lattice.Fold
 
 /-!

Mathlib/Combinatorics/Young/YoungDiagram.lean

@@ -3,8 +3,9 @@ Copyright (c) 2022 Jake Levinson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jake Levinson
 -/
-import Mathlib.Order.UpperLower.Basic
 import Mathlib.Data.Finset.Preimage
+import Mathlib.Data.Finset.Prod
+import Mathlib.Order.UpperLower.Basic
 
 /-!
 # Young diagrams