awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℤ)
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
have rw₁₁ : HAdd.hAdd (α := ℤ) (-1) (-(↑n : ℤ)) * smeval (ascPochhammer ℕ n) (HAdd.hAdd (α := ℤ) (-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 : ℤ)
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 : ℤ)
⊢ smeval (ascPochhammer ℕ (n + 1)) (-(↑(n + 1) : ℤ)) = HPow.hPow (α := ℤ) (-1) (n + 1) * (↑(n + 1).factorial : ℤ)
have rw₁₂ : HAdd.hAdd (α := ℤ) (-1) (-(↑n : ℤ)) * smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) =
  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 : ℕ
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
have rw : Eq (α := ℤ) ((ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) 0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C,
    pow_zero, pow_one, Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : Eq (α := ℤ) ((ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) 0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
have rw₁ : HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ n) (-(↑n : ℤ))) ((HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) =
  0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C,
    pow_zero, pow_one, Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : Eq (α := ℤ) ((ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) 0
rw₁ :
  HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ n) (-(↑n : ℤ)))
      ((HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) =
    0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
have rw₂ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
    HAdd.hAdd (α := ℤ) (smeval (R := ℕ) X (-(↑n : ℤ))) (smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
  0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C,
    pow_zero, pow_one, Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : Eq (α := ℤ) ((ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) 0
rw₁ :
  HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ n) (-(↑n : ℤ)))
      ((HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) =
    0
rw₂ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      HAdd.hAdd (α := ℤ) (smeval (R := ℕ) X (-(↑n : ℤ))) (smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
have rw₃ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
    (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
  0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C,
    pow_zero, pow_one, Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : Eq (α := ℤ) ((ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) 0
rw₁ :
  HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ n) (-(↑n : ℤ)))
      ((HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) =
    0
rw₂ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      HAdd.hAdd (α := ℤ) (smeval (R := ℕ) X (-(↑n : ℤ))) (smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₃ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
have rw₄ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
    (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) ((C : (a : ℕ) → ℕ[X]) (↑n : ℕ)) (-(↑n : ℤ))) =
  0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C,
    pow_zero, pow_one, Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : Eq (α := ℤ) ((ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) 0
rw₁ :
  HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ n) (-(↑n : ℤ)))
      ((HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) =
    0
rw₂ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      HAdd.hAdd (α := ℤ) (smeval (R := ℕ) X (-(↑n : ℤ))) (smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₃ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₄ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) ((C : (a : ℕ) → ℕ[X]) (↑n : ℕ)) (-(↑n : ℤ))) =
    0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
have rw₅ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
    (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 +
      HSMul.hSMul (α := ℕ) (↑n : ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 0)) =
  0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C,
    pow_zero, pow_one, Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : Eq (α := ℤ) ((ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) 0
rw₁ :
  HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ n) (-(↑n : ℤ)))
      ((HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) =
    0
rw₂ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      HAdd.hAdd (α := ℤ) (smeval (R := ℕ) X (-(↑n : ℤ))) (smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₃ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₄ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) ((C : (a : ℕ) → ℕ[X]) (↑n : ℕ)) (-(↑n : ℤ))) =
    0
rw₅ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 +
        HSMul.hSMul (α := ℕ) (↑n : ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 0)) =
    0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
have rw₆ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
    (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + HSMul.hSMul (α := ℕ) (β := ℤ) (↑n : ℕ) 1) =
  0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C,
    pow_zero, pow_one, Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : Eq (α := ℤ) ((ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) 0
rw₁ :
  HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ n) (-(↑n : ℤ)))
      ((HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) =
    0
rw₂ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      HAdd.hAdd (α := ℤ) (smeval (R := ℕ) X (-(↑n : ℤ))) (smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₃ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₄ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) ((C : (a : ℕ) → ℕ[X]) (↑n : ℕ)) (-(↑n : ℤ))) =
    0
rw₅ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 +
        HSMul.hSMul (α := ℕ) (↑n : ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 0)) =
    0
rw₆ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + HSMul.hSMul (α := ℕ) (β := ℤ) (↑n : ℕ) 1) =
    0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
