{motive : Mathlib.Linter.Flexible.StainData✝ → Sort u} →
  (t : Mathlib.Linter.Flexible.StainData✝¹) →
    ((stained : Mathlib.Linter.Flexible.Stained✝) →
        (stx : Lean.Syntax) →
          (ci : Lean.Elab.ContextInfo) →
            (mctx : Lean.MetavarContext) →
              (goals : List Lean.MVarId) →
                motive { stained := stained, stx := stx, ci := ci, mctx := mctx, goals := goals }) →
      motive t