(motive : Mathlib.Linter.Flexible.Stained✝ → Mathlib.Linter.Flexible.Stained✝ → Sort u_1) →
  (x x_1 : Mathlib.Linter.Flexible.Stained✝¹) →
    ((a b : Lean.Name) → motive (Mathlib.Linter.Flexible.Stained.name✝ a) (Mathlib.Linter.Flexible.Stained.name✝¹ b)) →
      ((a : Lean.Name) → motive (Mathlib.Linter.Flexible.Stained.name✝² a) Mathlib.Linter.Flexible.Stained.goal✝) →
        ((a : Lean.Name) →
            motive (Mathlib.Linter.Flexible.Stained.name✝³ a) Mathlib.Linter.Flexible.Stained.wildcard✝) →
          ((a : Lean.Name) → motive Mathlib.Linter.Flexible.Stained.goal✝¹ (Mathlib.Linter.Flexible.Stained.name✝⁴ a)) →
            (Unit → motive Mathlib.Linter.Flexible.Stained.goal✝² Mathlib.Linter.Flexible.Stained.goal✝³) →
              (Unit → motive Mathlib.Linter.Flexible.Stained.goal✝⁴ Mathlib.Linter.Flexible.Stained.wildcard✝¹) →
                ((a : Lean.Name) →
                    motive Mathlib.Linter.Flexible.Stained.wildcard✝² (Mathlib.Linter.Flexible.Stained.name✝⁵ a)) →
                  (Unit → motive Mathlib.Linter.Flexible.Stained.wildcard✝³ Mathlib.Linter.Flexible.Stained.goal✝⁵) →
                    (Unit →
                        motive Mathlib.Linter.Flexible.Stained.wildcard✝⁴ Mathlib.Linter.Flexible.Stained.wildcard✝⁵) →
                      motive x x_1