have rw₇ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HSMul.hSMul (α := ℕ) (β := ℤ) (↑n : ℕ) 1) = 0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C,
    pow_zero, pow_one, Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : Eq (α := ℤ) ((ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) 0
rw₁ :
  HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ n) (-(↑n : ℤ)))
      ((HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) =
    0
rw₂ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      HAdd.hAdd (α := ℤ) (smeval (R := ℕ) X (-(↑n : ℤ))) (smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₃ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₄ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) ((C : (a : ℕ) → ℕ[X]) (↑n : ℕ)) (-(↑n : ℤ))) =
    0
rw₅ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 +
        HSMul.hSMul (α := ℕ) (↑n : ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 0)) =
    0
rw₆ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + HSMul.hSMul (α := ℕ) (β := ℤ) (↑n : ℕ) 1) =
    0
rw₇ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HSMul.hSMul (α := ℕ) (β := ℤ) (↑n : ℕ) 1) = 0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
have rw₈ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HSMul.hSMul (β := ℤ) n 1) = 0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C,
    pow_zero, pow_one, Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : Eq (α := ℤ) ((ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) 0
rw₁ :
  HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ n) (-(↑n : ℤ)))
      ((HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) =
    0
rw₂ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      HAdd.hAdd (α := ℤ) (smeval (R := ℕ) X (-(↑n : ℤ))) (smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₃ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₄ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) ((C : (a : ℕ) → ℕ[X]) (↑n : ℕ)) (-(↑n : ℤ))) =
    0
rw₅ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 +
        HSMul.hSMul (α := ℕ) (↑n : ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 0)) =
    0
rw₆ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + HSMul.hSMul (α := ℕ) (β := ℤ) (↑n : ℕ) 1) =
    0
rw₇ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HSMul.hSMul (α := ℕ) (β := ℤ) (↑n : ℕ) 1) = 0
rw₈ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HSMul.hSMul (β := ℤ) n 1) = 0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
have rw₉ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HMul.hMul (α := ℤ) (↑n : ℤ) 1) = 0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C,
    pow_zero, pow_one, Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : Eq (α := ℤ) ((ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) 0
rw₁ :
  HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ n) (-(↑n : ℤ)))
      ((HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) =
    0
rw₂ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      HAdd.hAdd (α := ℤ) (smeval (R := ℕ) X (-(↑n : ℤ))) (smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₃ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₄ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) ((C : (a : ℕ) → ℕ[X]) (↑n : ℕ)) (-(↑n : ℤ))) =
    0
rw₅ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 +
        HSMul.hSMul (α := ℕ) (↑n : ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 0)) =
    0
rw₆ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + HSMul.hSMul (α := ℕ) (β := ℤ) (↑n : ℕ) 1) =
    0
rw₇ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HSMul.hSMul (α := ℕ) (β := ℤ) (↑n : ℕ) 1) = 0
rw₈ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HSMul.hSMul (β := ℤ) n 1) = 0
rw₉ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HMul.hMul (α := ℤ) (↑n : ℤ) 1) = 0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
have rw₁₀ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (↑n : ℤ) = 0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C,
    pow_zero, pow_one, Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : Eq (α := ℤ) ((ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) 0
rw₁ :
  HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ n) (-(↑n : ℤ)))
      ((HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) =
    0
rw₂ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      HAdd.hAdd (α := ℤ) (smeval (R := ℕ) X (-(↑n : ℤ))) (smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₃ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₄ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) ((C : (a : ℕ) → ℕ[X]) (↑n : ℕ)) (-(↑n : ℤ))) =
    0
rw₅ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 +
        HSMul.hSMul (α := ℕ) (↑n : ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 0)) =
    0
rw₆ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + HSMul.hSMul (α := ℕ) (β := ℤ) (↑n : ℕ) 1) =
    0
