∀ (x : Lean.Grind.CommRing.Expr),
  x.toPolyS_nc =
    match x with
    | Lean.Grind.CommRing.Expr.num n => Lean.Grind.CommRing.Poly.num ↑n.natAbs
    | Lean.Grind.CommRing.Expr.var x => Lean.Grind.CommRing.Poly.ofVar x
    | a.add b => a.toPolyS_nc.combine b.toPolyS_nc
    | a.mul b => a.toPolyS_nc.mul_nc b.toPolyS_nc
    | a.pow k =>
      match a with
      | Lean.Grind.CommRing.Expr.num n => Lean.Grind.CommRing.Poly.num (↑n.natAbs ^ k)
      | Lean.Grind.CommRing.Expr.var x =>
        Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.mult { x := x, k := k } Lean.Grind.CommRing.Mon.unit)
      | x => a.toPolyS_nc.pow_nc k
    | Lean.Grind.CommRing.Expr.natCast n => Lean.Grind.CommRing.Poly.num ↑n
    | a.sub b => Lean.Grind.CommRing.Poly.num 0
    | a.neg => Lean.Grind.CommRing.Poly.num 0
    | Lean.Grind.CommRing.Expr.intCast k => Lean.Grind.CommRing.Poly.num 0