From 851cb08aca06feddfcd5da28120dcc33c213b10f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 4 Oct 2024 07:44:55 +0000
Subject: [PATCH] Bump mathlib

---
 LeanCamCombi.lean                             |  2 +-
 .../Algebra/Group/Pointwise/Set/Card.lean     | 44 ++++++++++++++++---
 LeanCamCombi/Mathlib/Algebra/Order/Pi.lean    | 19 --------
 LeanCamCombi/Mathlib/Data/Finsupp/Order.lean  |  2 +-
 .../Mathlib/SetTheory/Cardinal/Basic.lean     | 17 +++++++
 lake-manifest.json                            |  8 ++--
 lean-toolchain                                |  2 +-
 7 files changed, 62 insertions(+), 32 deletions(-)
 delete mode 100644 LeanCamCombi/Mathlib/Algebra/Order/Pi.lean
 create mode 100644 LeanCamCombi/Mathlib/SetTheory/Cardinal/Basic.lean

diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean
index 6b588e8cbe..ecce95c70c 100644
--- a/LeanCamCombi.lean
+++ b/LeanCamCombi.lean
@@ -21,7 +21,6 @@ import LeanCamCombi.LittlewoodOfford
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Card
 import LeanCamCombi.Mathlib.Algebra.Order.BigOperators.LocallyFinite
-import LeanCamCombi.Mathlib.Algebra.Order.Pi
 import LeanCamCombi.Mathlib.Analysis.Convex.Between
 import LeanCamCombi.Mathlib.Analysis.Convex.Exposed
 import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
@@ -47,6 +46,7 @@ import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.Sublattice
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
+import LeanCamCombi.Mathlib.SetTheory.Cardinal.Basic
 import LeanCamCombi.MetricBetween
 import LeanCamCombi.MinkowskiCaratheodory
 import LeanCamCombi.OrderShatter
diff --git a/LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set/Card.lean b/LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set/Card.lean
index b99e5bff3f..484d377f1a 100644
--- a/LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set/Card.lean
+++ b/LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@@ -3,9 +3,10 @@ Copyright (c) 2024 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Algebra.Group.Action.Basic
-import Mathlib.Algebra.Group.Pointwise.Set.Basic
+import Mathlib.Algebra.Group.Pointwise.Set.Card
+import Mathlib.Data.Set.Pointwise.Finite
 import Mathlib.SetTheory.Cardinal.Finite
+import LeanCamCombi.Mathlib.SetTheory.Cardinal.Basic
 
 /-!
 # Cardinalities of pointwise operations on sets
@@ -16,6 +17,25 @@ open scoped Cardinal Pointwise
 namespace Set
 variable {G M α : Type*}
 
+section Mul
+variable [Mul M] {s t : Set M}
+
+@[to_additive]
+lemma _root_.Cardinal.mk_mul_le : #(s * t) ≤ #s * #t := by
+  rw [← image2_mul]; exact Cardinal.mk_image2_le
+
+variable [IsCancelMul M]
+
+@[to_additive]
+lemma natCard_mul_le : Nat.card (s * t) ≤ Nat.card s * Nat.card t := by
+  obtain h | h := (s * t).infinite_or_finite
+  · simp [Set.Infinite.card_eq_zero h]
+  simp only [Nat.card, ← Cardinal.toNat_mul]
+  refine Cardinal.toNat_le_toNat Cardinal.mk_mul_le ?_
+  aesop (add simp [Cardinal.mul_lt_aleph0_iff, finite_mul])
+
+end Mul
+
 section InvolutiveInv
 variable [InvolutiveInv G] {s t : Set G}
 
@@ -29,8 +49,23 @@ lemma natCard_inv (s : Set G) : Nat.card ↥(s⁻¹) = Nat.card s := by
 
 end InvolutiveInv
 
+section DivInvMonoid
+variable [DivInvMonoid M] {s t : Set M}
+
+@[to_additive]
+lemma _root_.Cardinal.mk_div_le : #(s / t) ≤ #s * #t := by
+  rw [← image2_div]; exact Cardinal.mk_image2_le
+
+end DivInvMonoid
+
 section Group
-variable [Group G] [MulAction G α] {s t : Set G}
+variable [Group G] {s t : Set G}
+
+@[to_additive]
+lemma natCard_div_le : Nat.card (s / t) ≤ Nat.card s * Nat.card t := by
+  rw [div_eq_mul_inv, ← natCard_inv t]; exact natCard_mul_le
+
+variable [MulAction G α]
 
 @[to_additive (attr := simp)]
 lemma _root_.Cardinal.mk_smul_set (a : G) (s : Set α) : #↥(a • s) = #s :=
