{u : Lean.Level} →
  {α : Q(Type u)} →
    (m exp : Q(ℕ)) →
      (dα : Q(DivisionRing «$α»)) →
        (motive :
            Option
                (ℚ ×
                  (n : Q(ℕ)) ×
                    (d : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNNRat (↑(mkRat (↑«$m») (10 ^ «$exp»))) «$n» «$d»)) →
              Sort u_1) →
          (x :
              Option
                (ℚ ×
                  (n : Q(ℕ)) ×
                    (d : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNNRat (↑(mkRat (↑«$m») (10 ^ «$exp»))) «$n» «$d»))) →
            ((q : ℚ) →
                (n d : Q(ℕ)) →
                  (p : Q(Mathlib.Meta.NormNum.IsNNRat (↑(mkRat (↑«$m») (10 ^ «$exp»))) «$n» «$d»)) →
                    motive (some (q, ⟨n, ⟨d, p⟩⟩))) →
              ((x :
                    Option
                      (ℚ ×
                        (n : Q(ℕ)) ×
                          (d : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNNRat (↑(mkRat (↑«$m») (10 ^ «$exp»))) «$n» «$d»))) →
                  motive x) →
                motive x