From d1f2d3a634c9e78b47f5a39c4324d920bb6f68aa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Thu, 29 Aug 2024 14:15:36 +0000
Subject: [PATCH] Bump mathlib

---
 LeanAPAP.lean                                   |  3 ---
 LeanAPAP/Mathlib/Analysis/RCLike/Basic.lean     | 17 -----------------
 LeanAPAP/Mathlib/Data/Fintype/Order.lean        |  3 ---
 .../Probability/ConditionalProbability.lean     | 13 -------------
 LeanAPAP/Prereqs/Energy.lean                    |  2 +-
 lake-manifest.json                              |  6 +++---
 6 files changed, 4 insertions(+), 40 deletions(-)
 delete mode 100644 LeanAPAP/Mathlib/Analysis/RCLike/Basic.lean
 delete mode 100644 LeanAPAP/Mathlib/Data/Fintype/Order.lean
 delete mode 100644 LeanAPAP/Mathlib/Probability/ConditionalProbability.lean

diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 093a197c4a..f32c5c7844 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -6,10 +6,8 @@ import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
 import LeanAPAP.Mathlib.Algebra.Order.Module.Defs
 import LeanAPAP.Mathlib.Algebra.Star.Basic
 import LeanAPAP.Mathlib.Algebra.Star.Rat
-import LeanAPAP.Mathlib.Analysis.RCLike.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
-import LeanAPAP.Mathlib.Data.Fintype.Order
 import LeanAPAP.Mathlib.Data.NNReal.Basic
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
@@ -17,7 +15,6 @@ import LeanAPAP.Mathlib.MeasureTheory.MeasurableSpace.Defs
 import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpaceDef
 import LeanAPAP.Mathlib.Order.Filter.Basic
 import LeanAPAP.Mathlib.Order.LiminfLimsup
-import LeanAPAP.Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
diff --git a/LeanAPAP/Mathlib/Analysis/RCLike/Basic.lean b/LeanAPAP/Mathlib/Analysis/RCLike/Basic.lean
deleted file mode 100644
index 59691ddda0..0000000000
--- a/LeanAPAP/Mathlib/Analysis/RCLike/Basic.lean
+++ /dev/null
@@ -1,17 +0,0 @@
-import Mathlib.Analysis.RCLike.Basic
-
-/-!
-# TODO
-
-Rename `Real.RCLike` to `Real.instRCLike`
--/
-
-open scoped ComplexConjugate
-
-namespace RCLike
-variable {K : Type*} [RCLike K] {z : K}
-
-@[simp] lemma nnnorm_conj : ‖conj z‖₊ = ‖z‖₊ := by simp [nnnorm]
-@[simp] lemma nnnorm_natCast (n : ℕ) : ‖(n : K)‖₊ = n := by simp [nnnorm]
-
-end RCLike
diff --git a/LeanAPAP/Mathlib/Data/Fintype/Order.lean b/LeanAPAP/Mathlib/Data/Fintype/Order.lean
deleted file mode 100644
index 2a467ba12d..0000000000
--- a/LeanAPAP/Mathlib/Data/Fintype/Order.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import Mathlib.Data.Fintype.Order
-
-attribute [simp] Finite.bddAbove_range Finite.bddBelow_range
diff --git a/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean b/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean
deleted file mode 100644
index f2b432f493..0000000000
--- a/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean
+++ /dev/null
@@ -1,13 +0,0 @@
-import Mathlib.Probability.ConditionalProbability
-
-open ENNReal MeasureTheory MeasureTheory.Measure MeasurableSpace Set
-
-variable {Ω Ω' α : Type*} {m : MeasurableSpace Ω} {m' : MeasurableSpace Ω'} (μ : Measure Ω)
-  {s t : Set Ω}
-
-namespace ProbabilityTheory
-
-@[simp] lemma cond_apply_self (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) : μ[|s] s = 1 := by
-  simpa [cond] using ENNReal.inv_mul_cancel hs₀ hs
-
-end ProbabilityTheory
diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean
index eab58479f7..caccde396d 100644
--- a/LeanAPAP/Prereqs/Energy.lean
+++ b/LeanAPAP/Prereqs/Energy.lean
@@ -20,7 +20,7 @@ lemma energy_nonneg (n : ℕ) (s : Finset G) (ν : G → ℂ) : 0 ≤ energy n s
 lemma energy_nsmul (m n : ℕ) (s : Finset G) (ν : G → ℂ) :
     energy n s (m • ν) = m • energy n s ν := by
   simp only [energy, nsmul_eq_mul, mul_sum, Pi.natCast_def, Pi.mul_apply, norm_mul,
-    Complex.norm_nat]
+    Complex.norm_natCast]
 
 @[simp] lemma energy_zero (s : Finset G) (ν : G → ℂ) : energy 0 s ν = ‖ν 0‖ := by simp [energy]
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 3cef812756..be4d80533f 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
+   "rev": "d38fb94558af9957b8f479e350841ce65a1ec42c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "adaeb6b4d4bf02f60ba3ff6717486a7e895eba77",
+   "rev": "f36af1a7011c102cdf3f5f6c31d2367de28da3a8",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "79ef7496100b18304654c1476691e872fa7c491a",
+   "rev": "6da6b5512d764c784ffef6f19bf5c3dfcec6d3f9",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,