{motive : Batteries.CodeAction.TacticCodeActions → Sort u} →
  (t : Batteries.CodeAction.TacticCodeActions) →
    ((onAnyTactic : Array Batteries.CodeAction.TacticCodeAction) →
        (onTactic : Lean.NameMap (Array Batteries.CodeAction.TacticCodeAction)) →
          motive { onAnyTactic := onAnyTactic, onTactic := onTactic }) →
      motive t