diff --git a/Mathlib/Data/List/Join.lean b/Mathlib/Data/List/Join.lean
index 4dca53b75a0e0..4f1c1ffe1fb39 100644
--- a/Mathlib/Data/List/Join.lean
+++ b/Mathlib/Data/List/Join.lean
@@ -52,7 +52,7 @@ theorem join_filter_isEmpty_eq_false [DecidablePred fun l : List α => l.isEmpty
   | [] :: L => by
       simp [join_filter_isEmpty_eq_false (L := L), isEmpty_iff_eq_nil]
   | (a :: l) :: L => by
-      simp [join_filter_isEmpty_eq_false (L := L), isEmpty_cons]
+      simp [join_filter_isEmpty_eq_false (L := L)]
 #align list.join_filter_empty_eq_ff List.join_filter_isEmpty_eq_false
 
 @[simp]
diff --git a/Mathlib/Tactic/Widget/Calc.lean b/Mathlib/Tactic/Widget/Calc.lean
index 634be8df3c637..0e2a1c8d4b2cf 100644
--- a/Mathlib/Tactic/Widget/Calc.lean
+++ b/Mathlib/Tactic/Widget/Calc.lean
@@ -137,6 +137,6 @@ elab_rules : tactic
     let json := open scoped Std.Json in json% {"replaceRange": $(replaceRange),
                                                         "isFirst": $(isFirst),
                                                         "indent": $(indent)}
-    ProofWidgets.savePanelWidgetInfo proofTerm `CalcPanel (pure json)
+    Widget.savePanelWidgetInfo CalcPanel.javascriptHash (pure json) proofTerm
     isFirst := false
   evalCalc (← `(tactic|calc%$calcstx $stx))
diff --git a/Mathlib/Tactic/Widget/Congrm.lean b/Mathlib/Tactic/Widget/Congrm.lean
index abf8365734b0f..9095c828b36ae 100644
--- a/Mathlib/Tactic/Widget/Congrm.lean
+++ b/Mathlib/Tactic/Widget/Congrm.lean
@@ -51,4 +51,5 @@ open scoped Json in
 subexpressions in the goal.-/
 elab stx:"congrm?" : tactic => do
   let some replaceRange := (← getFileMap).rangeOfStx? stx | return
-  savePanelWidgetInfo stx ``CongrmSelectionPanel $ pure $ json% { replaceRange: $(replaceRange) }
+  Widget.savePanelWidgetInfo CongrmSelectionPanel.javascriptHash
+    (pure $ json% { replaceRange: $(replaceRange) }) stx
diff --git a/Mathlib/Tactic/Widget/Conv.lean b/Mathlib/Tactic/Widget/Conv.lean
index aa268c2bdcdf2..aabc847b6ac06 100644
--- a/Mathlib/Tactic/Widget/Conv.lean
+++ b/Mathlib/Tactic/Widget/Conv.lean
@@ -133,4 +133,5 @@ open scoped Json in
 in the goal.-/
 elab stx:"conv?" : tactic => do
   let some replaceRange := (← getFileMap).rangeOfStx? stx | return
-  savePanelWidgetInfo stx ``ConvSelectionPanel $ pure $ json% { replaceRange: $(replaceRange) }
+  Widget.savePanelWidgetInfo ConvSelectionPanel.javascriptHash
+   (pure $ json% { replaceRange: $(replaceRange) }) stx
diff --git a/Mathlib/Tactic/Widget/Gcongr.lean b/Mathlib/Tactic/Widget/Gcongr.lean
index df7ce0c32a9c9..f4fb3cc4788f6 100644
--- a/Mathlib/Tactic/Widget/Gcongr.lean
+++ b/Mathlib/Tactic/Widget/Gcongr.lean
@@ -49,4 +49,5 @@ open scoped Json in
 subexpressions in the goal.-/
 elab stx:"gcongr?" : tactic => do
   let some replaceRange := (← getFileMap).rangeOfStx? stx | return
-  savePanelWidgetInfo stx ``GCongrSelectionPanel $ pure $ json% { replaceRange: $(replaceRange) }
+  Widget.savePanelWidgetInfo GCongrSelectionPanel.javascriptHash
+    (pure $ json% { replaceRange: $(replaceRange) }) stx
diff --git a/lake-manifest.json b/lake-manifest.json
index bfa77660582b7..770a08b2e6eb6 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "49b36f282e56ce9a695923e2df156cd4abf33fc8",
+   "rev": "4165f2c46b6dffcca0abbacb1cea2dafa1282166",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "bump/v4.5.0",
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
+   "rev": "bf61e90de075abfa27f638922e7aafafdce77c44",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.23",
+   "inputRev": "v0.0.24-pre2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
diff --git a/lakefile.lean b/lakefile.lean
index e4aa94ed240b3..7070f27f49d7d 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -29,7 +29,7 @@ require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 require std from git "https://github.com/leanprover/std4" @ "bump/v4.5.0"
 require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
 require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
-require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.23"
+require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.24-pre2"
 require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
 
 /-!
diff --git a/lean-toolchain b/lean-toolchain
index 2dfbd8295af30..ab0fdcb8b0063 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-12-19
+leanprover/lean4:nightly-2023-12-21