Commit 2026-10-21 14:10 a2f40e9c

View on Github →

chore: bump ProofWidgets to v0.0.118 (#45113) This PR bumps ProofWidgets and adjusts usages of ProofWidgets.Html which is now protected.

Estimated changes

Modified Mathlib/Tactic/ClickSuggestions.lean

Modified Mathlib/Tactic/ClickSuggestions/SectionState.lean

modified def Mathlib.Tactic.ClickSuggestions.renderSection

Modified Mathlib/Tactic/ClickSuggestions/TryPremises.lean

Modified Mathlib/Tactic/ClickSuggestions/Unfold.lean

Modified Mathlib/Tactic/ClickSuggestions/Util.lean

modified def Mathlib.Tactic.ClickSuggestions.Premise.toHtml

modified def Mathlib.Tactic.ClickSuggestions.constToHtml

modified def Mathlib.Tactic.ClickSuggestions.exprToHtml

modified def Mathlib.Tactic.ClickSuggestions.formatToHtmlWithDoc

modified def Mathlib.Tactic.ClickSuggestions.mkSuggestion

modified def Mathlib.Tactic.ClickSuggestions.tacticToHtml

Modified Mathlib/Tactic/Widget/CommDiag.lean

modified def Mathlib.Tactic.Widget.commSquareM?

modified def Mathlib.Tactic.Widget.commTriangleM?

modified def Mathlib.Tactic.Widget.mkCommDiag

Modified Mathlib/Tactic/Widget/LibraryRewrite.lean

modified def Mathlib.Tactic.LibraryRewrite.rpc

Modified Mathlib/Tactic/Widget/SelectPanelUtils.lean

Modified Mathlib/Tactic/Widget/StringDiagram.lean

modified def Mathlib.Tactic.Widget.StringDiagram.mkEqHtml

modified def Mathlib.Tactic.Widget.StringDiagram.rpc

modified def Mathlib.Tactic.Widget.StringDiagram.stringEqM?

modified def Mathlib.Tactic.Widget.StringDiagram.stringM?

modified def Mathlib.Tactic.Widget.StringDiagram.stringMorOrEqM?

Modified MathlibTest/ClickSuggestions/TestImpl.lean

Modified lake-manifest.json