rw₇ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HSMul.hSMul (α := ℕ) (β := ℤ) (↑n : ℕ) 1) = 0
rw₈ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HSMul.hSMul (β := ℤ) n 1) = 0
rw₉ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HMul.hMul (α := ℤ) (↑n : ℤ) 1) = 0
rw₁₀ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (↑n : ℤ) = 0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
have rw₁₁ : HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ n) (-(↑n : ℤ))) 0 = 0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C,
    pow_zero, pow_one, Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : Eq (α := ℤ) ((ascPochhammer ℕ n * HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) 0
rw₁ :
  HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ n) (-(↑n : ℤ)))
      ((HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval (-(↑n : ℤ))) =
    0
rw₂ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      HAdd.hAdd (α := ℤ) (smeval (R := ℕ) X (-(↑n : ℤ))) (smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₃ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) (↑n : ℕ[X]) (-(↑n : ℤ))) =
    0
rw₄ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + smeval (R := ℕ) ((C : (a : ℕ) → ℕ[X]) (↑n : ℕ)) (-(↑n : ℤ))) =
    0
rw₅ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 +
        HSMul.hSMul (α := ℕ) (↑n : ℕ) (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 0)) =
    0
rw₆ :
  smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) *
      (HPow.hPow (α := ℤ) (β := ℕ) (-(↑n : ℤ)) 1 + HSMul.hSMul (α := ℕ) (β := ℤ) (↑n : ℕ) 1) =
    0
rw₇ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HSMul.hSMul (α := ℕ) (β := ℤ) (↑n : ℕ) 1) = 0
rw₈ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HSMul.hSMul (β := ℤ) n 1) = 0
rw₉ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * (-(↑n : ℤ) + HMul.hMul (α := ℤ) (↑n : ℤ) 1) = 0
rw₁₀ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) * HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (↑n : ℤ) = 0
rw₁₁ : HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ n) (-(↑n : ℤ))) 0 = 0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
have rw₁₂ : Eq (α := ℤ) 0 0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C,
    pow_zero, pow_one, Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 0 + 1)) (-(↑n : ℤ))) 0
have rw₁ : Eq (α := ℤ) 0 0
Tactic: rw [add_zero, smeval_ascPochhammer_succ_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n k : ℕ
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + (k + 1) + 1)) (-(↑n : ℤ))) 0
have rw : Eq (α := ℤ) ((ascPochhammer ℕ (n + (k + 1)) * HAdd.hAdd (α := ℕ[X]) X (↑(n + (k + 1)) : ℕ[X])).smeval (-(↑n : ℤ))) 0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, ← add_assoc, smeval_ascPochhammer_neg_add n k,
      zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n k : ℕ
rw :
  Eq (α := ℤ) ((ascPochhammer ℕ (n + (k + 1)) * HAdd.hAdd (α := ℕ[X]) X (↑(n + (k + 1)) : ℕ[X])).smeval (-(↑n : ℤ))) 0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + (k + 1) + 1)) (-(↑n : ℤ))) 0
have rw₁ : HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ (n + (k + 1))) (-(↑n : ℤ)))
    ((HAdd.hAdd (α := ℕ[X]) X (↑(n + (k + 1)) : ℕ[X])).smeval (-(↑n : ℤ))) =
  0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, ← add_assoc, smeval_ascPochhammer_neg_add n k,
      zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n k : ℕ
rw :
  Eq (α := ℤ) ((ascPochhammer ℕ (n + (k + 1)) * HAdd.hAdd (α := ℕ[X]) X (↑(n + (k + 1)) : ℕ[X])).smeval (-(↑n : ℤ))) 0
rw₁ :
  HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ (n + (k + 1))) (-(↑n : ℤ)))
      ((HAdd.hAdd (α := ℕ[X]) X (↑(n + (k + 1)) : ℕ[X])).smeval (-(↑n : ℤ))) =
    0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + (k + 1) + 1)) (-(↑n : ℤ))) 0
have rw₂ : HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ (n + k + 1)) (-(↑n : ℤ)))
    ((HAdd.hAdd (α := ℕ[X]) X (↑(n + k + 1) : ℕ[X])).smeval (-(↑n : ℤ))) =
  0
Tactic: rw [ascPochhammer_succ_right, smeval_mul, ← add_assoc, smeval_ascPochhammer_neg_add n k,
      zero_mul]