-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.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 → motive b b.toPoly → motive (a.add b) (a.toPoly.combine b.toPoly)) →
            (∀ (a b : Lean.Grind.CommRing.Expr),
                motive a a.toPoly → motive b b.toPoly → motive (a.mul b) (a.toPoly.mul b.toPoly)) →
              (∀ (a : Lean.Grind.CommRing.Expr),
                  motive a a.toPoly → motive a.neg (Lean.Grind.CommRing.Poly.mulConst (-1) a.toPoly)) →
                (∀ (a b : Lean.Grind.CommRing.Expr),
                    motive a a.toPoly →
                      motive b b.toPoly →
                        motive (a.sub b) (a.toPoly.combine (Lean.Grind.CommRing.Poly.mulConst (-1) b.toPoly))) →
                  (∀ (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 → motive (a.pow k) (a.toPoly.pow k)) →
                              ∀ (a : Lean.Grind.CommRing.Expr), motive a a.toPoly