diff --git a/ProofWidgets/Component/Panel.lean b/ProofWidgets/Component/Panel.lean
index 8dfb666..5587f76 100644
--- a/ProofWidgets/Component/Panel.lean
+++ b/ProofWidgets/Component/Panel.lean
@@ -34,17 +34,17 @@ def processIdent (stx : Syntax) (nmStx : TSyntax `ident) : CoreM Unit := do
 /-- Display the selected panel widgets in the nested tactic script. For example,
 assuming we have written a `GeometryDisplay` component,
 ```lean
-by withPanelWidgets [GeometryDisplay]
+by with_panel_widgets [GeometryDisplay]
   simp
   rfl
 ```
 will show the geometry display alongside the usual tactic state throughout the proof.
 -/
-syntax (name := withPanelWidgetsTacticStx) "withPanelWidgets" "[" ident,+ "]" tacticSeq : tactic
+syntax (name := withPanelWidgetsTacticStx) "with_panel_widgets" "[" ident,+ "]" tacticSeq : tactic
 
 @[tactic withPanelWidgetsTacticStx]
 def withPanelWidgets : Tactic
-  | stx@`(tactic| withPanelWidgets [ $nms,* ] $seq) => do
+  | stx@`(tactic| with_panel_widgets [ $nms,* ] $seq) => do
     liftM <| nms.getElems.forM (processIdent stx)
     evalTacticSeq seq
   | _ => throwUnsupportedSyntax
diff --git a/ProofWidgets/Demos/ExprPresentation.lean b/ProofWidgets/Demos/ExprPresentation.lean
index 6693f83..67d1ce9 100644
--- a/ProofWidgets/Demos/ExprPresentation.lean
+++ b/ProofWidgets/Demos/ExprPresentation.lean
@@ -14,13 +14,13 @@ def presenter : ExprPresenter where
       </span>
 
 example : 2 + 2 = 4 ∧ 3 + 3 = 6 := by
-  withPanelWidgets [GoalTypePanel]
+  with_panel_widgets [GoalTypePanel]
     -- Place cursor here.
     constructor
     rfl
     rfl
 
 example (h : 2 + 2 = 5) : 2 + 2 = 4 := by
-  withPanelWidgets [SelectionPanel]
+  with_panel_widgets [SelectionPanel]
     -- Place cursor here and select subexpressions in the goal with shift-click.
     rfl
diff --git a/ProofWidgets/Demos/RbTree.lean b/ProofWidgets/Demos/RbTree.lean
index dcf6b6a..9737f6b 100644
--- a/ProofWidgets/Demos/RbTree.lean
+++ b/ProofWidgets/Demos/RbTree.lean
@@ -138,7 +138,7 @@ example {α : Type} (x y z : α) (a b c d : RBTree α)
     (h : ¬ ∃ e w f, a = node red e w f) :
     balance black (node red a x (node red b y c)) z d =
     node red (node black a x b) y (node black c z d) := by
-  withPanelWidgets [SelectionPanel]
+  with_panel_widgets [SelectionPanel]
     match a with
     | .empty => simp [balance]
     | node black .. => simp [balance]