Commit 2025-07-05 16:16 58f56b34

fix: add whnfR in the code for the string diagram widget (#26748) Without this, the widget cannot see the expression after have line. The following example is reported on #Infinity-Cosmos > Bicategory of enriched categories @ 💬

example {C : Type} [Category C] [MonoidalCategory C]
    {D : Type} [Category D] [MonoidalCategory D]
    (F G : C ⥤ D) (α : F ⟶ G)
    {X Y : C} {Z : D} (h : α.app X = α.app X) :
    α.app X ⊗ₘ 𝟙 Z = α.app X ⊗ₘ 𝟙 Z := by
  have h' := h
  with_panel_widgets [Mathlib.Tactic.Widget.StringDiagram]
  sorry  -- "No String Diagram."