{u : Lean.Level} →
  {α : Q(Type u)} →
    (a b : Q(«$α»)) →
      (dsα : Q(DivisionSemiring «$α»)) →
        (dα : Q(DivisionRing «$α»)) →
          (motive : ℚ × (n : Q(ℤ)) × (d : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsRat («$a» * «$b»⁻¹) «$n» «$d») → Sort u_1) →
            (__discr : ℚ × (n : Q(ℤ)) × (d : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsRat («$a» * «$b»⁻¹) «$n» «$d»)) →
              ((qa : ℚ) →
                  (na : Q(ℤ)) →
                    (da : Q(ℕ)) →
                      (pa : Q(Mathlib.Meta.NormNum.IsRat («$a» * «$b»⁻¹) «$na» «$da»)) → motive (qa, ⟨na, ⟨da, pa⟩⟩)) →
                motive __discr