chore: revert ProofWidgets bump in #7044 and #7056 (#7069)

The cache is broken after #7044 and #7056, so I am reverting them. (And merging directly, rather than via bors.)

Mathlib/Tactic/Widget/CommDiag.lean

@@ -8,7 +8,7 @@ import Mathlib.CategoryTheory.Category.Basic
 
 import ProofWidgets.Component.PenroseDiagram
 import ProofWidgets.Presentation.Expr
-import ProofWidgets.Component.Panel.SelectionPanel
+import ProofWidgets.Component.SelectionPanel
 
 /-! This module defines tactic/meta infrastructure for displaying commutative diagrams in the
 infoview. -/
@@ -58,13 +58,13 @@ open scoped Jsx in
 display as labels in the diagram. -/
 def mkCommDiag (sub : String) (embeds : ExprEmbeds) : MetaM Html := do
   let embeds ← embeds.mapM fun (s, h) =>
-      return (s, <InteractiveCode fmt={← Widget.ppExprTagged h} />)
-  return (
+      return (s, Html.ofTHtml <InteractiveCode fmt={← Widget.ppExprTagged h} />)
+  return Html.ofTHtml
     <PenroseDiagram
       embeds={embeds}
       dsl={include_str ".."/".."/".."/"widget"/"src"/"penrose"/"commutative.dsl"}
       sty={include_str ".."/".."/".."/"widget"/"src"/"penrose"/"commutative.sty"}
-      sub={sub} />)
+      sub={sub} />
 
 /-! ## Commutative triangles -/
 

lake-manifest.json

@@ -4,10 +4,10 @@
  [{"git":
    {"url": "https://github.com/EdAyers/ProofWidgets4",
     "subDir?": null,
-    "rev": "44e6673a20fc0449d003983d1e1f472df40f7107",
+    "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
     "opts": {},
     "name": "proofwidgets",
-    "inputRev?": "v0.0.15",
+    "inputRev?": "v0.0.13",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",

lakefile.lean

@@ -44,7 +44,7 @@ require std from git "https://github.com/leanprover/std4" @ "main"
 require Qq from git "https://github.com/gebner/quote4" @ "master"
 require aesop from git "https://github.com/JLimperg/aesop" @ "master"
 require Cli from git "https://github.com/mhuisi/lean4-cli.git" @ "nightly"
-require proofwidgets from git "https://github.com/EdAyers/ProofWidgets4" @ "v0.0.15"
+require proofwidgets from git "https://github.com/EdAyers/ProofWidgets4" @ "v0.0.13"
 
 lean_lib Cache where
   moreLeanArgs := moreLeanArgs

test/CommDiag.lean

@@ -1,5 +1,5 @@
 import Mathlib.Tactic.Widget.CommDiag
-import ProofWidgets.Component.Panel.GoalTypePanel
+import ProofWidgets.Component.GoalTypePanel
 
 /-! ## Example use of commutative diagram widgets -/