fix(client): show Lean error messages in typewriter mode

[fushanbobfan]

What was wrong

Since #492, a failing tactic in typewriter mode shows "Failed command: rw [x]" but no error message, so the player does not see why it failed. This is the should show error message when using invalid tactic call test in cypress/e2e/game-features.cy.ts, which has failed on Linux and macOS on main since #492 (it passed on the run before it, 2026-09-16).

The diagnostic does reach the client: it is in the step's diags. Error.tsx turns the message into text with TaggedText_stripTags, which only keeps the text under a tag and drops the MsgEmbed itself. Lean sends most of a message's text inside expr embeds, e.g.

{"append":[{"tag":[{"expr":{"text":"Invalid rewrite argument: Expected an equality or iff proof or definition name, but"}},{"text":""}]}, ...]}

so the string comes out empty and Error renders nothing.

What this changes

Adds messageToString in client/src/components/editor/messages/Error.tsx, which reads the text out of expr, goal, widget (its alt) and trace (its msg) embeds, and uses it in place of TaggedText_stripTags. The "unsolved goals" handling is unchanged. The player now sees e.g.

Invalid rewrite argument: Expected an equality or iff proof or definition name, but `x` is a value of type
  Nat

How it was tested

Cypress on Windows (Electron, dev server via npm start). Running the editor on Windows needs the change from #567, so I tested this on main plus #567:

• game-features.cy.ts: should show error message when using invalid tactic call fails without this change and passes with it (18 of 20 passing after). In the run without the change, should not change language of hints to selected language if translation is not available also failed once; it passed in every later run.
• 01-basic-interface.cy.ts: 6/6 passing.
• Still failing, with and without this change: should show goal and hint in editor mode ("Current Goal") and should show unsolved goals only in editor mode. Both look for editor-mode infoview content, which Refactor: eliminate old infoview implementations #492 lists as still to do, so I left them alone.
• npm run build:client succeeds; tsc reports no errors in Error.tsx.