(v : Lean.Level) →
  (α : Q(Type v)) →
    (ipo : Q(PartialOrder «$α»)) →
      (a b : Q(«$α»)) →
        (motive : Except Mathlib.Tactic.Ring.ExceptType Q(«$a» < «$b») → Sort u_1) →
          (__do_lift : Except Mathlib.Tactic.Ring.ExceptType Q(«$a» < «$b»)) →
            ((p : Q(«$a» < «$b»)) → motive (Except.ok p)) →
              ((e : Mathlib.Tactic.Ring.ExceptType) → motive (Except.error e)) → motive __do_lift