(motive :
    MProd (Array (Lean.TSyntax `Lean.Parser.Term.attrInstance))
        (MProd (List ℕ)
          (MProd (Option Mathlib.Tactic.Translate.RelevantArg) (Option Mathlib.Tactic.Translate.Reorder))) →
      Sort u_1) →
  (r :
      MProd (Array (Lean.TSyntax `Lean.Parser.Term.attrInstance))
        (MProd (List ℕ)
          (MProd (Option Mathlib.Tactic.Translate.RelevantArg) (Option Mathlib.Tactic.Translate.Reorder)))) →
    ((attrs : Array (Lean.TSyntax `Lean.Parser.Term.attrInstance)) →
        (dontTranslate : List ℕ) →
          (relevantArg? : Option Mathlib.Tactic.Translate.RelevantArg) →
            (reorder? : Option Mathlib.Tactic.Translate.Reorder) →
              motive ⟨attrs, dontTranslate, relevantArg?, reorder?⟩) →
      motive r