awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
ih : smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r
h : (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) = -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r
succ :
  Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₁ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₂ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    (HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑1 : ℤ)).negOnePow •
      (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₃ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1).negOnePow •
      (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₄ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₅ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -(Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r))
⊢ Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
have succ₆ : -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
  -(Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r))
Tactic: rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul,
      Units.smul_def, Units.smul_def, ← smul_mul_assoc, neg_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
ih : smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r
h : (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) = -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r
succ :
  Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₁ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₂ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    (HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑1 : ℤ)).negOnePow •
      (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₃ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1).negOnePow •
      (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₄ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₅ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -(Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r))
succ₆ :
  -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) • smeval (descPochhammer ℤ k) r) *
      (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -(Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r))
⊢ Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
have succ₇ : -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
  -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) •
      (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r))
Tactic: rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul,
      Units.smul_def, Units.smul_def, ← smul_mul_assoc, neg_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
ih : smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r
h : (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) = -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r
succ :
  Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₁ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₂ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    (HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑1 : ℤ)).negOnePow •
      (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₃ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1).negOnePow •
      (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₄ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₅ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -(Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r))
succ₆ :
  -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) • smeval (descPochhammer ℤ k) r) *
      (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -(Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r))
succ₇ :
  -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) • smeval (descPochhammer ℤ k) r) *
      (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) •
        (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r))
⊢ Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
have succ₈ : -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
  -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) • smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
Tactic: rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul,
      Units.smul_def, Units.smul_def, ← smul_mul_assoc, neg_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
⊢ smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r
have zero : smeval (ascPochhammer ℕ 0) (-r) = Int.negOnePow (↑0 : ℤ) • smeval (descPochhammer ℤ 0) r
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    simp only [ascPochhammer_succ_right, smeval_mul, ih, descPochhammer_succ_right, sub_eq_add_neg]
    have h : (X + (k : ℕ[X])).smeval (-r) = -(X + (-k : ℤ[X])).smeval r := by
      simp [smeval_natCast, add_comm]
    rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul,
      Units.smul_def, Units.smul_def, ← smul_mul_assoc, neg_mul]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
zero : smeval (ascPochhammer ℕ 0) (-r) = Int.negOnePow (↑0 : ℤ) • smeval (descPochhammer ℤ 0) r
⊢ smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r
have succ : ∀ (k : ℕ) (ih : smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r),
  smeval (ascPochhammer ℕ (k + 1)) (-r) = Int.negOnePow (↑(k + 1) : ℤ) • smeval (descPochhammer ℤ (k + 1)) r
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    simp only [ascPochhammer_succ_right, smeval_mul, ih, descPochhammer_succ_right, sub_eq_add_neg]
    have h : (X + (k : ℕ[X])).smeval (-r) = -(X + (-k : ℤ[X])).smeval r := by
      simp [smeval_natCast, add_comm]
    rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul,
      Units.smul_def, Units.smul_def, ← smul_mul_assoc, neg_mul]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
