From 4811a5beece18c60f7f4614a4429f22a0fbe3e4e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sun, 24 Nov 2024 08:33:24 +0000
Subject: [PATCH] Bump mathlib

---
 LeanAPAP.lean                                          |  2 --
 .../Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean | 10 ----------
 LeanAPAP/Mathlib/Probability/UniformOn.lean            |  8 --------
 LeanAPAP/Physics/AlmostPeriodicity.lean                |  1 -
 LeanAPAP/Prereqs/Chang.lean                            |  1 -
 lake-manifest.json                                     |  4 ++--
 6 files changed, 2 insertions(+), 24 deletions(-)
 delete mode 100644 LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
 delete mode 100644 LeanAPAP/Mathlib/Probability/UniformOn.lean

diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 72421693bd..0ae1f812d7 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -1,9 +1,7 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
-import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Mathlib.Probability.UniformOn
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
diff --git a/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean b/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
deleted file mode 100644
index bc8de6bd9b..0000000000
--- a/LeanAPAP/Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-import Mathlib.Algebra.Order.GroupWithZero.Unbundled
-
-@[bound] alias ⟨_, Bound.one_le_inv₀⟩ := one_le_inv₀
-
-attribute [bound] mul_le_one₀
-
-@[bound]
-protected lemma Bound.one_lt_mul {M₀ : Type*} [MonoidWithZero M₀] [Preorder M₀] [ZeroLEOneClass M₀]
-    [PosMulMono M₀] [MulPosMono M₀] {a b : M₀} : 1 ≤ a ∧ 1 < b ∨ 1 < a ∧ 1 ≤ b → 1 < a * b := by
-  rintro (⟨ha, hb⟩ | ⟨ha, hb⟩); exacts [one_lt_mul ha hb, one_lt_mul_of_lt_of_le ha hb]
diff --git a/LeanAPAP/Mathlib/Probability/UniformOn.lean b/LeanAPAP/Mathlib/Probability/UniformOn.lean
deleted file mode 100644
index 24ab9172d4..0000000000
--- a/LeanAPAP/Mathlib/Probability/UniformOn.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-import Mathlib.Probability.UniformOn
-
-namespace ProbabilityTheory
-variable {Ω : Type*} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω}
-
-@[simp] lemma uniformOn_eq_zero : uniformOn s = 0 ↔ s.Infinite ∨ s = ∅ := by simp [uniformOn]
-
-end ProbabilityTheory
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
index 98a41e1fcd..f7db7df333 100644
--- a/LeanAPAP/Physics/AlmostPeriodicity.lean
+++ b/LeanAPAP/Physics/AlmostPeriodicity.lean
@@ -2,7 +2,6 @@ import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.Data.Complex.ExponentialBounds
 import Mathlib.Tactic.Bound
-import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Inner.Hoelder.Discrete
diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean
index a0226e897e..737425e76a 100644
--- a/LeanAPAP/Prereqs/Chang.lean
+++ b/LeanAPAP/Prereqs/Chang.lean
@@ -1,7 +1,6 @@
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Analysis.MeanInequalities
 import Mathlib.Tactic.Bound
-import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Prereqs.Rudin
diff --git a/lake-manifest.json b/lake-manifest.json
index 74df2e8009..03b0f36292 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "485efbc439ee0ebdeae8afb0acd24a5e82e2f771",
+   "rev": "0dc51ac7947ff6aa2c16bcffb64c46c7149d1276",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fb23240e8b4409f2f23bcd07aa73c7451f216413",
+   "rev": "3ece930d0a4a55679efa52b1a825ac93b2469a06",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,