{α : Type u} →
  {motive : Lean.Grind.Ring α → Sort u_1} →
    (t : Lean.Grind.Ring α) →
      ([toSemiring : Lean.Grind.Semiring α] →
          [toNeg : Neg α] →
            [toSub : Sub α] →
              [intCast : IntCast α] →
                [zsmul : SMul ℤ α] →
                  (neg_add_cancel : ∀ (a : α), -a + a = 0) →
                    (sub_eq_add_neg : ∀ (a b : α), a - b = a + -b) →
                      (neg_zsmul : ∀ (i : ℤ) (a : α), -i • a = -(i • a)) →
                        (zsmul_natCast_eq_nsmul : ∀ (n : ℕ) (a : α), ↑n • a = n • a) →
                          (intCast_ofNat : ∀ (n : ℕ), ↑(OfNat.ofNat n) = OfNat.ofNat n) →
                            (intCast_neg : ∀ (i : ℤ), ↑(-i) = -↑i) →
                              motive
                                { toSemiring := toSemiring, toNeg := toNeg, toSub := toSub, intCast := intCast,
                                  zsmul := zsmul, neg_add_cancel := neg_add_cancel, sub_eq_add_neg := sub_eq_add_neg,
                                  neg_zsmul := neg_zsmul, zsmul_natCast_eq_nsmul := zsmul_natCast_eq_nsmul,
                                  intCast_ofNat := intCast_ofNat, intCast_neg := intCast_neg }) →
        motive t