r n : ℕ
⊢ n ! • r.multichoose n = smeval (ascPochhammer ℕ n) r
have rw : n ! * r.multichoose n = smeval (ascPochhammer ℕ n) r
Tactic: rw [smul_eq_mul, Nat.multichoose_eq r n, ← Nat.descFactorial_eq_factorial_mul_choose,
      ← eval_eq_smeval r (ascPochhammer ℕ n), ascPochhammer_nat_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
r n : ℕ
rw : n ! * r.multichoose n = smeval (ascPochhammer ℕ n) r
⊢ n ! • r.multichoose n = smeval (ascPochhammer ℕ n) r
have rw₁ : n ! * (r + n - 1).choose n = smeval (ascPochhammer ℕ n) r
Tactic: rw [smul_eq_mul, Nat.multichoose_eq r n, ← Nat.descFactorial_eq_factorial_mul_choose,
      ← eval_eq_smeval r (ascPochhammer ℕ n), ascPochhammer_nat_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
r n : ℕ
rw : n ! * r.multichoose n = smeval (ascPochhammer ℕ n) r
rw₁ : n ! * (r + n - 1).choose n = smeval (ascPochhammer ℕ n) r
⊢ n ! • r.multichoose n = smeval (ascPochhammer ℕ n) r
have rw₂ : (r + n - 1).descFactorial n = smeval (ascPochhammer ℕ n) r
Tactic: rw [smul_eq_mul, Nat.multichoose_eq r n, ← Nat.descFactorial_eq_factorial_mul_choose,
      ← eval_eq_smeval r (ascPochhammer ℕ n), ascPochhammer_nat_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
r n : ℕ
rw : n ! * r.multichoose n = smeval (ascPochhammer ℕ n) r
rw₁ : n ! * (r + n - 1).choose n = smeval (ascPochhammer ℕ n) r
rw₂ : (r + n - 1).descFactorial n = smeval (ascPochhammer ℕ n) r
⊢ n ! • r.multichoose n = smeval (ascPochhammer ℕ n) r
have rw₃ : (r + n - 1).descFactorial n = Polynomial.eval r (ascPochhammer ℕ n)
Tactic: rw [smul_eq_mul, Nat.multichoose_eq r n, ← Nat.descFactorial_eq_factorial_mul_choose,
      ← eval_eq_smeval r (ascPochhammer ℕ n), ascPochhammer_nat_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
r n : ℕ
rw : n ! * r.multichoose n = smeval (ascPochhammer ℕ n) r
rw₁ : n ! * (r + n - 1).choose n = smeval (ascPochhammer ℕ n) r
rw₂ : (r + n - 1).descFactorial n = smeval (ascPochhammer ℕ n) r
rw₃ : (r + n - 1).descFactorial n = Polynomial.eval r (ascPochhammer ℕ n)
⊢ n ! • r.multichoose n = smeval (ascPochhammer ℕ n) r
have rw₄ : (r + n - 1).descFactorial n = (r + n - 1).descFactorial n
Tactic: rw [smul_eq_mul, Nat.multichoose_eq r n, ← Nat.descFactorial_eq_factorial_mul_choose,
      ← eval_eq_smeval r (ascPochhammer ℕ n), ascPochhammer_nat_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
r : ℤ
k : ℕ
⊢ k.factorial • r.multichoose k = smeval (ascPochhammer ℕ k) r
have rw : HMul.hMul (α := ℤ) (β := ℤ) ((↑k.factorial : ℤ) : ℤ)
    (match (motive := ℤ → ℤ) r with
      | ofNat n => (↑((n + k - 1).choose k) : ℤ)
      | -[n+1] => (↑(negOnePow (↑k : ℤ)) : ℤ) * (↑((n + 1).choose k) : ℤ) :
      ℤ) =
  smeval (ascPochhammer ℕ k) r
Tactic: rw [Int.multichoose.eq_def, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
k n : ℕ
⊢ Eq (α := ℤ) (↑(k.factorial * (n + k - 1).choose k) : ℤ) (smeval (ascPochhammer ℕ k) (↑n : ℤ))
have ofNat : Eq (α := ℤ) (↑((n + k - 1).descFactorial k) : ℤ) (smeval (ascPochhammer ℕ k) (↑n : ℤ))
Tactic: rw [← Nat.descFactorial_eq_factorial_mul_choose, smeval_at_natCast, ← eval_eq_smeval n,
        ascPochhammer_nat_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
k n : ℕ
ofNat : Eq (α := ℤ) (↑((n + k - 1).descFactorial k) : ℤ) (smeval (ascPochhammer ℕ k) (↑n : ℤ))
⊢ Eq (α := ℤ) (↑(k.factorial * (n + k - 1).choose k) : ℤ) (smeval (ascPochhammer ℕ k) (↑n : ℤ))
have ofNat₁ : Eq (α := ℤ) (↑((n + k - 1).descFactorial k) : ℤ) (↑(smeval (ascPochhammer ℕ k) n) : ℤ)
Tactic: rw [← Nat.descFactorial_eq_factorial_mul_choose, smeval_at_natCast, ← eval_eq_smeval n,
        ascPochhammer_nat_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
k n : ℕ
ofNat : Eq (α := ℤ) (↑((n + k - 1).descFactorial k) : ℤ) (smeval (ascPochhammer ℕ k) (↑n : ℤ))
ofNat₁ : Eq (α := ℤ) (↑((n + k - 1).descFactorial k) : ℤ) (↑(smeval (ascPochhammer ℕ k) n) : ℤ)
⊢ Eq (α := ℤ) (↑(k.factorial * (n + k - 1).choose k) : ℤ) (smeval (ascPochhammer ℕ k) (↑n : ℤ))
have ofNat₂ : Eq (α := ℤ) (↑((n + k - 1).descFactorial k) : ℤ) (↑(Polynomial.eval n (ascPochhammer ℕ k)) : ℤ)
Tactic: rw [← Nat.descFactorial_eq_factorial_mul_choose, smeval_at_natCast, ← eval_eq_smeval n,
        ascPochhammer_nat_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
k n : ℕ
ofNat : Eq (α := ℤ) (↑((n + k - 1).descFactorial k) : ℤ) (smeval (ascPochhammer ℕ k) (↑n : ℤ))
ofNat₁ : Eq (α := ℤ) (↑((n + k - 1).descFactorial k) : ℤ) (↑(smeval (ascPochhammer ℕ k) n) : ℤ)
ofNat₂ : Eq (α := ℤ) (↑((n + k - 1).descFactorial k) : ℤ) (↑(Polynomial.eval n (ascPochhammer ℕ k)) : ℤ)
⊢ Eq (α := ℤ) (↑(k.factorial * (n + k - 1).choose k) : ℤ) (smeval (ascPochhammer ℕ k) (↑n : ℤ))
have ofNat₃ : Eq (α := ℤ) (↑((n + k - 1).descFactorial k) : ℤ) (↑((n + k - 1).descFactorial k) : ℤ)
Tactic: rw [← Nat.descFactorial_eq_factorial_mul_choose, smeval_at_natCast, ← eval_eq_smeval n,
        ascPochhammer_nat_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
k n : ℕ
⊢ (↑k.factorial : ℤ) * ((↑(negOnePow (↑k : ℤ)) : ℤ) * (↑((n + 1).choose k) : ℤ)) = smeval (ascPochhammer ℕ k) -[n+1]
have negSucc : (↑(negOnePow (↑k : ℤ)) : ℤ) * smeval (descPochhammer ℤ k) (↑(n + 1) : ℤ) =
  HSMul.hSMul (β := ℤ) (negOnePow (↑k : ℤ)) (smeval (descPochhammer ℤ k) (↑n.succ : ℤ))
Tactic: rw [mul_comm, mul_assoc, ← Nat.cast_mul, mul_comm _ (k.factorial),
        ← Nat.descFactorial_eq_factorial_mul_choose, ← descPochhammer_smeval_eq_descFactorial,
        ← Int.neg_ofNat_succ, ascPochhammer_smeval_neg_eq_descPochhammer]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
r : ℤ
k : ℕ
⊢ HMul.hMul (α := ℤ) (β := ℤ) ((↑k.factorial : ℤ) : ℤ)
      (match (motive := ℤ → ℤ) r with
        | ofNat n => (↑((n + k - 1).choose k) : ℤ)
        | -[n+1] => (↑(negOnePow (↑k : ℤ)) : ℤ) * (↑((n + 1).choose k) : ℤ) :
        ℤ) =
    smeval (ascPochhammer ℕ k) r
have ofNat : ∀ (n : ℕ),
  HMul.hMul (α := ℤ) (β := ℤ) ((↑k.factorial : ℤ) : ℤ)
      (match (motive := ℤ → ℤ) ofNat n with
        | ofNat n => (↑((n + k - 1).choose k) : ℤ)
        | -[n+1] => (↑(negOnePow (↑k : ℤ)) : ℤ) * (↑((n + 1).choose k) : ℤ) :
        ℤ) =
    smeval (ascPochhammer ℕ k) (ofNat n)
Tactic: cases r with
    | ofNat n =>
      simp only [Int.ofNat_eq_natCast, Int.ofNat_mul_ofNat]
      rw [← Nat.descFactorial_eq_factorial_mul_choose, smeval_at_natCast, ← eval_eq_smeval n,
        ascPochhammer_nat_eq_descFactorial]
    | negSucc n =>
      simp only
      rw [mul_comm, mul_assoc, ← Nat.cast_mul, mul_comm _ (k.factorial),
        ← Nat.descFactorial_eq_factorial_mul_choose, ← descPochhammer_smeval_eq_descFactorial,
        ← Int.neg_ofNat_succ, ascPochhammer_smeval_neg_eq_descPochhammer]
      norm_cast
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
r : ℤ
k : ℕ
ofNat :
  ∀ (n : ℕ),
    HMul.hMul (α := ℤ) (β := ℤ) ((↑k.factorial : ℤ) : ℤ)
        (match (motive := ℤ → ℤ) Int.ofNat n with
          | Int.ofNat n => (↑((n + k - 1).choose k) : ℤ)
          | -[n+1] => (↑(negOnePow (↑k : ℤ)) : ℤ) * (↑((n + 1).choose k) : ℤ) :
          ℤ) =
      smeval (ascPochhammer ℕ k) (Int.ofNat n)
⊢ HMul.hMul (α := ℤ) (β := ℤ) ((↑k.factorial : ℤ) : ℤ)
      (match (motive := ℤ → ℤ) r with
        | Int.ofNat n => (↑((n + k - 1).choose k) : ℤ)
        | -[n+1] => (↑(negOnePow (↑k : ℤ)) : ℤ) * (↑((n + 1).choose k) : ℤ) :
        ℤ) =
    smeval (ascPochhammer ℕ k) r
have negSucc : ∀ (n : ℕ),
  HMul.hMul (α := ℤ) (β := ℤ) ((↑k.factorial : ℤ) : ℤ)
      (match (motive := ℤ → ℤ) -[n+1] with
        | Int.ofNat n => (↑((n + k - 1).choose k) : ℤ)
        | -[n+1] => (↑(negOnePow (↑k : ℤ)) : ℤ) * (↑((n + 1).choose k) : ℤ) :
        ℤ) =
    smeval (ascPochhammer ℕ k) -[n+1]
Tactic: cases r with
    | ofNat n =>
      simp only [Int.ofNat_eq_natCast, Int.ofNat_mul_ofNat]
      rw [← Nat.descFactorial_eq_factorial_mul_choose, smeval_at_natCast, ← eval_eq_smeval n,
        ascPochhammer_nat_eq_descFactorial]
    | negSucc n =>
      simp only
      rw [mul_comm, mul_assoc, ← Nat.cast_mul, mul_comm _ (k.factorial),
        ← Nat.descFactorial_eq_factorial_mul_choose, ← descPochhammer_smeval_eq_descFactorial,
        ← Int.neg_ofNat_succ, ascPochhammer_smeval_neg_eq_descPochhammer]
      norm_cast
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Module ℚ≥0 R
inst_2 : Pow R ℕ
r : R
n : ℕ
⊢ n.factorial • HSMul.hSMul (α := ℚ≥0) (↑n.factorial : ℚ≥0)⁻¹ (smeval (ascPochhammer ℕ n) r) =
    smeval (ascPochhammer ℕ n) r
have match_scalars : (↑n.factorial : ℚ≥0) * HMul.hMul (α := ℚ≥0) (↑n.factorial : ℚ≥0)⁻¹ 1 = 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
⊢ smeval (ascPochhammer ℕ 0) (-(↑0 : ℤ)) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
have rw : smeval (ascPochhammer ℕ 0) (-0) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
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) : ℤ)
⊢ smeval (ascPochhammer ℕ 0) (-(↑0 : ℤ)) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
have rw₁ : smeval (ascPochhammer ℕ 0) 0 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
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) : ℤ)
⊢ smeval (ascPochhammer ℕ 0) (-(↑0 : ℤ)) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
have rw₂ : smeval (R := ℕ) 1 0 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
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) : ℤ)
⊢ smeval (ascPochhammer ℕ 0) (-(↑0 : ℤ)) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
have rw₃ : smeval (R := ℕ) 1 0 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑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 : ℤ)
⊢ smeval (ascPochhammer ℕ 0) (-(↑0 : ℤ)) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
have rw₄ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (α := ℤ) (β := ℕ) 0 0) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑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 : ℤ)
⊢ smeval (ascPochhammer ℕ 0) (-(↑0 : ℤ)) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
have rw₅ : HSMul.hSMul (α := ℕ) (β := ℤ) 1 1 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑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 : ℤ)
⊢ smeval (ascPochhammer ℕ 0) (-(↑0 : ℤ)) = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(Nat.factorial 0) : ℤ)
have rw₆ : 1 = HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑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]