{motive : Mathlib.TacticAnalysis.ComplexConfig → Sort u} →
  (t : Mathlib.TacticAnalysis.ComplexConfig) →
    ((out ctx : Type) →
        (trigger : Option ctx → Lean.Syntax → Mathlib.TacticAnalysis.TriggerCondition ctx) →
          (test :
              Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → ctx → Lean.MVarId → Lean.Elab.Command.CommandElabM out) →
            (tell :
                Lean.Syntax →
                  List Lean.MVarId → ℕ → out → ℕ → Lean.Elab.Command.CommandElabM (Option Lean.MessageData)) →
              motive { out := out, ctx := ctx, trigger := trigger, test := test, tell := tell }) →
      motive t