-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
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 : ℤ)
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
have rw₁₉ : HPow.hPow (α := ℤ) (-1) n * -1 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * (↑n.factorial : ℤ) =
  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]