awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : NonAssocSemiring S
inst_2 : Pow S ℕ
inst_3 : Module R S
inst_4 : IsScalarTower R S S
inst_5 : NatPowAssoc S
x : S
n : ℕ
zero : smeval (ascPochhammer R 0) x = smeval (ascPochhammer ℕ 0) x
succ :
  ∀ (n : ℕ) (hn : smeval (ascPochhammer R n) x = smeval (ascPochhammer ℕ n) x),
    smeval (ascPochhammer R (n + 1)) x = smeval (ascPochhammer ℕ (n + 1)) x
⊢ smeval (ascPochhammer R n) x = smeval (ascPochhammer ℕ n) x

Tactic:
induction n with
  | zero => simp only [ascPochhammer_zero, smeval_one]
  | succ n hn =>
    simp only [ascPochhammer_succ_right, mul_add, smeval_add, smeval_mul_X, ← Nat.cast_comm]
    simp only [← C_eq_natCast, smeval_C_mul, hn, Nat.cast_smul_eq_nsmul R n]
    simp only [nsmul_eq_mul, Nat.cast_id]

Premises used: Nat.cast_comm, Polynomial.smeval_mul_X, Nat.cast_id, Polynomial.C_eq_natCast, Polynomial.smeval_C_mul, Polynomial.smeval_one, ascPochhammer_zero, Nat.cast_smul_eq_nsmul, nsmul_eq_mul, mul_add, Polynomial.smeval_add, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℕ
rw : smeval (ascPochhammer ℕ n) r = smeval (ascPochhammer R n) r
rw₁ rw₂ : smeval (ascPochhammer ℕ n) r = smeval (ascPochhammer ℕ n) r
⊢ smeval (ascPochhammer ℕ n) r = eval r (ascPochhammer R n)

Tactic:
rw [eval_eq_smeval, ascPochhammer_smeval_cast R]

Premises used: Polynomial.ascPochhammer_smeval_cast, Polynomial.eval_eq_smeval
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
⊢ smeval (descPochhammer ℤ 0) r = smeval (ascPochhammer ℕ 0) (r - (↑0 : R) + 1)

Tactic:
simp only [descPochhammer_zero, ascPochhammer_zero, smeval_one, npow_zero]

Premises used: npow_zero, Polynomial.smeval_one, ascPochhammer_zero, descPochhammer_zero
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
n : ℕ
ih : smeval (descPochhammer ℤ n) r = smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
succ :
  smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1) *
      (smeval (R := ℤ) X r - HSMul.hSMul (α := ℤ) (↑n : ℤ) (HPow.hPow (β := ℕ) r 0)) =
    smeval (ascPochhammer ℕ n)
        (smeval (R := ℕ) X (r - (↑n : R)) + HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) (r - (↑n : R)) 0)) *
      (r - (↑n : R))
⊢ smeval (descPochhammer ℤ (n + 1)) r = smeval (ascPochhammer ℕ (n + 1)) (r - (↑(n + 1) : R) + 1)

Tactic:
rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right, smeval_mul, ih,
      ascPochhammer_succ_left, X_mul, smeval_mul_X, smeval_comp, smeval_sub, ← C_eq_natCast,
      smeval_add, smeval_one, smeval_C]

Premises used: sub_add, Nat.cast_succ, Polynomial.smeval_mul_X, Polynomial.C_eq_natCast, descPochhammer_succ_right, Polynomial.smeval_sub, Polynomial.smeval_C, Polynomial.smeval_mul, Polynomial.smeval_one, Polynomial.X_mul, Polynomial.smeval_comp, Polynomial.smeval_add, add_sub_cancel_right, ascPochhammer_succ_left
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
n : ℕ
ih : smeval (descPochhammer ℤ n) r = smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
⊢ smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1) *
      (smeval (R := ℤ) X r - HSMul.hSMul (α := ℤ) (↑n : ℤ) (HPow.hPow (β := ℕ) r 0)) =
    smeval (ascPochhammer ℕ n)
        (smeval (R := ℕ) X (r - (↑n : R)) + HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) (r - (↑n : R)) 0)) *
      (r - (↑n : R))

