Lean4
example (s : Grind.CommRing α) : CommRing α :=
{ s with
zero_add := Grind.AddCommMonoid.zero_add
right_distrib := Grind.Semiring.right_distrib
mul_zero := Grind.Semiring.mul_zero
one_mul := Grind.Semiring.one_mul
nsmul := nsmulRec
zsmul := zsmulRec
npow := npowRec
natCast := Nat.cast
natCast_zero := Grind.Semiring.natCast_zero
natCast_succ n := Grind.Semiring.natCast_succ n
intCast := Int.cast
intCast_ofNat := Grind.Ring.intCast_natCast
intCast_negSucc
n := by
rw [Int.negSucc_eq, Grind.Ring.intCast_neg, Grind.Ring.intCast_natCast_add_one, Grind.Semiring.natCast_succ] }
-- Verify that we do not have a defeq problems in `Lean.Grind.Semiring` instances.
