feat: add TraceData.headerContent? for pre-emoji header access

`withTraceNodeBefore` prepends `TraceResult.toEmoji` to the header
before storing it in the trace tree. This makes it difficult for
programmatic consumers to compare headers across trace runs, since
the same check gets different emoji prefixes depending on
success/failure.

Add `headerContent? : Option MessageData` to `TraceData` that stores
the original pre-emoji header content. This is purely additive — the
emoji-prefixed header continues to be stored as before, and all
existing trace output is unchanged.

Closes #13069

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

src/Lean/Message.lean

@@ -97,6 +97,12 @@ structure TraceData where
   collapsed : Bool := true
   /-- Optional tag shown in `trace.profiler.output` output after the trace class name. -/
   tag       : String := ""
+  /-- The trace header content without the leading status emoji.
+  `withTraceNodeBefore` prepends `TraceResult.toEmoji` to the stored header message;
+  this field provides the original pre-emoji content for programmatic consumers
+  that need to compare headers across trace runs (where the same check may have
+  different emoji prefixes depending on success/failure). -/
+  headerContent? : Option MessageData := none
 
 /-- Structured message data. We use it for reporting errors, trace messages, etc. -/
 inductive MessageData where

src/Lean/Util/Trace.lean

@@ -418,8 +418,10 @@ where
       modifyTraces (oldTraces ++ ·)
       return (← MonadExcept.ofExcept res)
     let result := res.toTraceResult
+    let headerContent := msg
     let mut msg := m!"{result.toEmoji} {msg}"
-    let mut data : TraceData := { cls, collapsed, tag, result? := some result }
+    let mut data : TraceData := { cls, collapsed, tag, result? := some result,
+      headerContent? := some headerContent }
     if trace.profiler.get opts then
       data := { data with startTime := start, stopTime := stop }
     addTraceNode oldTraces data ref msg