Tactic:
simp only [smeval_X, npow_one, npow_zero, zsmul_one, Int.cast_natCast, one_smul]

Premises used: Int.cast_natCast, npow_one, npow_zero, Polynomial.smeval_X, one_smul, zsmul_one
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
n : ℕ
zero : smeval (descPochhammer ℤ 0) r = smeval (ascPochhammer ℕ 0) (r - (↑0 : R) + 1)
succ :
  ∀ (n : ℕ) (ih : smeval (descPochhammer ℤ n) r = smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)),
    smeval (descPochhammer ℤ (n + 1)) r = smeval (ascPochhammer ℕ (n + 1)) (r - (↑(n + 1) : R) + 1)
⊢ smeval (descPochhammer ℤ n) r = smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)

Tactic:
induction n with
  | zero => simp only [descPochhammer_zero, ascPochhammer_zero, smeval_one, npow_zero]
  | succ n ih =>
    rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right, smeval_mul, ih,
      ascPochhammer_succ_left, X_mul, smeval_mul_X, smeval_comp, smeval_sub, ← C_eq_natCast,
      smeval_add, smeval_one, smeval_C]
    simp only [smeval_X, npow_one, npow_zero, zsmul_one, Int.cast_natCast, one_smul]

Premises used: sub_add, Nat.cast_succ, Int.cast_natCast, Polynomial.smeval_mul_X, Polynomial.C_eq_natCast, descPochhammer_succ_right, Polynomial.smeval_sub, npow_one, Polynomial.smeval_C, Polynomial.smeval_mul, npow_zero, Polynomial.smeval_X, one_smul, Polynomial.smeval_one, ascPochhammer_zero, Polynomial.X_mul, Polynomial.smeval_comp, Polynomial.smeval_add, zsmul_one, add_sub_cancel_right, ascPochhammer_succ_left, descPochhammer_zero
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n : ℕ
zero : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) (↑(n.descFactorial 0) : R)
zero₁ : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) (↑1 : R)
zero₂ : Eq.{u_1 + 1} (α := R) (smeval (R := ℤ) 1 (↑n : R)) 1
zero₃ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (α := R) (β := ℕ) (↑n : R) 0) = 1
zero₄ : HSMul.hSMul (α := ℕ) (β := R) 1 1 = 1
zero₅ zero₆ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ 0) (↑n : R)) (↑(n.descFactorial 0) : R)

Tactic:
rw [descPochhammer_zero, Nat.descFactorial_zero, Nat.cast_one, smeval_one, npow_zero, one_smul]

Premises used: npow_zero, one_smul, Polynomial.smeval_one, Nat.descFactorial_zero, Nat.cast_one, descPochhammer_zero
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n k : ℕ
ih : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(n.descFactorial k) : R)
succ :
  (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
    HMul.hMul (α := R) (↑(n.descFactorial k) : R) (↑(n - k) : R)
⊢ Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ (k + 1)) (↑n : R)) (↑(n.descFactorial (k + 1)) : R)

Tactic:
rw [descPochhammer_succ_right, Nat.descFactorial_succ, smeval_mul, ih, mul_comm, Nat.cast_mul,
      smeval_sub, smeval_X, smeval_natCast, npow_one, npow_zero, nsmul_one]

