{u : Lean.Level} →
  {α : Q(Type u)} →
    (a : Q(«$α»)) →
      (_c : Q(DivisionSemiring «$α»)) →
        (nb : Q(ℕ)) →
          (motive : Mathlib.Meta.NormNum.Result q(«$a» ^ «$nb») → Sort u_1) →
            (__do_lift : Mathlib.Meta.NormNum.Result q(«$a» ^ «$nb»)) →
              ((val : Bool) → (proof : Lean.Expr) → motive (Mathlib.Meta.NormNum.Result'.isBool val proof)) →
                ((sα' : Q(AddMonoidWithOne «$α»)) →
                    (ne' : Q(ℕ)) →
                      (pe' : Q(Mathlib.Meta.NormNum.IsNat («$a» ^ «$nb») «$ne'»)) →
                        motive (Mathlib.Meta.NormNum.Result'.isNat sα' ne' pe')) →
                  ((sα' : Q(Ring «$α»)) →
                      (ne' : Q(ℕ)) →
                        (pe' : Q(Mathlib.Meta.NormNum.IsInt («$a» ^ «$nb») (Int.negOfNat «$ne'»))) →
                          motive (Mathlib.Meta.NormNum.Result'.isNegNat sα' ne' pe')) →
                    ((dsα' : Q(DivisionSemiring «$α»)) →
                        (qe' : ℚ) →
                          (nume' dene' : Q(ℕ)) →
                            (pe' : Q(Mathlib.Meta.NormNum.IsNNRat («$a» ^ «$nb») «$nume'» «$dene'»)) →
                              motive (Mathlib.Meta.NormNum.Result'.isNNRat dsα' qe' nume' dene' pe')) →
                      ((dα' : Q(DivisionRing «$α»)) →
                          (qe' : ℚ) →
                            (nume' dene' : Q(ℕ)) →
                              (pe' : Q(Mathlib.Meta.NormNum.IsRat («$a» ^ «$nb») (Int.negOfNat «$nume'») «$dene'»)) →
                                motive (Mathlib.Meta.NormNum.Result'.isNegNNRat dα' qe' nume' dene' pe')) →
                        motive __do_lift