(u_1 : Lean.Level) →
  (α : Q(Type u_1)) →
    (x : Q(«$α»)) →
      (motive : Mathlib.Meta.NormNum.Result x → Sort u_1) →
        (__do_lift : Mathlib.Meta.NormNum.Result x) →
          ((val : Bool) → (proof : Lean.Expr) → motive (Mathlib.Meta.NormNum.Result'.isBool val proof)) →
            ((sα : Q(AddMonoidWithOne «$α»)) →
                (nb : Q(ℕ)) →
                  (pb : Q(Mathlib.Meta.NormNum.IsNat «$x» «$nb»)) →
                    motive (Mathlib.Meta.NormNum.Result'.isNat sα nb pb)) →
              ((sα : Q(Ring «$α»)) →
                  (nb : Q(ℕ)) →
                    (pb : Q(Mathlib.Meta.NormNum.IsInt «$x» (Int.negOfNat «$nb»))) →
                      motive (Mathlib.Meta.NormNum.Result'.isNegNat sα nb pb)) →
                ((dα : Q(DivisionSemiring «$α»)) →
                    (q : ℚ) →
                      (n d : Q(ℕ)) →
                        (h : Q(Mathlib.Meta.NormNum.IsNNRat «$x» «$n» «$d»)) →
                          motive (Mathlib.Meta.NormNum.Result'.isNNRat dα q n d h)) →
                  ((inst : Q(DivisionRing «$α»)) →
                      (q : ℚ) →
                        (n d : Q(ℕ)) →
                          (h : Q(Mathlib.Meta.NormNum.IsRat «$x» (Int.negOfNat «$n») «$d»)) →
                            motive (Mathlib.Meta.NormNum.Result'.isNegNNRat inst q n d h)) →
                    motive __do_lift