Premises used: descPochhammer_succ_right, Polynomial.smeval_sub, Polynomial.smeval_natCast, npow_one, Polynomial.smeval_mul, npow_zero, Polynomial.smeval_X, Nat.descFactorial_succ, Nat.cast_mul, mul_comm, nsmul_one
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n k : ℕ
ih : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(n.descFactorial k) : R)
pos :
  ∀ (h : n < k),
    (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
      HMul.hMul (α := R) (↑(n.descFactorial k) : R) (↑(n - k) : R)
neg :
  ∀ (h : k ≤ n),
    (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
      HMul.hMul (α := R) (↑(n.descFactorial k) : R) (↑(n - k) : R)
⊢ (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
    HMul.hMul (α := R) (↑(n.descFactorial k) : R) (↑(n - k) : R)

Tactic:
by_cases! h : n < k
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n k : ℕ
ih : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(n.descFactorial k) : R)
h : n < k
⊢ (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
    HMul.hMul (α := R) (↑(n.descFactorial k) : R) (↑(n - k) : R)

Tactic:
simp only [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, zero_mul]

Premises used: Iff.mpr, MulZeroClass.zero_mul, Nat.descFactorial_eq_zero_iff_lt, Nat.cast_zero
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n k : ℕ
ih : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(n.descFactorial k) : R)
h : k ≤ n
neg neg₁ :
  (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
    (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R)
⊢ (↑(n.descFactorial k) : R) * HSub.hSub (α := R) (↑n : R) (↑k : R) =
    HMul.hMul (α := R) (↑(n.descFactorial k) : R) (↑(n - k) : R)

Tactic:
rw [Nat.cast_sub h]

Premises used: Nat.cast_sub
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n k : ℕ
zero : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ 0) (↑n : R)) (↑(n.descFactorial 0) : R)
succ :
  ∀ (k : ℕ) (ih : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(n.descFactorial k) : R)),
    Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ (k + 1)) (↑n : R)) (↑(n.descFactorial (k + 1)) : R)
⊢ Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(n.descFactorial k) : R)

Tactic:
induction k with
  | zero =>
    rw [descPochhammer_zero, Nat.descFactorial_zero, Nat.cast_one, smeval_one, npow_zero, one_smul]
  | succ k ih =>
    rw [descPochhammer_succ_right, Nat.descFactorial_succ, smeval_mul, ih, mul_comm, Nat.cast_mul,
      smeval_sub, smeval_X, smeval_natCast, npow_one, npow_zero, nsmul_one]
    by_cases! h : n < k
    · simp only [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, zero_mul]
    · rw [Nat.cast_sub h]

Premises used: MulZeroClass.zero_mul, descPochhammer_succ_right, Polynomial.smeval_sub, Polynomial.smeval_natCast, npow_one, Polynomial.smeval_mul, npow_zero, Polynomial.smeval_X, one_smul, Nat.descFactorial_succ, Polynomial.smeval_one, Nat.cast_mul, mul_comm, Nat.descFactorial_zero, Nat.cast_zero, nsmul_one, Nat.cast_one, descPochhammer_zero
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
⊢ smeval (ascPochhammer ℕ 0) (-r) = Int.negOnePow (↑0 : ℤ) • smeval (descPochhammer ℤ 0) r

Tactic:
simp
-- Module: Mathlib.RingTheory.Binomial
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
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)
⊢ smeval (ascPochhammer ℕ (k + 1)) (-r) = Int.negOnePow (↑(k + 1) : ℤ) • smeval (descPochhammer ℤ (k + 1)) r

Tactic:
simp only [ascPochhammer_succ_right, smeval_mul, ih, descPochhammer_succ_right, sub_eq_add_neg]

Premises used: sub_eq_add_neg, descPochhammer_succ_right, Polynomial.smeval_mul, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Binomial
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
⊢ (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) = -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r

Tactic:
simp [smeval_natCast, add_comm]

Premises used: Polynomial.smeval_natCast, add_comm
-- Module: Mathlib.RingTheory.Binomial
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
⊢ (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) = -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r

Tactic:
have h : (X + (k : ℕ[X])).smeval (-r) = -(X + (-k : ℤ[X])).smeval r := by
      simp [smeval_natCast, add_comm]
-- Module: Mathlib.RingTheory.Binomial
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
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
⊢ smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) 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]

