Bump mathlib

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

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

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*}

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

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,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.13.0-rc2