-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go.induct_unfolding : ∀ (c : ℕ) (motive : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly → Prop),
  (∀ (k : ℤ), motive (Lean.Grind.CommRing.Expr.num k) (Lean.Grind.CommRing.Poly.num (k % ↑c))) →
    (∀ (k : ℕ), motive (Lean.Grind.CommRing.Expr.natCast k) (Lean.Grind.CommRing.Poly.num (↑k % ↑c))) →
      (∀ (k : ℤ), motive (Lean.Grind.CommRing.Expr.intCast k) (Lean.Grind.CommRing.Poly.num (k % ↑c))) →
        (∀ (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 (Lean.Grind.CommRing.Expr.toPolyC.go c a) →
                motive b (Lean.Grind.CommRing.Expr.toPolyC.go c b) →
                  motive (a.add b)
                    ((Lean.Grind.CommRing.Expr.toPolyC.go c a).combineC (Lean.Grind.CommRing.Expr.toPolyC.go c b) c)) →
            (∀ (a b : Lean.Grind.CommRing.Expr),
                motive a (Lean.Grind.CommRing.Expr.toPolyC.go c a) →
                  motive b (Lean.Grind.CommRing.Expr.toPolyC.go c b) →
                    motive (a.mul b)
                      ((Lean.Grind.CommRing.Expr.toPolyC.go c a).mulC (Lean.Grind.CommRing.Expr.toPolyC.go c b) c)) →
              (∀ (a : Lean.Grind.CommRing.Expr),
                  motive a (Lean.Grind.CommRing.Expr.toPolyC.go c a) →
                    motive a.neg
                      (Lean.Grind.CommRing.Poly.mulConstC (-1) (Lean.Grind.CommRing.Expr.toPolyC.go c a) c)) →
                (∀ (a b : Lean.Grind.CommRing.Expr),
                    motive a (Lean.Grind.CommRing.Expr.toPolyC.go c a) →
                      motive b (Lean.Grind.CommRing.Expr.toPolyC.go c b) →
                        motive (a.sub b)
                          ((Lean.Grind.CommRing.Expr.toPolyC.go c a).combineC
                            (Lean.Grind.CommRing.Poly.mulConstC (-1) (Lean.Grind.CommRing.Expr.toPolyC.go c b) c) c)) →
                  (∀ (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 % ↑c))) →
                      (∀ (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) →
                                (∀ (x : Lean.Grind.CommRing.Var), a = Lean.Grind.CommRing.Expr.var x → False) →
                                  motive a (Lean.Grind.CommRing.Expr.toPolyC.go c a) →
                                    motive (a.pow k) ((Lean.Grind.CommRing.Expr.toPolyC.go c a).powC k c)) →
                          ∀ (a : Lean.Grind.CommRing.Expr), motive a (Lean.Grind.CommRing.Expr.toPolyC.go c a)