diff --git a/SciLean.lean b/SciLean.lean
index 98837305..b7903553 100644
--- a/SciLean.lean
+++ b/SciLean.lean
@@ -8,6 +8,8 @@ import SciLean.Modules.DifferentialEquations
 
 import SciLean.Tactic.LSimp2.Elab
 
+import SciLean.Util.Profile
+
 /-!
 
 SciLean
diff --git a/SciLean/Core/Monads/StateT.lean b/SciLean/Core/Monads/StateT.lean
index 9756f1cd..12e4d937 100644
--- a/SciLean/Core/Monads/StateT.lean
+++ b/SciLean/Core/Monads/StateT.lean
@@ -113,30 +113,30 @@ by
   ftrans
 
 
--- setThe ----------------------------------------------------------------------
---------------------------------------------------------------------------------
-
-@[fprop]
-theorem _root_.setThe.arg_s.IsDifferentiableM_rule
-  (s : X → S) (ha0 : IsDifferentiable K s)
-  : IsDifferentiableM K (m:=StateT S m) (fun x => setThe S (s x)) := 
-by 
-  simp[setThe, set, StateT.set, IsDifferentiableValM, IsDifferentiableM]
-  fprop
-
-
-@[ftrans]
-theorem _root_.setThe.arg_s.fwdDerivM_rule
-  (s : X → S) (hs : IsDifferentiable K s)
-  : fwdDerivM K (m:=StateT S m) (fun x => setThe S (s x))
-    = 
-    (fun x dx => do
-      let sds := fwdCDeriv K s x dx
-      setThe _ sds
-      pure ((),())) :=
-by 
-  simp[setThe, set, StateT.set,fwdDerivM,bind,Bind.bind, StateT.bind]
-  ftrans; congr
+-- -- setThe ----------------------------------------------------------------------
+-- --------------------------------------------------------------------------------
+
+-- @[fprop]
+-- theorem _root_.setThe.arg_s.IsDifferentiableM_rule
+--   (s : X → S) (ha0 : IsDifferentiable K s)
+--   : IsDifferentiableM K (m:=StateT S m) (fun x => setThe S (s x)) := 
+-- by 
+--   simp[setThe, set, StateT.set, IsDifferentiableValM, IsDifferentiableM]
+--   fprop
+
+
+-- @[ftrans]
+-- theorem _root_.setThe.arg_s.fwdDerivM_rule
+--   (s : X → S) (hs : IsDifferentiable K s)
+--   : fwdDerivM K (m:=StateT S m) (fun x => setThe S (s x))
+--     = 
+--     (fun x dx => do
+--       let sds := fwdCDeriv K s x dx
+--       setThe _ sds
+--       pure ((),())) :=
+-- by 
+--   simp[setThe, set, StateT.set,fwdDerivM,bind,Bind.bind, StateT.bind]
+--   ftrans; congr
 
 
 -- MonadStateOf.set ------------------------------------------------------------
@@ -305,7 +305,7 @@ theorem _root_.getThe.arg.revDerivValM_rule
     (do
       pure ((← getThe S), fun ds => modifyThe S (fun ds' => ds + ds'))) := 
 by 
-  simp[getThe, MonadStateOf.get, StateT.get,revDerivValM, revDerivM, pure, StateT.pure, bind, StateT.bind, setThe, set, StateT.set, modifyThe, modify, MonadStateOf.modifyGet, StateT.modifyGet]
+  simp[getThe, MonadStateOf.get, StateT.get,revDerivValM, revDerivM, pure, StateT.pure, bind, StateT.bind, set, StateT.set, modifyThe, modify, MonadStateOf.modifyGet, StateT.modifyGet]
   ftrans
 
 -- MonadState.get --------------------------------------------------------------
@@ -327,37 +327,37 @@ theorem _root_.MonadState.get.arg.revDerivValM_rule
     (do
       pure ((← get), fun ds => modify (fun ds' => ds + ds'))) := 
 by 
-  simp[MonadState.get, getThe, MonadStateOf.get, StateT.get,revDerivValM, revDerivM, pure, StateT.pure, bind, StateT.bind, setThe, set, StateT.set, modifyThe, modify, MonadStateOf.modifyGet, StateT.modifyGet, modifyGet]
+  simp[MonadState.get, getThe, MonadStateOf.get, StateT.get,revDerivValM, revDerivM, pure, StateT.pure, bind, StateT.bind, set, StateT.set, modifyThe, modify, MonadStateOf.modifyGet, StateT.modifyGet, modifyGet]
   ftrans
 
 
