{α : Type u} →
  {P : Sort u_1} →
    {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)⁻¹} →
                          {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)⁻¹} →
                                                { 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 } =
                                                    { 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' } →
                                                  (toCommRing ≍ toCommRing' →
                                                      toInv ≍ toInv' → toDiv ≍ toDiv' → zpow ≍ zpow' → P) →
                                                    P