{motive : Mathlib.Tactic.Linarith.GlobalPreprocessor → Sort u} →
  (t : Mathlib.Tactic.Linarith.GlobalPreprocessor) →
    ((toPreprocessorBase : Mathlib.Tactic.Linarith.PreprocessorBase) →
        (transform : List Lean.Expr → Lean.MetaM (List Lean.Expr)) →
          motive { toPreprocessorBase := toPreprocessorBase, transform := transform }) →
      motive t