--- setThe ----------------------------------------------------------------------
---------------------------------------------------------------------------------
+-- -- setThe ----------------------------------------------------------------------
+-- --------------------------------------------------------------------------------
 
-@[fprop]
-theorem _root_.setThe.arg_s.HasAdjDiffM_rule
-  (s : X → S) (ha0 : HasAdjDiff K s)
-  : HasAdjDiffM K (m:=StateT S m) (fun x => setThe S (s x)) := 
-by 
-  simp[setThe, set, StateT.set, HasAdjDiffValM, HasAdjDiffM]
-  fprop
+-- @[fprop]
+-- theorem _root_.setThe.arg_s.HasAdjDiffM_rule
+--   (s : X → S) (ha0 : HasAdjDiff K s)
+--   : HasAdjDiffM K (m:=StateT S m) (fun x => setThe S (s x)) := 
+-- by 
+--   simp[setThe, set, StateT.set, HasAdjDiffValM, HasAdjDiffM]
+--   fprop
 
 
-@[ftrans]
-theorem _root_.setThe.arg_s.revDerivM_rule
-  (s : X → S) (hs : HasAdjDiff K s)
-  : revDerivM K (m:=StateT S m) (fun x => setThe S (s x))
-    = 
-    (fun x => do
-      let sds := revCDeriv K s x
-      pure (← setThe S sds.1,
-            fun _ => do
-              let dx := sds.2 (← getThe S)
-              setThe S 0
-              pure dx)) :=
-by 
-  simp[setThe, set, StateT.set, revDerivM, getThe, MonadStateOf.get, StateT.get, bind, StateT.bind, pure, StateT.pure]
-  ftrans
+-- @[ftrans]
+-- theorem _root_.setThe.arg_s.revDerivM_rule
+--   (s : X → S) (hs : HasAdjDiff K s)
+--   : revDerivM K (m:=StateT S m) (fun x => setThe S (s x))
+--     = 
+--     (fun x => do
+--       let sds := revCDeriv K s x
+--       pure (← setThe S sds.1,
+--             fun _ => do
+--               let dx := sds.2 (← getThe S)
+--               setThe S 0
+--               pure dx)) :=
+-- by 
+--   simp[setThe, set, StateT.set, revDerivM, getThe, MonadStateOf.get, StateT.get, bind, StateT.bind, pure, StateT.pure]
+--   ftrans
 
 
 -- MonadStateOf.set ------------------------------------------------------------
@@ -385,37 +385,37 @@ theorem _root_.MonadStateOf.set.arg_a0.revDerivM_rule
               set (0:S)
               pure dx)) :=
 by 
-  simp[setThe, set, StateT.set, revDerivM, getThe, MonadStateOf.get, StateT.get, bind, StateT.bind, pure, StateT.pure, get]
+  simp[set, StateT.set, revDerivM, getThe, MonadStateOf.get, StateT.get, bind, StateT.bind, pure, StateT.pure, get]
   ftrans
 
