{α : Type u} →
  {motive : Lean.Grind.Field α → Sort u_1} →
    (t : Lean.Grind.Field α) →
      ([toCommRing : Lean.Grind.CommRing α] →
          [toInv : Inv α] →
            [toDiv : Div α] →
              [zpow : HPow α ℤ α] →
                (div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹) →
                  (zero_ne_one : 0 ≠ 1) →
                    (inv_zero : 0⁻¹ = 0) →
                      (mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1) →
                        (zpow_zero : ∀ (a : α), a ^ 0 = 1) →
                          (zpow_succ : ∀ (a : α) (n : ℕ), a ^ (↑n + 1) = a ^ ↑n * a) →
                            (zpow_neg : ∀ (a : α) (n : ℤ), a ^ (-n) = (a ^ n)⁻¹) →
                              motive
                                { toCommRing := toCommRing, toInv := toInv, toDiv := toDiv, zpow := zpow,
                                  div_eq_mul_inv := div_eq_mul_inv, zero_ne_one := zero_ne_one, inv_zero := inv_zero,
                                  mul_inv_cancel := mul_inv_cancel, zpow_zero := zpow_zero, zpow_succ := zpow_succ,
                                  zpow_neg := zpow_neg }) →
        motive t