{α : Type u} →
  {motive : Lean.Grind.Semiring α → Sort u_1} →
    ([toAdd : Add α] →
        [toMul : Mul α] →
          [natCast : NatCast α] →
            [ofNat : (n : ℕ) → OfNat α n] →
              [nsmul : SMul ℕ α] →
                [npow : HPow α ℕ α] →
                  (add_zero : ∀ (a : α), a + 0 = a) →
                    (add_comm : ∀ (a b : α), a + b = b + a) →
                      (add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)) →
                        (mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)) →
                          (mul_one : ∀ (a : α), a * 1 = a) →
                            (one_mul : ∀ (a : α), 1 * a = a) →
                              (left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c) →
                                (right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c) →
                                  (zero_mul : ∀ (a : α), 0 * a = 0) →
                                    (mul_zero : ∀ (a : α), a * 0 = 0) →
                                      (pow_zero : ∀ (a : α), a ^ 0 = 1) →
                                        (pow_succ : ∀ (a : α) (n : ℕ), a ^ (n + 1) = a ^ n * a) →
                                          (ofNat_succ : ∀ (a : ℕ), OfNat.ofNat (a + 1) = OfNat.ofNat a + 1) →
                                            (ofNat_eq_natCast : ∀ (n : ℕ), OfNat.ofNat n = ↑n) →
                                              (nsmul_eq_natCast_mul : ∀ (n : ℕ) (a : α), n • a = ↑n * a) →
                                                motive
                                                  { toAdd := toAdd, toMul := toMul, natCast := natCast, ofNat := ofNat,
                                                    nsmul := nsmul, npow := npow, add_zero := add_zero,
                                                    add_comm := add_comm, add_assoc := add_assoc,
                                                    mul_assoc := mul_assoc, mul_one := mul_one, one_mul := one_mul,
                                                    left_distrib := left_distrib, right_distrib := right_distrib,
                                                    zero_mul := zero_mul, mul_zero := mul_zero, pow_zero := pow_zero,
                                                    pow_succ := pow_succ, ofNat_succ := ofNat_succ,
                                                    ofNat_eq_natCast := ofNat_eq_natCast,
                                                    nsmul_eq_natCast_mul := nsmul_eq_natCast_mul }) →
      (t : Lean.Grind.Semiring α) → motive t