{α : Type u} →
  (add : α → α → α) →
    (∀ (a b c : α), a + b + c = a + (b + c)) →
      (zero : α) →
        (∀ (a : α), 0 + a = a) →
          (∀ (a : α), a + 0 = a) →
            (nsmul : ℕ → α → α) →
              autoParam (∀ (x : α), nsmul 0 x = 0) AddMonoid.nsmul_zero._autoParam →
                autoParam (∀ (n : ℕ) (x : α), nsmul (n + 1) x = nsmul n x + x) AddMonoid.nsmul_succ._autoParam →
                  (∀ (a b : α), a + b = b + a) →
                    (mul : α → α → α) →
                      (∀ (a b c : α), a * (b + c) = a * b + a * c) →
                        (∀ (a b c : α), (a + b) * c = a * c + b * c) →
                          (∀ (a : α), 0 * a = 0) →
                            (∀ (a : α), a * 0 = 0) →
                              (∀ (a b c : α), a * b * c = a * (b * c)) →
                                (one : α) →
                                  (∀ (a : α), 1 * a = a) →
                                    (∀ (a : α), a * 1 = a) →
                                      (natCast : ℕ → α) →
                                        autoParam (natCast 0 = 0) AddMonoidWithOne.natCast_zero._autoParam →
                                          autoParam (∀ (n : ℕ), natCast (n + 1) = natCast n + 1)
                                              AddMonoidWithOne.natCast_succ._autoParam →
                                            (npow : ℕ → α → α) →
                                              autoParam (∀ (x : α), npow 0 x = 1) Monoid.npow_zero._autoParam →
                                                autoParam (∀ (n : ℕ) (x : α), npow (n + 1) x = npow n x * x)
                                                    Monoid.npow_succ._autoParam →
                                                  (neg : α → α) →
                                                    (sub : α → α → α) →
                                                      autoParam (∀ (a b : α), a - b = a + neg b)
                                                          SubNegMonoid.sub_eq_add_neg._autoParam →
                                                        (zsmul : ℤ → α → α) →
                                                          autoParam (∀ (a : α), zsmul 0 a = 0)
                                                              SubNegMonoid.zsmul_zero'._autoParam →
                                                            autoParam
                                                                (∀ (n : ℕ) (a : α),
                                                                  zsmul (↑n.succ) a = zsmul (↑n) a + a)
                                                                SubNegMonoid.zsmul_succ'._autoParam →
                                                              autoParam
                                                                  (∀ (n : ℕ) (a : α),
                                                                    zsmul (Int.negSucc n) a = neg (zsmul (↑n.succ) a))
                                                                  SubNegMonoid.zsmul_neg'._autoParam →
                                                                (∀ (a : α), neg a + a = 0) →
                                                                  (intCast : ℤ → α) →
                                                                    autoParam (∀ (n : ℕ), intCast ↑n = ↑n)
                                                                        AddGroupWithOne.intCast_ofNat._autoParam →
                                                                      autoParam
                                                                          (∀ (n : ℕ),
                                                                            intCast (Int.negSucc n) = neg ↑(n + 1))
                                                                          AddGroupWithOne.intCast_negSucc._autoParam →
                                                                        (∀ (a b : α), a * b = b * a) → CommRing α