diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean
index 8890e01..3949eef 100644
--- a/Nevanlinna/partialDeriv.lean
+++ b/Nevanlinna/partialDeriv.lean
@@ -297,7 +297,7 @@ lemma partialDeriv_fderivOn
   rw [fderiv_clm_apply]
   · simp
   · convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
-    apply ContDiffOn.differentiableOn _ (Submonoid.oneLE.proof_2 ℕ∞)
+    apply ContDiffOn.differentiableOn _ (Preorder.le_refl 1)
     exact ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 hf).2
   · simp
 
@@ -407,7 +407,7 @@ theorem partialDeriv_comm
     let f'' := (fderiv ℝ f' z)
     have h₁ : HasFDerivAt f' f'' z := by
       apply DifferentiableAt.hasFDerivAt
-      apply (contDiff_succ_iff_fderiv.1 h).right.differentiable (Submonoid.oneLE.proof_2 ℕ∞)
+      apply (contDiff_succ_iff_fderiv.1 h).right.differentiable (Preorder.le_refl 1)
 
     apply second_derivative_symmetric h₀ h₁ v₁ v₂
 
@@ -441,7 +441,7 @@ theorem partialDeriv_commOn
     have h₁ : HasFDerivAt f' f'' z := by
       apply DifferentiableAt.hasFDerivAt
       apply DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
-      apply ContDiffOn.differentiableOn _ (Submonoid.oneLE.proof_2 ℕ∞)
+      apply ContDiffOn.differentiableOn _ (Preorder.le_refl 1)
       exact ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 h).2
 
     have h₀' : ∀ᶠ (y : E) in nhds z, HasFDerivAt f (f' y) y := by
diff --git a/lake-manifest.json b/lake-manifest.json
index a1cb342..2c44ff7 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d747f070e42dd21e2649b75090f5b0d45c6ec8e0",
+   "rev": "8feac540abb781cb1349688c816dc02fae66b49c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
+   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
+   "rev": "e291aa4de57079b3d2199b9eb7b4b00922b85a7c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
+   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.41",
+   "inputRev": "v0.0.42",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
+   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cae1b27ace5330f372b57f1051e228fe9b264d57",
+   "rev": "8c811c94af285516e8c76a63165c87027f18ccd0",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/lean-toolchain b/lean-toolchain
index e7a4f40..98556ba 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.11.0-rc2
+leanprover/lean4:v4.12.0-rc1