diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
index 4b137e04590b..2ad00405d149 100644
--- a/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -207,7 +207,9 @@ partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent
         | .widget wi alt =>
           return .tag (.widget wi (← fmtToTT alt col)) default
         | .trace cls msg collapsed children => do
-          let col := col + tt.stripTags.length - 2
+          -- absolute column = request-level indentation (e.g. from nested lazy trace request) +
+          -- offset inside `fmt`
+          let col := indent + col
           let children ←
             match children with
               | .lazy children => pure <| .lazy ⟨{indent := col+2, children := children.map .mk}⟩