--- modifyThe ----------------------------------------------------------------------
---------------------------------------------------------------------------------
-
-@[fprop]
-theorem _root_.modifyThe.arg_f.HasAdjDiffM_rule
-  (f : X → S → S) (ha0 : HasAdjDiff K (fun xs : X×S => f xs.1 xs.2))
-  : HasAdjDiffM K (m:=StateT S m) (fun x => modifyThe S (f x)) := 
-by 
-  simp[modifyThe, MonadStateOf.modifyGet, StateT.modifyGet, HasAdjDiffValM, HasAdjDiffM]
-  fprop
-
-
-@[ftrans]
-theorem _root_.modifyThe.arg_f.revDerivM_rule
-  (f : X → S → S) (ha0 : HasAdjDiff K (fun xs : X×S => f xs.1 xs.2))
-  : revDerivM K (m:=StateT S m) (fun x => modifyThe S (f x))
-    = 
-    (fun x => do
-      let sdf := revCDeriv K (fun xs : X×S => f xs.1 xs.2) (x, ← getThe S)
-      setThe S sdf.1
-      pure ((),
-            fun _ => do
-              let dxs := sdf.2 (← getThe S)
-              setThe S dxs.2
-              pure dxs.1)) := 
-by 
-  simp[modifyThe, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet,revDerivM, bind, StateT.bind, getThe, MonadStateOf.get, StateT.get, setThe, set, StateT.set]
-  ftrans; congr
+-- -- modifyThe ----------------------------------------------------------------------
+-- --------------------------------------------------------------------------------
+
+-- @[fprop]
+-- theorem _root_.modifyThe.arg_f.HasAdjDiffM_rule
+--   (f : X → S → S) (ha0 : HasAdjDiff K (fun xs : X×S => f xs.1 xs.2))
+--   : HasAdjDiffM K (m:=StateT S m) (fun x => modifyThe S (f x)) := 
+-- by 
+--   simp[modifyThe, MonadStateOf.modifyGet, StateT.modifyGet, HasAdjDiffValM, HasAdjDiffM]
+--   fprop
+
+
+-- @[ftrans]
+-- theorem _root_.modifyThe.arg_f.revDerivM_rule
+--   (f : X → S → S) (ha0 : HasAdjDiff K (fun xs : X×S => f xs.1 xs.2))
+--   : revDerivM K (m:=StateT S m) (fun x => modifyThe S (f x))
+--     = 
+--     (fun x => do
+--       let sdf := revCDeriv K (fun xs : X×S => f xs.1 xs.2) (x, ← getThe S)
+--       setThe S sdf.1
+--       pure ((),
+--             fun _ => do
+--               let dxs := sdf.2 (← getThe S)
+--               setThe S dxs.2
+--               pure dxs.1)) := 
+-- by 
+--   simp[modifyThe, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet,revDerivM, bind, StateT.bind, getThe, MonadStateOf.get, StateT.get, setThe, set, StateT.set]
+--   ftrans; congr
 
 
 -- modify ----------------------------------------------------------------------
@@ -444,7 +444,7 @@ theorem _root_.modify.arg_f.revDerivM_rule
               set dxs.2
               pure dxs.1)) := 
 by 
-  simp[modifyThe, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet,revDerivM, bind, StateT.bind, getThe, MonadStateOf.get, StateT.get, setThe, set, StateT.set, get, pure, StateT.pure, modify]
+  simp[modifyThe, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet,revDerivM, bind, StateT.bind, getThe, MonadStateOf.get, StateT.get, set, StateT.set, get, pure, StateT.pure, modify]
   ftrans
 
 end RevDerivMonad
diff --git a/lake-manifest.json b/lake-manifest.json
index 5ee72c9e..dde340a4 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,26 +1,10 @@
-{"version": 5,
+{"version": 6,
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
-   {"url": "https://github.com/EdAyers/ProofWidgets4",
-    "subDir?": null,
-    "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
-    "opts": {},
-    "name": "proofwidgets",
-    "inputRev?": "v0.0.13",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/mhuisi/lean4-cli.git",
-    "subDir?": null,
-    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
-    "opts": {},
-    "name": "Cli",
-    "inputRev?": "nightly",
-    "inherited": true}},
-  {"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "96f0a9003a1032e51a21b807aa9fe772112b5816",
+    "rev": "a5516f580a31bf7ec20be84cc4fe50824cd3e35a",
     "opts": {},
     "name": "mathlib",
     "inputRev?": "master",
@@ -28,7 +12,7 @@
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
-    "rev": "81cc13c524a68d0072561dbac276cd61b65872a6",
+    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
     "opts": {},
     "name": "Qq",
     "inputRev?": "master",
@@ -36,16 +20,33 @@
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "086c98bb129ca856381d4414dc0afd6e3e4ae2ef",
+    "rev": "4f8b397237411249930791f1cba0a9d2880a02dd",
     "opts": {},
     "name": "aesop",
     "inputRev?": "master",
     "inherited": true}},
+  {"git":
+   {"url": "https://github.com/mhuisi/lean4-cli.git",
+    "subDir?": null,
+    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+    "opts": {},
+    "name": "Cli",
+    "inputRev?": "nightly",
+    "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "49353fa54abdac7221fe27f7b57a6ed9ff559d5c",
+    "rev": "f2df4ab8c0726fce3bafb73a5727336b0c3120ea",
     "opts": {},
     "name": "std",
     "inputRev?": "main",
-    "inherited": true}}]}
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/EdAyers/ProofWidgets4",
+    "subDir?": null,
+    "rev": "9f68f14df384f43b74aeb2908b97ae54a0ad9d95",
+    "opts": {},
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.17",
+    "inherited": true}}],
+ "name": "scilean"}
diff --git a/lean-toolchain b/lean-toolchain
index ea806c14..400394aa 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-08-17
+leanprover/lean4:v4.2.0-rc1