-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly_nc.induct_unfolding : ∀ (motive : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly → Prop),
  (∀ (k : ℤ), motive (Lean.Grind.CommRing.Expr.num k) (Lean.Grind.CommRing.Poly.num k)) →
    (∀ (k : ℤ), motive (Lean.Grind.CommRing.Expr.intCast k) (Lean.Grind.CommRing.Poly.num k)) →
      (∀ (k : ℕ), motive (Lean.Grind.CommRing.Expr.natCast k) (Lean.Grind.CommRing.Poly.num ↑k)) →
        (∀ (x : Lean.Grind.CommRing.Var), motive (Lean.Grind.CommRing.Expr.var x) (Lean.Grind.CommRing.Poly.ofVar x)) →
          (∀ (a b : Lean.Grind.CommRing.Expr),
              motive a a.toPoly_nc → motive b b.toPoly_nc → motive (a.add b) (a.toPoly_nc.combine b.toPoly_nc)) →
            (∀ (a b : Lean.Grind.CommRing.Expr),
                motive a a.toPoly_nc → motive b b.toPoly_nc → motive (a.mul b) (a.toPoly_nc.mul_nc b.toPoly_nc)) →
              (∀ (a : Lean.Grind.CommRing.Expr),
                  motive a a.toPoly_nc → motive a.neg (Lean.Grind.CommRing.Poly.mulConst (-1) a.toPoly_nc)) →
                (∀ (a b : Lean.Grind.CommRing.Expr),
                    motive a a.toPoly_nc →
                      motive b b.toPoly_nc →
                        motive (a.sub b) (a.toPoly_nc.combine (Lean.Grind.CommRing.Poly.mulConst (-1) b.toPoly_nc))) →
                  (∀ (a : Lean.Grind.CommRing.Expr) (k : ℕ),
                      (k == 0) = true → motive (a.pow k) (Lean.Grind.CommRing.Poly.num 1)) →
                    (∀ (k : ℕ),
                        (k == 0) = false →
                          ∀ (n : ℤ),
                            motive ((Lean.Grind.CommRing.Expr.num n).pow k) (Lean.Grind.CommRing.Poly.num (n ^ k))) →
                      (∀ (k : ℕ),
                          (k == 0) = false →
                            ∀ (n : ℤ),
                              motive ((Lean.Grind.CommRing.Expr.intCast n).pow k)
                                (Lean.Grind.CommRing.Poly.num (n ^ k))) →
                        (∀ (k : ℕ),
                            (k == 0) = false →
                              ∀ (n : ℕ),
                                motive ((Lean.Grind.CommRing.Expr.natCast n).pow k)
                                  (Lean.Grind.CommRing.Poly.num (↑n ^ k))) →
                          (∀ (k : ℕ),
                              (k == 0) = false →
                                ∀ (x : Lean.Grind.CommRing.Var),
                                  motive ((Lean.Grind.CommRing.Expr.var x).pow k)
                                    (Lean.Grind.CommRing.Poly.ofMon
                                      (Lean.Grind.CommRing.Mon.mult { x := x, k := k } Lean.Grind.CommRing.Mon.unit))) →
                            (∀ (a : Lean.Grind.CommRing.Expr) (k : ℕ),
                                (k == 0) = false →
                                  (∀ (n : ℤ), a = Lean.Grind.CommRing.Expr.num n → False) →
                                    (∀ (n : ℤ), a = Lean.Grind.CommRing.Expr.intCast n → False) →
                                      (∀ (n : ℕ), a = Lean.Grind.CommRing.Expr.natCast n → False) →
                                        (∀ (x : Lean.Grind.CommRing.Var), a = Lean.Grind.CommRing.Expr.var x → False) →
                                          motive a a.toPoly_nc → motive (a.pow k) (a.toPoly_nc.pow_nc k)) →
                              ∀ (a : Lean.Grind.CommRing.Expr), motive a a.toPoly_nc