{K : Type u} →
  {motive : Field K → Sort u_1} →
    ([toCommRing : CommRing K] →
        [toInv : Inv K] →
          [toDiv : Div K] →
            (div_eq_mul_inv : ∀ (a b : K), a / b = a * b⁻¹) →
              (zpow : ℤ → K → K) →
                (zpow_zero' : ∀ (a : K), zpow 0 a = 1) →
                  (zpow_succ' : ∀ (n : ℕ) (a : K), zpow (↑n.succ) a = zpow (↑n) a * a) →
                    (zpow_neg' : ∀ (n : ℕ) (a : K), zpow (Int.negSucc n) a = (zpow (↑n.succ) a)⁻¹) →
                      [toNontrivial : Nontrivial K] →
                        [toNNRatCast : NNRatCast K] →
                          [toRatCast : RatCast K] →
                            (mul_inv_cancel : ∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) →
                              (inv_zero : 0⁻¹ = 0) →
                                (nnratCast_def : ∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den) →
                                  (nnqsmul : ℚ≥0 → K → K) →
                                    (nnqsmul_def : ∀ (q : ℚ≥0) (a : K), nnqsmul q a = ↑q * a) →
                                      (ratCast_def : ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den) →
                                        (qsmul : ℚ → K → K) →
                                          (qsmul_def : ∀ (a : ℚ) (x : K), qsmul a x = ↑a * x) →
                                            motive
                                              { toCommRing := toCommRing, toInv := toInv, toDiv := toDiv,
                                                div_eq_mul_inv := div_eq_mul_inv, zpow := zpow,
                                                zpow_zero' := zpow_zero', zpow_succ' := zpow_succ',
                                                zpow_neg' := zpow_neg', toNontrivial := toNontrivial,
                                                toNNRatCast := toNNRatCast, toRatCast := toRatCast,
                                                mul_inv_cancel := mul_inv_cancel, inv_zero := inv_zero,
                                                nnratCast_def := nnratCast_def, nnqsmul := nnqsmul,
                                                nnqsmul_def := nnqsmul_def, ratCast_def := ratCast_def, qsmul := qsmul,
                                                qsmul_def := qsmul_def }) →
      (t : Field K) → motive t