(motive : Lean.Elab.Term.SyntheticMVarKind → Sort u_1) →
  (x : Lean.Elab.Term.SyntheticMVarKind) →
    ((extraErrorMsg? : Option Lean.MessageData) → motive (Lean.Elab.Term.SyntheticMVarKind.typeClass extraErrorMsg?)) →
      ((_header? : Option String) →
          (expectedType e : Lean.Expr) →
            (_f? : Option Lean.Expr) →
              (mkErrorMsg? : Option (Lean.MVarId → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MessageData)) →
                motive (Lean.Elab.Term.SyntheticMVarKind.coe _header? expectedType e _f? mkErrorMsg?)) →
        ((savedContext : Lean.Elab.Term.SavedContext) →
            motive (Lean.Elab.Term.SyntheticMVarKind.postponed savedContext)) →
          ((tacticCode : Lean.Syntax) →
              (savedContext : Lean.Elab.Term.SavedContext) →
                (kind : Lean.Elab.Term.TacticMVarKind) →
                  (delayOnMVars : Bool) →
                    motive (Lean.Elab.Term.SyntheticMVarKind.tactic tacticCode savedContext kind delayOnMVars)) →
            motive x