Premises used: Int.natCast_add, sub_eq_add_neg, descPochhammer_succ_right, Polynomial.smeval_mul, smul_mul_assoc, Int.natCast_one, Units.neg_smul, Units.smul_def, neg_mul_comm, neg_mul, Int.negOnePow_succ, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Binomial
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)
rw₄ rw₅ : (r + n - 1).descFactorial n = (r + n - 1).descFactorial n
⊢ 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]

Premises used: ascPochhammer_nat_eq_descFactorial, ascPochhammer, Nat, Nat.multichoose_eq, Polynomial.eval_eq_smeval, smul_eq_mul, Nat.descFactorial_eq_factorial_mul_choose
-- Module: Mathlib.RingTheory.Binomial
Goal:
r : ℤ
k : ℕ
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
⊢ k.factorial • r.multichoose k = smeval (ascPochhammer ℕ k) r

Tactic:
rw [Int.multichoose.eq_def, nsmul_eq_mul]

Premises used: Int.multichoose.eq_def, nsmul_eq_mul
-- Module: Mathlib.RingTheory.Binomial
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)) : ℤ)
ofNat₃ ofNat₄ : Eq (α := ℤ) (↑((n + k - 1).descFactorial k) : ℤ) (↑((n + k - 1).descFactorial k) : ℤ)
⊢ Eq (α := ℤ) (↑(k.factorial * (n + k - 1).choose k) : ℤ) (smeval (ascPochhammer ℕ k) (↑n : ℤ))

Tactic:
rw [← Nat.descFactorial_eq_factorial_mul_choose, smeval_at_natCast, ← eval_eq_smeval n,
        ascPochhammer_nat_eq_descFactorial]

Premises used: ascPochhammer_nat_eq_descFactorial, Polynomial.smeval_at_natCast, Polynomial.eval_eq_smeval, Nat.descFactorial_eq_factorial_mul_choose
-- Module: Mathlib.RingTheory.Binomial
Goal:
k n : ℕ
negSucc :
  (↑(negOnePow (↑k : ℤ)) : ℤ) * smeval (descPochhammer ℤ k) (↑(n + 1) : ℤ) =
    HSMul.hSMul (β := ℤ) (negOnePow (↑k : ℤ)) (smeval (descPochhammer ℤ k) (↑n.succ : ℤ))
⊢ (↑k.factorial : ℤ) * ((↑(negOnePow (↑k : ℤ)) : ℤ) * (↑((n + 1).choose k) : ℤ)) = smeval (ascPochhammer ℕ k) -[n+1]

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]

Premises used: Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer, mul_assoc, Polynomial.descPochhammer_smeval_eq_descFactorial, Int.neg_ofNat_succ, Nat.cast_mul, Nat.factorial, mul_comm, Nat.descFactorial_eq_factorial_mul_choose
-- Module: Mathlib.RingTheory.Binomial
Goal:
k n : ℕ
⊢ (↑(negOnePow (↑k : ℤ)) : ℤ) * smeval (descPochhammer ℤ k) (↑(n + 1) : ℤ) =
    HSMul.hSMul (β := ℤ) (negOnePow (↑k : ℤ)) (smeval (descPochhammer ℤ k) (↑n.succ : ℤ))

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.Binomial
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)
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]
⊢ 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

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

Premises used: Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer, ascPochhammer_nat_eq_descFactorial, mul_assoc, Polynomial.descPochhammer_smeval_eq_descFactorial, Int.ofNat_eq_natCast, Int.ofNat, Polynomial.smeval_at_natCast, Int.neg_ofNat_succ, Nat.cast_mul, Nat.factorial, Int.ofNat_mul_ofNat, mul_comm, Int.negSucc, Nat.descFactorial_eq_factorial_mul_choose
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Module ℚ≥0 R
inst_2 : Pow R ℕ
r : R
n : ℕ
match_scalars : (↑n.factorial : ℚ≥0) * HMul.hMul (α := ℚ≥0) (↑n.factorial : ℚ≥0)⁻¹ 1 = 1
⊢ n.factorial • HSMul.hSMul (α := ℚ≥0) (↑n.factorial : ℚ≥0)⁻¹ (smeval (ascPochhammer ℕ n) r) =
    smeval (ascPochhammer ℕ n) r

