awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
rw : smeval (ascPochhammer ℕ 0) (-0) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
rw₁ : smeval (ascPochhammer ℕ 0) 0 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
rw₂ : smeval (R := ℕ) 1 0 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
rw₃ : smeval (R := ℕ) 1 0 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑1 : ℤ)
rw₄ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (α := ℤ) (β := ℕ) 0 0) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑1 : ℤ)
rw₅ : HSMul.hSMul (α := ℕ) (β := ℤ) 1 1 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑1 : ℤ)
rw₆ : 1 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑1 : ℤ)
⊢ smeval (ascPochhammer ℕ 0) (-(↑0 : ℤ)) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
have rw₇ : 1 = HMul.hMul (α := ℤ) 1 (↑1 : ℤ)
Tactic: rw [Nat.cast_zero, neg_zero, ascPochhammer_zero, Nat.factorial_zero, smeval_one, pow_zero,
      one_smul, pow_zero, Nat.cast_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
rw : smeval (ascPochhammer ℕ 0) (-0) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
rw₁ : smeval (ascPochhammer ℕ 0) 0 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
rw₂ : smeval (R := ℕ) 1 0 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
rw₃ : smeval (R := ℕ) 1 0 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑1 : ℤ)
rw₄ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (α := ℤ) (β := ℕ) 0 0) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑1 : ℤ)
rw₅ : HSMul.hSMul (α := ℕ) (β := ℤ) 1 1 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑1 : ℤ)
rw₆ : 1 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑1 : ℤ)
rw₇ : 1 = HMul.hMul (α := ℤ) 1 (↑1 : ℤ)
⊢ smeval (ascPochhammer ℕ 0) (-(↑0 : ℤ)) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
have rw₈ : 1 = HMul.hMul (α := ℤ) 1 1
Tactic: rw [Nat.cast_zero, neg_zero, ascPochhammer_zero, Nat.factorial_zero, smeval_one, pow_zero,
      one_smul, pow_zero, Nat.cast_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
rw : smeval (ascPochhammer ℕ 0) (-0) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
rw₁ : smeval (ascPochhammer ℕ 0) 0 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
rw₂ : smeval (R := ℕ) 1 0 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
rw₃ : smeval (R := ℕ) 1 0 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑1 : ℤ)
rw₄ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (α := ℤ) (β := ℕ) 0 0) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑1 : ℤ)
rw₅ : HSMul.hSMul (α := ℕ) (β := ℤ) 1 1 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑1 : ℤ)
rw₆ : 1 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑1 : ℤ)
rw₇ : 1 = HMul.hMul (α := ℤ) 1 (↑1 : ℤ)
rw₈ : 1 = HMul.hMul (α := ℤ) 1 1
⊢ smeval (ascPochhammer ℕ 0) (-(↑0 : ℤ)) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
have rw₉ : Eq (α := ℤ) 1 1
Tactic: rw [Nat.cast_zero, neg_zero, ascPochhammer_zero, Nat.factorial_zero, smeval_one, pow_zero,
      one_smul, pow_zero, Nat.cast_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
have rw : (X * Polynomial.comp (ascPochhammer ℕ n) (HAdd.hAdd (α := ℕ[X]) X 1)).smeval (-(↑(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]
-- 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 : ℤ)
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
have 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 : ℤ)
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]
-- 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 : ℤ)
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
have rw₂ : HMul.hMul (α := ℤ) (-(↑(n + 1) : ℤ))
    (smeval (ascPochhammer ℕ n) ((HAdd.hAdd (α := ℕ[X]) X 1).smeval (-(↑(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]
-- 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 : ℤ)
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
have 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 : ℤ)
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]
-- 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 : ℤ)
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
have rw₄ : -(↑(n + 1) : ℤ) *
    smeval (ascPochhammer ℕ n) (HPow.hPow (α := ℤ) (β := ℕ) (-(↑(n + 1) : ℤ)) 1 + smeval (R := ℕ) 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]
-- 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 : ℤ)
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
have 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 : ℤ)
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]
-- 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 : ℤ)
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
have rw₆ : -(↑(n + 1) : ℤ) *
    smeval (ascPochhammer ℕ n) (HPow.hPow (α := ℤ) (β := ℕ) (-(↑(n + 1) : ℤ)) 1 + HSMul.hSMul (α := ℕ) (β := ℤ) 1 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]
-- 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 : ℤ)
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
have rw₇ : -(↑(n + 1) : ℤ) * smeval (ascPochhammer ℕ n) (-(↑(n + 1) : ℤ) + HSMul.hSMul (α := ℕ) (β := ℤ) 1 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]
-- 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 : ℤ)
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
have rw₈ : -(↑(n + 1) : ℤ) * smeval (ascPochhammer ℕ n) (HAdd.hAdd (α := ℤ) (-(↑(n + 1) : ℤ)) 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]
-- 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 : ℤ)
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
have rw₉ : -HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) * smeval (ascPochhammer ℕ n) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑1 : ℤ) + 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]
-- 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 : ℤ)
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
have rw₁₀ : -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * smeval (ascPochhammer ℕ n) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 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]