diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 49e02e2e9a..3d3cb3fe76 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -9,7 +9,6 @@ import LeanAPAP.Mathlib.Analysis.Normed.Field.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.NNReal.Basic
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.MeasureTheory.MeasurableSpace.Defs
diff --git a/LeanAPAP/Mathlib/Data/NNReal/Basic.lean b/LeanAPAP/Mathlib/Data/NNReal/Basic.lean
deleted file mode 100644
index 30d49ef3a5..0000000000
--- a/LeanAPAP/Mathlib/Data/NNReal/Basic.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-import Mathlib.Data.NNReal.Basic
-
-namespace NNReal
-
-@[simp, norm_cast] lemma coe_nnqsmul (q : ℚ≥0) (x : ℝ≥0) : ↑(q • x) = (q • x : ℝ) := rfl
-
-end NNReal
diff --git a/lake-manifest.json b/lake-manifest.json
index 23b9f1250e..773efa8a9b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6ce4187086ef93261927bbc72d061888099b30fc",
+   "rev": "0844193bcedb553ac72342e6ac8b6ae9a5287a14",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,