-- Module: Mathlib.RingTheory.Binomial
Goal:
n : ℕ
rw :
  (X * Polynomial.comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1)).smeval (-(↑(n + 1) : ℤ)) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₁ :
  HMul.hMul (α := ℤ) (-(↑(n + 1) : ℤ))
      ((Polynomial.comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1)).smeval (-(↑(n + 1) : ℤ))) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₂ :
  HMul.hMul (α := ℤ) (-(↑(n + 1) : ℤ))
      (smeval (ascPochhammer ℕ n) ((HAdd.hAdd (α := ℕ[X]) X 1).smeval (-(↑(n + 1) : ℤ)))) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₃ :
  -(↑(n + 1) : ℤ) *
      smeval (ascPochhammer ℕ n)
        (HAdd.hAdd (α := ℤ) (smeval (R := ℕ) X (-(↑(n + 1) : ℤ))) (smeval (R := ℕ) 1 (-(↑(n + 1) : ℤ)))) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₄ :
  -(↑(n + 1) : ℤ) *
      smeval (ascPochhammer ℕ n)
        (HPow.hPow (α := ℤ) (β := ℕ) (-(↑(n + 1) : ℤ)) 1 + smeval (R := ℕ) 1 (-(↑(n + 1) : ℤ))) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₅ :
  -(↑(n + 1) : ℤ) *
      smeval (ascPochhammer ℕ n)
        (HPow.hPow (α := ℤ) (β := ℕ) (-(↑(n + 1) : ℤ)) 1 +
          HSMul.hSMul (α := ℕ) 1 (HPow.hPow (α := ℤ) (β := ℕ) (-(↑(n + 1) : ℤ)) 0)) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₆ :
  -(↑(n + 1) : ℤ) *
      smeval (ascPochhammer ℕ n) (HPow.hPow (α := ℤ) (β := ℕ) (-(↑(n + 1) : ℤ)) 1 + HSMul.hSMul (α := ℕ) (β := ℤ) 1 1) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₇ :
  -(↑(n + 1) : ℤ) * smeval (ascPochhammer ℕ n) (-(↑(n + 1) : ℤ) + HSMul.hSMul (α := ℕ) (β := ℤ) 1 1) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₈ :
  -(↑(n + 1) : ℤ) * smeval (ascPochhammer ℕ n) (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 1) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₉ :
  -HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) * smeval (ascPochhammer ℕ n) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) + 1) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₁₀ :
  -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * smeval (ascPochhammer ℕ n) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₁₁ :
  HAdd.hAdd (α := ℤ) (-1) (-(↑n : ℤ)) * smeval (ascPochhammer ℕ n) (HAdd.hAdd (α := ℤ) (-1) (-(↑n : ℤ)) + 1) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₁₂ :
  HAdd.hAdd (α := ℤ) (-1) (-(↑n : ℤ)) * smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₁₃ :
  HAdd.hAdd (α := ℤ) (-1) (-(↑n : ℤ)) * (HPow.hPow (α := ℤ) (-1) n * (↑n.factorial : ℤ)) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₁₄ :
  HAdd.hAdd (α := ℤ) (-1) (-(↑n : ℤ)) * HPow.hPow (α := ℤ) (-1) n * (↑n.factorial : ℤ) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₁₅ :
  HPow.hPow (α := ℤ) (-1) n * HAdd.hAdd (α := ℤ) (-1) (-(↑n : ℤ)) * (↑n.factorial : ℤ) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₁₆ :
  HPow.hPow (α := ℤ) (-1) n * (-1 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) * (↑n.factorial : ℤ) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₁₇ :
  HPow.hPow (α := ℤ) (-1) n * -1 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑n.factorial : ℤ) =
    HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
rw₁₈ :
  HPow.hPow (α := ℤ) (-1) n * -1 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑n.factorial : ℤ) =
    HPow.hPow (α := ℤ) (-1) n * HPow.hPow (α := ℤ) (β := ℕ) (-1) 1 * (↑(n + 1).factorial : ℤ)
rw₁₉ :
  HPow.hPow (α := ℤ) (-1) n * -1 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑n.factorial : ℤ) =
    HPow.hPow (α := ℤ) (-1) n * -1 * (↑(n + 1).factorial : ℤ)
rw₂₀ :
  HPow.hPow (α := ℤ) (-1) n * -1 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑n.factorial : ℤ) =
    HPow.hPow (α := ℤ) (-1) n * -1 * (↑(n.succ * n.factorial) : ℤ)
rw₂₁ :
  HPow.hPow (α := ℤ) (-1) n * -1 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑n.factorial : ℤ) =
    HPow.hPow (α := ℤ) (-1) n * -1 * HMul.hMul (α := ℤ) (↑n.succ : ℤ) (↑n.factorial : ℤ)
rw₂₂ :
  HPow.hPow (α := ℤ) (-1) n * -1 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑n.factorial : ℤ) =
    HPow.hPow (α := ℤ) (-1) n * -1 * (↑n.succ : ℤ) * (↑n.factorial : ℤ)
rw₂₃ rw₂₄ :
  HPow.hPow (α := ℤ) (-1) n * -1 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑n.factorial : ℤ) =
    HPow.hPow (α := ℤ) (-1) n * -1 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑n.factorial : ℤ)
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)

Tactic:
rw [ascPochhammer_succ_left, smeval_X_mul, smeval_comp, smeval_add, smeval_X, smeval_one,
      pow_zero, pow_one, one_smul, Nat.cast_add, Nat.cast_one, neg_add_rev, neg_add_cancel_comm,
      smeval_ascPochhammer_self_neg n, ← mul_assoc, mul_comm _ ((-1) ^ n),
      show (-1 + -↑n = (-1 : ℤ) * (n + 1)) by lia, ← mul_assoc, pow_add, pow_one,
      Nat.factorial, Nat.cast_mul, ← mul_assoc, Nat.cast_succ]

Premises used: neg_add_rev, Nat.cast_succ, mul_assoc, pow_add, Polynomial.smeval_X, pow_zero, one_smul, Polynomial.smeval_X_mul, neg_add_cancel_comm, Nat.cast_add, Polynomial.smeval_one, Nat.cast_mul, HPow.hPow, Nat.factorial, pow_one, Polynomial.smeval_comp, mul_comm, Polynomial.smeval_add, OfNat.ofNat, Nat.cast_one, ascPochhammer_succ_left, Neg.neg