{α : Type u} →
  [toCommRing : Lean.Grind.CommRing α] →
    [toInv : Inv α] →
      [toDiv : Div α] →
        [zpow : HPow α ℤ α] →
          (∀ (a b : α), a / b = a * b⁻¹) →
            0 ≠ 1 →
              0⁻¹ = 0 →
                (∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1) →
                  (∀ (a : α), a ^ 0 = 1) →
                    (∀ (a : α) (n : ℕ), a ^ (↑n + 1) = a ^ ↑n * a) →
                      (∀ (a : α) (n : ℤ), a ^ (-n) = (a ^ n)⁻¹) → Lean.Grind.Field α