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,