diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 534087843e..dc5c086c19 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -17,7 +17,6 @@ import LeanAPAP.Mathlib.Algebra.Order.Ring.Defs
 import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom
 import LeanAPAP.Mathlib.Data.Complex.Basic
@@ -33,9 +32,7 @@ import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.MeasureTheory.Measure.Count
 import LeanAPAP.Mathlib.Order.CompleteLattice
-import LeanAPAP.Mathlib.Order.Filter.Basic
 import LeanAPAP.Mathlib.Order.Hom.Basic
-import LeanAPAP.Mathlib.Order.LiminfLimsup
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
deleted file mode 100644
index 20004ebe35..0000000000
--- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
+++ /dev/null
@@ -1,115 +0,0 @@
-import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
-
-/-!
-# TODO
-
-Turn `ENNReal.coe_rpow_of_nonneg` and `ENNReal.coe_rpow_of_ne_zero` around
--/
-
-namespace ENNReal
-
--- TODO: Replace `toNNReal_rpow`
-@[simp] lemma toNNReal_rpow' (x : ℝ≥0∞) (z : ℝ) : (x ^ z).toNNReal = x.toNNReal ^ z :=
-  (toNNReal_rpow ..).symm
-
-end ENNReal
-
-namespace NNReal
-variable {x : ℝ≥0} {y : ℝ}
-
-lemma rpow_eq_zero (hy : y ≠ 0) : x ^ y = 0 ↔ x = 0 := by simp [hy]
-
-lemma rpow_natCast_mul (x : ℝ≥0) (n : ℕ) (z : ℝ) : x ^ (n * z) = (x ^ n) ^ z := by
-  rw [rpow_mul, rpow_natCast]
-
-lemma rpow_mul_natCast (x : ℝ≥0) (y : ℝ) (n : ℕ) : x ^ (y * n) = (x ^ y) ^ n := by
-  rw [rpow_mul, rpow_natCast]
-
-lemma rpow_intCast_mul (x : ℝ≥0) (n : ℤ) (z : ℝ) : x ^ (n * z) = (x ^ n) ^ z := by
-  rw [rpow_mul, rpow_intCast]
-
-lemma rpow_mul_intCast (x : ℝ≥0) (y : ℝ) (n : ℤ) : x ^ (y * n) = (x ^ y) ^ n := by
-  rw [rpow_mul, rpow_intCast]
-
-lemma rpow_add_intCast (hx : x ≠ 0) (y : ℝ) (n : ℤ) : x ^ (y + n) = x ^ y * x ^ n := by
-  ext; exact Real.rpow_add_intCast (mod_cast hx) _ _
-
-lemma rpow_add_natCast (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y + n) = x ^ y * x ^ n := by
-  ext; exact Real.rpow_add_natCast (mod_cast hx) _ _
-
-lemma rpow_sub_intCast (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y - n) = x ^ y / x ^ n := by
-  ext; exact Real.rpow_sub_intCast (mod_cast hx) _ _
-
-lemma rpow_sub_natCast (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y - n) = x ^ y / x ^ n := by
-  ext; exact Real.rpow_sub_natCast (mod_cast hx) _ _
-
-lemma rpow_add_intCast' {n : ℤ} (h : y + n ≠ 0) (x : ℝ≥0) : x ^ (y + n) = x ^ y * x ^ n := by
-  ext; exact Real.rpow_add_intCast' (mod_cast x.2) h
-
-lemma rpow_add_natCast' {n : ℕ} (h : y + n ≠ 0) (x : ℝ≥0) : x ^ (y + n) = x ^ y * x ^ n := by
-  ext; exact Real.rpow_add_natCast' (mod_cast x.2) h
-
-lemma rpow_sub_intCast' {n : ℤ} (h : y - n ≠ 0) (x : ℝ≥0) : x ^ (y - n) = x ^ y / x ^ n := by
-  ext; exact Real.rpow_sub_intCast' (mod_cast x.2) h
-
-lemma rpow_sub_natCast' {n : ℕ} (h : y - n ≠ 0) (x : ℝ≥0) : x ^ (y - n) = x ^ y / x ^ n := by
-  ext; exact Real.rpow_sub_natCast' (mod_cast x.2) h
-
-lemma rpow_add_one (hx : x ≠ 0) (y : ℝ) : x ^ (y + 1) = x ^ y * x := by
-  simpa using rpow_add_natCast hx y 1
-
-lemma rpow_sub_one (hx : x ≠ 0) (y : ℝ) : x ^ (y - 1) = x ^ y / x := by
-  simpa using rpow_sub_natCast hx y 1
-
--- TODO: Swap argument order to `rpow_add'`/`rpow_sub'`
-lemma rpow_add_one' (h : y + 1 ≠ 0) (x : ℝ≥0) : x ^ (y + 1) = x ^ y * x := by
-  rw [rpow_add' x h, rpow_one]
-
-lemma rpow_one_add' (h : 1 + y ≠ 0) (x : ℝ≥0) : x ^ (1 + y) = x * x ^ y := by
-  rw [rpow_add' x h, rpow_one]
-
-lemma rpow_sub_one' (h : y - 1 ≠ 0) (x : ℝ≥0) : x ^ (y - 1) = x ^ y / x := by
-  rw [rpow_sub' x h, rpow_one]
-
-lemma rpow_one_sub' (h : 1 - y ≠ 0) (x : ℝ≥0) : x ^ (1 - y) = x / x ^ y := by
-  rw [rpow_sub' x h, rpow_one]
-
-variable {x y : ℝ≥0} {z : ℝ}
-
-lemma rpow_lt_rpow_of_neg (hx : 0 < x) (hxy : x < y) (hz : z < 0) : y ^ z < x ^ z :=
-  Real.rpow_lt_rpow_of_neg hx hxy hz
-
-lemma rpow_le_rpow_of_nonpos (hx : 0 < x) (hxy : x ≤ y) (hz : z ≤ 0) : y ^ z ≤ x ^ z :=
-  Real.rpow_le_rpow_of_nonpos hx hxy hz
-
-lemma rpow_lt_rpow_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x ^ z < y ^ z ↔ y < x :=
-  Real.rpow_lt_rpow_iff_of_neg hx hy hz
-
-lemma rpow_le_rpow_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x ^ z ≤ y ^ z ↔ y ≤ x :=
-  Real.rpow_le_rpow_iff_of_neg hx hy hz
-
-lemma le_rpow_inv_iff_of_pos (hy : 0 ≤ y) (hz : 0 < z) (x : ℝ≥0) : x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y :=
-  Real.le_rpow_inv_iff_of_pos x.2 hy hz
-
-lemma rpow_inv_le_iff_of_pos (hy : 0 ≤ y) (hz : 0 < z) (x : ℝ≥0) : x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z :=
-  Real.rpow_inv_le_iff_of_pos x.2 hy hz
-
-lemma lt_rpow_inv_iff_of_pos (hy : 0 ≤ y) (hz : 0 < z) (x : ℝ≥0) : x < y ^ z⁻¹ ↔ x ^ z < y :=
-  Real.lt_rpow_inv_iff_of_pos x.2 hy hz
-
-lemma rpow_inv_lt_iff_of_pos (hy : 0 ≤ y) (hz : 0 < z) (x : ℝ≥0) : x ^ z⁻¹ < y ↔ x < y ^ z :=
-  Real.rpow_inv_lt_iff_of_pos x.2 hy hz
-
-lemma le_rpow_inv_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z :=
-  Real.le_rpow_inv_iff_of_neg hx hy hz
-
-lemma lt_rpow_inv_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x < y ^ z⁻¹ ↔ y < x ^ z :=
-  Real.lt_rpow_inv_iff_of_neg hx hy hz
-
-lemma rpow_inv_lt_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x ^ z⁻¹ < y ↔ y ^ z < x :=
-  Real.rpow_inv_lt_iff_of_neg hx hy hz
-
-lemma rpow_inv_le_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x :=
-  Real.rpow_inv_le_iff_of_neg hx hy hz
-
-end NNReal
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean
index fd83b98ab2..5f1fc2451f 100644
--- a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean
+++ b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean
@@ -1,7 +1,6 @@
 import Mathlib.MeasureTheory.Function.EssSup
 import Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.MeasureTheory.Measure.Count
-import LeanAPAP.Mathlib.Order.LiminfLimsup
 
 open Filter MeasureTheory ProbabilityTheory
 open scoped ENNReal
diff --git a/LeanAPAP/Mathlib/Order/Filter/Basic.lean b/LeanAPAP/Mathlib/Order/Filter/Basic.lean
deleted file mode 100644
index 9c1f20ac23..0000000000
--- a/LeanAPAP/Mathlib/Order/Filter/Basic.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-import Mathlib.Order.Filter.Basic
-
-namespace Filter
-variable {α β : Type*} {f g : α → β}
-
-@[simp] lemma eventuallyEq_top : f =ᶠ[⊤] g ↔ f = g := by simp [EventuallyEq, funext_iff]
-
-end Filter
diff --git a/LeanAPAP/Mathlib/Order/LiminfLimsup.lean b/LeanAPAP/Mathlib/Order/LiminfLimsup.lean
deleted file mode 100644
index da2a6987c7..0000000000
--- a/LeanAPAP/Mathlib/Order/LiminfLimsup.lean
+++ /dev/null
@@ -1,14 +0,0 @@
-import Mathlib.Order.LiminfLimsup
-
-open Set
-
-namespace Filter
-variable {α β : Type*} [ConditionallyCompleteLattice α] {u : β → α} {s : Set α}
-
-lemma limsup_top_eq_ciSup [Nonempty β] (hu : BddAbove (range u)) : limsup u ⊤ = ⨆ i, u i := by
-  rw [limsup, map_top, limsSup_principal hu (range_nonempty _), sSup_range]
-
-lemma liminf_top_eq_ciInf [Nonempty β] (hu : BddBelow (range u)) : liminf u ⊤ = ⨅ i, u i := by
-  rw [liminf, map_top, limsInf_principal hu (range_nonempty _), sInf_range]
-
-end Filter
diff --git a/LeanAPAP/Prereqs/LpNorm/Compact.lean b/LeanAPAP/Prereqs/LpNorm/Compact.lean
index ffc8558026..8ce3b62686 100644
--- a/LeanAPAP/Prereqs/LpNorm/Compact.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Compact.lean
@@ -3,7 +3,6 @@ import Mathlib.Data.Finset.Density
 import Mathlib.Data.Fintype.Order
 import Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
-import LeanAPAP.Mathlib.Order.Filter.Basic
 import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Expect.Order
 import LeanAPAP.Prereqs.Function.Translate
diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
index 4a7ec98b66..dda2b05ffb 100644
--- a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
@@ -1,6 +1,5 @@
 import Mathlib.Data.Fintype.Order
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
-import LeanAPAP.Mathlib.Order.Filter.Basic
 import LeanAPAP.Prereqs.NNLpNorm
 
 /-!
diff --git a/LeanAPAP/Prereqs/NNLpNorm.lean b/LeanAPAP/Prereqs/NNLpNorm.lean
index 298f84f04f..d42b1b9348 100644
--- a/LeanAPAP/Prereqs/NNLpNorm.lean
+++ b/LeanAPAP/Prereqs/NNLpNorm.lean
@@ -2,7 +2,6 @@ import Mathlib.Analysis.Normed.Group.Constructions
 import Mathlib.MeasureTheory.Integral.Bochner
 import Mathlib.Tactic.Positivity.Finset
 import LeanAPAP.Mathlib.Algebra.Order.Module.Rat
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Prereqs.Expect.Basic
 
diff --git a/lake-manifest.json b/lake-manifest.json
index f763bea03b..d4ca8068f8 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8feac540abb781cb1349688c816dc02fae66b49c",
+   "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e291aa4de57079b3d2199b9eb7b4b00922b85a7c",
+   "rev": "e5e4f1e9385f5a636cd95f7b5833d9ba7907115c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3e96ea03edd48b932566ca9b201285ae2d57130d",
+   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "57e84d671a0d63a14c1ccd2bcdfe43bccb5fe6ab",
+   "rev": "4b83244f3ea8cf1ebc70f68bc5b94691e826c827",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "09aca1c90e4f75b286d955e1c57b2df75ae51948",
+   "rev": "1b0072fea2aa6a0ef8ef8b506ec5223b184cb4d0",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",