{motive : Lean.Widget.EmbedFmt✝ → Sort u} →
  (t : Lean.Widget.EmbedFmt✝¹) →
    ((ctx : Lean.Elab.ContextInfo) →
        (infos : Std.TreeMap ℕ Lean.Elab.Info compare) → motive (Lean.Widget.EmbedFmt.code✝ ctx infos)) →
      ((ctx : Lean.Elab.ContextInfo) →
          (lctx : Lean.LocalContext) → (g : Lean.MVarId) → motive (Lean.Widget.EmbedFmt.goal✝ ctx lctx g)) →
        ((wi : Lean.Widget.WidgetInstance) → (alt : Std.Format) → motive (Lean.Widget.EmbedFmt.widget✝ wi alt)) →
          ((cls : Lean.Name) →
              (msg : Std.Format) →
                (collapsed : Bool) →
                  (children : Lean.Widget.StrictOrLazy (Array Std.Format) (Array Lean.MessageData)) →
                    motive (Lean.Widget.EmbedFmt.trace✝ cls msg collapsed children)) →
            motive Lean.Widget.EmbedFmt.ignoreTags✝ → motive t