@@ -40,8 +75,5 @@ lemma _root_.Cardinal.mk_smul_set (a : G) (s : Set α) : #↥(a • s) = #s :=
 lemma natCard_smul_set (a : G) (s : Set α) : Nat.card ↥(a • s) = Nat.card s :=
   Nat.card_image_of_injective (MulAction.injective a) _
 
-@[to_additive (attr := deprecated (since := "2024-09-30"))]
-alias card_smul_set := Cardinal.mk_smul_set
-
 end Group
 end Set
diff --git a/LeanCamCombi/Mathlib/Algebra/Order/Pi.lean b/LeanCamCombi/Mathlib/Algebra/Order/Pi.lean
deleted file mode 100644
index 110d0aa5b8..0000000000
--- a/LeanCamCombi/Mathlib/Algebra/Order/Pi.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-import Mathlib.Algebra.Order.Pi
-
-namespace Pi
-variable {ι : Type*} {α : ι → Type*} [DecidableEq ι] [∀ i, One (α i)] [∀ i, Preorder (α i)] {i : ι}
-  {a b : α i}
-
-@[to_additive (attr := simp)]
-lemma mulSingle_le_mulSingle : mulSingle i a ≤ mulSingle i b ↔ a ≤ b := by
-  simp [mulSingle, update_le_update_iff]
-
-@[to_additive (attr := gcongr)] alias ⟨_, GCongr.mulSingle_mono⟩ := mulSingle_le_mulSingle
-
-@[to_additive (attr := simp) single_nonneg]
-lemma one_le_mulSingle : 1 ≤ mulSingle i a ↔ 1 ≤ a := by simp [mulSingle]
-
-@[to_additive (attr := simp)]
-lemma mulSingle_le_one : mulSingle i a ≤ 1 ↔ a ≤ 1 := by simp [mulSingle]
-
-end Pi
diff --git a/LeanCamCombi/Mathlib/Data/Finsupp/Order.lean b/LeanCamCombi/Mathlib/Data/Finsupp/Order.lean
index 71ab1610a7..ba9448624c 100644
--- a/LeanCamCombi/Mathlib/Data/Finsupp/Order.lean
+++ b/LeanCamCombi/Mathlib/Data/Finsupp/Order.lean
@@ -1,6 +1,6 @@
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Algebra.Order.Pi
 import Mathlib.Data.Finsupp.Order
-import LeanCamCombi.Mathlib.Algebra.Order.Pi
 
 namespace Finsupp
 variable {ι κ α β : Type*}
diff --git a/LeanCamCombi/Mathlib/SetTheory/Cardinal/Basic.lean b/LeanCamCombi/Mathlib/SetTheory/Cardinal/Basic.lean
new file mode 100644
index 0000000000..faa0ce5af1
--- /dev/null
+++ b/LeanCamCombi/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -0,0 +1,17 @@
+import Mathlib.SetTheory.Cardinal.Basic
+
+open Set
+
+universe u
+
+namespace Cardinal
+
+@[simp] lemma mk_setProd {α β : Type u} (s : Set α) (t : Set β) : #(s ×ˢ t) = #s * #t := by
+  rw [mul_def, mk_congr (Equiv.Set.prod ..)]
+
+lemma mk_image2_le {α β γ : Type u} {f : α → β → γ} {s : Set α} {t : Set β} :
+    #(image2 f s t) ≤ #s * #t := by
+  rw [← image_uncurry_prod, ← mk_setProd]
+  exact mk_image_le
+
+end Cardinal
diff --git a/lake-manifest.json b/lake-manifest.json
index 7c82b98bc1..e3e8b1d94b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f274aed7ae8d1addd3e70adaf3183ccc6e1ed43d",
+   "rev": "63c1c38b123b0741b7b7fd56fb8510f95bfd0e55",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ff420521a0c098891f4f44ecda9dd7ff57b50bad",
+   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
+   "rev": "6b6ad220389444229d6b29c386b039e18345a003",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0c13e18343c06775d5f2121a433f70392b7e2caa",
+   "rev": "b0bcf46fb80c3cb1eba7696aadf4ee19b959fd09",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/lean-toolchain b/lean-toolchain
index 89985206ac..7c79e97102 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.13.0-rc2