(motive : Lean.NamingContext → Option Lean.MessageDataContext → Lean.MessageData → Sort u_1) →
  (x : Lean.NamingContext) →
    (x_1 : Option Lean.MessageDataContext) →
      (x_2 : Lean.MessageData) →
        ((x : Lean.NamingContext) →
            (x_3 : Option Lean.MessageDataContext) →
              (fmt : Lean.FormatWithInfos) → motive x x_3 (Lean.MessageData.ofFormatWithInfos fmt)) →
          ((x : Lean.NamingContext) → (mvarId : Lean.MVarId) → motive x none (Lean.MessageData.ofGoal mvarId)) →
            ((nCtx : Lean.NamingContext) →
                (ctx : Lean.MessageDataContext) →
                  (mvarId : Lean.MVarId) → motive nCtx (some ctx) (Lean.MessageData.ofGoal mvarId)) →
              ((nCtx : Lean.NamingContext) →
                  (ctx : Option Lean.MessageDataContext) →
                    (a : Lean.Widget.WidgetInstance) →
                      (d : Lean.MessageData) → motive nCtx ctx (Lean.MessageData.ofWidget a d)) →
                ((nCtx : Lean.NamingContext) →
                    (x : Option Lean.MessageDataContext) →
                      (ctx : Lean.MessageDataContext) →
                        (d : Lean.MessageData) → motive nCtx x (Lean.MessageData.withContext ctx d)) →
                  ((x : Lean.NamingContext) →
                      (ctx : Option Lean.MessageDataContext) →
                        (nCtx : Lean.NamingContext) →
                          (d : Lean.MessageData) → motive x ctx (Lean.MessageData.withNamingContext nCtx d)) →
                    ((nCtx : Lean.NamingContext) →
                        (ctx : Option Lean.MessageDataContext) →
                          (a : Lean.Name) → (d : Lean.MessageData) → motive nCtx ctx (Lean.MessageData.tagged a d)) →
                      ((nCtx : Lean.NamingContext) →
                          (ctx : Option Lean.MessageDataContext) →
                            (n : ℕ) → (d : Lean.MessageData) → motive nCtx ctx (Lean.MessageData.nest n d)) →
                        ((nCtx : Lean.NamingContext) →
                            (ctx : Option Lean.MessageDataContext) →
                              (d₁ d₂ : Lean.MessageData) → motive nCtx ctx (d₁.compose d₂)) →
                          ((nCtx : Lean.NamingContext) →
                              (ctx : Option Lean.MessageDataContext) →
                                (d : Lean.MessageData) → motive nCtx ctx d.group) →
                            ((nCtx : Lean.NamingContext) →
                                (ctx : Option Lean.MessageDataContext) →
                                  (data : Lean.TraceData) →
                                    (header : Lean.MessageData) →
                                      (children : Array Lean.MessageData) →
                                        motive nCtx ctx (Lean.MessageData.trace data header children)) →
                              ((nCtx : Lean.NamingContext) →
                                  (ctx? : Option Lean.MessageDataContext) →
                                    (pp : Option Lean.PPContext → BaseIO Dynamic) →
                                      (hasSyntheticSorry : Lean.MetavarContext → Bool) →
                                        motive nCtx ctx? (Lean.MessageData.ofLazy pp hasSyntheticSorry)) →
                                motive x x_1 x_2