diff --git a/LeanMachineLearning/Tactic/KernelHom/Tactic/KernelDiagram.lean b/LeanMachineLearning/Tactic/KernelHom/Tactic/KernelDiagram.lean
index a2eb3742..e755746d 100644
--- a/LeanMachineLearning/Tactic/KernelHom/Tactic/KernelDiagram.lean
+++ b/LeanMachineLearning/Tactic/KernelHom/Tactic/KernelDiagram.lean
@@ -90,7 +90,7 @@ end Mathlib.Tactic.Widget.StringDiagram
 namespace KernelDiagram
 
 /-- Given a kernel expression, return a string diagram. Otherwise `none`. -/
-def KernelM? (e : Expr) : MetaM (Option Html) := do
+def KernelM? (e : Expr) : MetaM (Option ProofWidgets.Html) := do
   let e ← instantiateMVars e
   try
     let (e, _) ← transformKernelToHom e []
@@ -120,7 +120,7 @@ def KernelM? (e : Expr) : MetaM (Option Html) := do
   catch _ => return none
 
 /-- Help function for displaying two string diagrams in an equality. -/
-def mkEqHtml (lhs rhs : Html) : Html :=
+def mkEqHtml (lhs rhs : ProofWidgets.Html) : ProofWidgets.Html :=
   jsx%{<div className="flex">
     <div className="w-50">
       <details open={true}>
@@ -136,7 +136,7 @@ def mkEqHtml (lhs rhs : Html) : Html :=
 
 /-- Given an equality between kernels, return a string diagram of the LHS and RHS.
 Otherwise `none`. -/
-def kernelEqM? (e : Expr) : MetaM (Option Html) := do
+def kernelEqM? (e : Expr) : MetaM (Option ProofWidgets.Html) := do
   try
     let e ← unfoldKernelOp <| ← instantiateMVars e
     let (lifted_e, _) ← liftEquality e
@@ -148,15 +148,15 @@ def kernelEqM? (e : Expr) : MetaM (Option Html) := do
 
 /-- Reduce a forall expression and try to display a kernel diagram
 if it is an equality of kernels. -/
-def kernelEqMReduce? (e : Expr) : MetaM (Option Html) := do
+def kernelEqMReduce? (e : Expr) : MetaM (Option ProofWidgets.Html) := do
   forallTelescopeReducing (← whnfR <| ← inferType e) fun _ expr => do
     kernelEqM? expr
 
 /-- The RPC method for displaying kernel diagrams. -/
 @[server_rpc_method]
-def rpc (props : PanelWidgetProps) : RequestM (RequestTask Html) :=
+def rpc (props : PanelWidgetProps) : RequestM (RequestTask ProofWidgets.Html) :=
   RequestM.asTask do
-    let html : Option Html ← (do
+    let html : Option ProofWidgets.Html ← (do
       if props.goals.isEmpty then
         return none
       let some g := props.goals[0]? | unreachable!
diff --git a/lake-manifest.json b/lake-manifest.json
index 5b9eb0a4..be14d92e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "625d8914199bc567cca9b91f90e8e5afafa5ae51",
+   "rev": "9d581dfff2e41de989072ea63abf3daf69311520",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "625d8914199bc567cca9b91f90e8e5afafa5ae51",
+   "inputRev": "v4.36.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f7a4dc6867f8df27778b2b320763ec9e3b7be070",
+   "rev": "71a2035b44e7f54a797ce799fd1b03cdd3a44684",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.36.0-rc1",
+   "inputRev": "v4.36.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c2d7840c65673533e15b499f25beecdc6227f7d8",
+   "rev": "129d1ba9a16bc0660f46c79e9fb041ef5d5d80de",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9d39f9bb0c30aa2f6200808805ff16e6ce950890",
+   "rev": "c61286b7b63cbfd563b28e11e81d0a18233a044a",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b3cc36c295aa5e3e3c0197b09a6556298e710447",
+   "rev": "b8cc5dd0a36233b88a6ed5a7dbf1207d09338c60",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "17137fad38a2cc782ff00b323a13c3a991d085ab",
+   "rev": "16259c0d07d61ee37d999d05b5cf96338b8daa11",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cbdde3aa2665915fb286c48bcd4cdf885c629511",
+   "rev": "7d11bfa88558f8d3d90afdf6bd877ed70001498d",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6d26f8bb4b2bb78f929ad160feac508866821316",
+   "rev": "b0256621cb88178e9ad932a53633077b3029e621",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4453b52d2468f4c346a8711d728c0742e7483c9b",
+   "rev": "d4c39b228d4a06f3b00748c2c445a7b9f056a6e3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,17 +95,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "34d2efffcb6dc8d5f3537cf6a7f88bfaa999ec49",
+   "rev": "c09cb1e4f1e6e1c231a1175a12b681b075054a1b",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.36.0-rc1",
+   "inputRev": "v4.36.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/illuminate",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d22e76ef3d2a925132315af902ea432233b4a44a",
+   "rev": "758bff3509b8e90ca82e37aa5de81de3c9e70fc0",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.toml b/lakefile.toml
index 583c54e6..366fbf69 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -12,12 +12,12 @@ weak.linter.mathlibStandardSet = true
 [[require]]
 name = "verso"
 git = "https://github.com/leanprover/verso"
-rev = "v4.36.0-rc1"
+rev = "v4.36.0-rc2"
 
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "625d8914199bc567cca9b91f90e8e5afafa5ae51"
+rev = "v4.36.0-rc2"
 
 [[lean_lib]]
 name = "LeanMachineLearning"
diff --git a/lean-toolchain b/lean-toolchain
index d0cf8c52..9b8f2683 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.36.0-rc1
\ No newline at end of file
+leanprover/lean4:v4.36.0-rc2
\ No newline at end of file