diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index d91d30e90c..49e02e2e9a 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -3,15 +3,12 @@ import LeanAPAP.FiniteField.Basic
 import LeanAPAP.Mathlib.Algebra.Group.Action.Defs
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 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.Normed.Field.Basic
-import LeanAPAP.Mathlib.Analysis.RCLike.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.Data.ENNReal.Operations
-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
@@ -20,7 +17,6 @@ import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpaceDef
 import LeanAPAP.Mathlib.Order.ConditionallyCompleteLattice.Basic
 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/Algebra/Order/Module/Defs.lean b/LeanAPAP/Mathlib/Algebra/Order/Module/Defs.lean
deleted file mode 100644
index 8534515b29..0000000000
--- a/LeanAPAP/Mathlib/Algebra/Order/Module/Defs.lean
+++ /dev/null
@@ -1,4 +0,0 @@
-import Mathlib.Algebra.Order.Module.Defs
-
-attribute [gcongr] smul_le_smul_of_nonneg_left smul_le_smul_of_nonneg_right
-  smul_lt_smul_of_pos_left smul_lt_smul_of_pos_right
diff --git a/LeanAPAP/Mathlib/Analysis/Normed/Field/Basic.lean b/LeanAPAP/Mathlib/Analysis/Normed/Field/Basic.lean
index b1574ccbac..68d51f52ba 100644
--- a/LeanAPAP/Mathlib/Analysis/Normed/Field/Basic.lean
+++ b/LeanAPAP/Mathlib/Analysis/Normed/Field/Basic.lean
@@ -10,7 +10,7 @@ lemma norm_one_sub_mul (ha : ‖a‖ ≤ 1) : ‖c - a * b‖ ≤ ‖c - a‖ +
     _ ≤ ‖c - a‖ + 1 * ‖1 - b‖ := by gcongr
     _ = ‖c - a‖ + ‖1 - b‖ := by simp
 
-lemma norm_one_sub_mpul' (hb : ‖b‖ ≤ 1) : ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖ := by
+lemma norm_one_sub_mul' (hb : ‖b‖ ≤ 1) : ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖ := by
   rw [add_comm]; exact norm_one_sub_mul (R := Rᵐᵒᵖ) hb
 
 lemma nnnorm_one_sub_mul (ha : ‖a‖₊ ≤ 1) : ‖c - a * b‖₊ ≤ ‖c - a‖₊ + ‖1 - b‖₊ := norm_one_sub_mul ha
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..23b9f1250e 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": "6ce4187086ef93261927bbc72d061888099b30fc",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,