Tactic:
match_scalars
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : Module ℚ≥0 R
inst_2 : Pow R ℕ
r : R
n : ℕ
⊢ (↑n.factorial : ℚ≥0) * HMul.hMul (α := ℚ≥0) (↑n.factorial : ℚ≥0)⁻¹ 1 = 1

Tactic:
field
-- Module: Mathlib.RingTheory.Binomial
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
rw₉ rw₁₀ : Eq (α := ℤ) 1 1
⊢ 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]

Premises used: pow_zero, one_smul, Polynomial.smeval_one, ascPochhammer_zero, Nat.factorial_zero, Nat.cast_zero, neg_zero, Nat.cast_one, one_mul
-- Module: Mathlib.RingTheory.Binomial
Goal:
n : ℕ
⊢ HAdd.hAdd (α := ℤ) (-1) (-(↑n : ℤ)) = -1 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Binomial
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
rw₁₂ rw₁₃ : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑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]

Premises used: Nat.cast_id, Polynomial.C_eq_natCast, Polynomial.smeval_C, Polynomial.smeval_mul, Polynomial.smeval_X, pow_zero, MulZeroClass.mul_zero, neg_add_cancel, pow_one, nsmul_eq_mul, Polynomial.smeval_add, mul_one, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Binomial
Goal:
n : ℕ
rw : Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) 0
rw₁ rw₂ : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + 0 + 1)) (-(↑n : ℤ))) 0

Tactic:
rw [add_zero, smeval_ascPochhammer_succ_neg]

Premises used: Ring.smeval_ascPochhammer_succ_neg, add_zero
-- Module: Mathlib.RingTheory.Binomial
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
rw₂ :
  HMul.hMul (α := ℤ) (smeval (ascPochhammer ℕ (n + k + 1)) (-(↑n : ℤ)))
      ((HAdd.hAdd (α := ℕ[X]) X (↑(n + k + 1) : ℕ[X])).smeval (-(↑n : ℤ))) =
    0
rw₃ : HMul.hMul (α := ℤ) 0 ((HAdd.hAdd (α := ℕ[X]) X (↑(n + k + 1) : ℕ[X])).smeval (-(↑n : ℤ))) = 0
rw₄ rw₅ : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + (k + 1) + 1)) (-(↑n : ℤ))) 0

Tactic:
rw [ascPochhammer_succ_right, smeval_mul, ← add_assoc, smeval_ascPochhammer_neg_add n k,
      zero_mul]

Premises used: add_assoc, MulZeroClass.zero_mul, Polynomial.smeval_mul, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Binomial
Goal:
n k : ℕ
h : n < k
⊢ k = n + (k - n - 1) + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.Binomial
Goal:
n k : ℕ
h : n < k
rw : Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + (k - n - 1) + 1)) (-(↑n : ℤ))) 0
rw₁ rw₂ : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ k) (-(↑n : ℤ))) 0

Tactic:
rw [show k = n + (k - n - 1) + 1 by lia, smeval_ascPochhammer_neg_add]

Premises used: Ring.smeval_ascPochhammer_neg_add
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n k : ℕ
rw rw₁ : Eq.{u_2 + 1} (α := R) (↑(smeval (ascPochhammer ℕ k) n) : R) (↑(smeval (ascPochhammer ℕ k) n) : R)
⊢ Eq.{u_2 + 1} (α := R) (smeval (ascPochhammer ℕ k) (↑n : R)) (↑(smeval (ascPochhammer ℕ k) n) : R)

Tactic:
rw [smeval_at_natCast (ascPochhammer ℕ k) n]

Premises used: ascPochhammer, Polynomial.smeval_at_natCast, Nat