awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 (α := ℤ) 0 ((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
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
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + (k + 1) + 1)) (-(↑n : ℤ))) 0
have rw₄ : Eq (α := ℤ) 0 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 : ℕ
h : n < k
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ k) (-(↑n : ℤ))) 0
have rw : Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + (k - n - 1) + 1)) (-(↑n : ℤ))) 0
Tactic: rw [show k = n + (k - n - 1) + 1 by lia, smeval_ascPochhammer_neg_add]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n k : ℕ
h : n < k
rw : Eq (α := ℤ) (smeval (ascPochhammer ℕ (n + (k - n - 1) + 1)) (-(↑n : ℤ))) 0
⊢ Eq (α := ℤ) (smeval (ascPochhammer ℕ k) (-(↑n : ℤ))) 0
have rw₁ : Eq (α := ℤ) 0 0
Tactic: rw [show k = n + (k - n - 1) + 1 by lia, smeval_ascPochhammer_neg_add]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocSemiring R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
n k : ℕ
⊢ Eq.{u_2 + 1} (α := R) (smeval (ascPochhammer ℕ k) (↑n : R)) (↑(smeval (ascPochhammer ℕ k) n) : R)
have rw : Eq.{u_2 + 1} (α := R) (↑(smeval (ascPochhammer ℕ k) n) : R) (↑(smeval (ascPochhammer ℕ k) n) : R)
Tactic: rw [smeval_at_natCast (ascPochhammer ℕ k) n]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
⊢ multichoose (-(↑n : ℤ)) n = HPow.hPow (α := ℤ) (-1) n
have rw : HSMul.hSMul (β := ℤ) n.factorial (multichoose (-(↑n : ℤ)) n) = n.factorial • HPow.hPow (α := ℤ) (-1) n
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero _),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_self_neg, nsmul_eq_mul,
    Nat.cast_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : HSMul.hSMul (β := ℤ) n.factorial (multichoose (-(↑n : ℤ)) n) = n.factorial • HPow.hPow (α := ℤ) (-1) n
rw₁ : ℕ
⊢ multichoose (-(↑n : ℤ)) n = HPow.hPow (α := ℤ) (-1) n
have rw₂ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) = n.factorial • HPow.hPow (α := ℤ) (-1) n
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero _),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_self_neg, nsmul_eq_mul,
    Nat.cast_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : HSMul.hSMul (β := ℤ) n.factorial (multichoose (-(↑n : ℤ)) n) = n.factorial • HPow.hPow (α := ℤ) (-1) n
rw₁ : ℕ
rw₂ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) = n.factorial • HPow.hPow (α := ℤ) (-1) n
⊢ multichoose (-(↑n : ℤ)) n = HPow.hPow (α := ℤ) (-1) n
have rw₃ : HPow.hPow (α := ℤ) (-1) n * (↑n.factorial : ℤ) = n.factorial • HPow.hPow (α := ℤ) (-1) n
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero _),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_self_neg, nsmul_eq_mul,
    Nat.cast_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : HSMul.hSMul (β := ℤ) n.factorial (multichoose (-(↑n : ℤ)) n) = n.factorial • HPow.hPow (α := ℤ) (-1) n
rw₁ : ℕ
rw₂ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) = n.factorial • HPow.hPow (α := ℤ) (-1) n
rw₃ : HPow.hPow (α := ℤ) (-1) n * (↑n.factorial : ℤ) = n.factorial • HPow.hPow (α := ℤ) (-1) n
⊢ multichoose (-(↑n : ℤ)) n = HPow.hPow (α := ℤ) (-1) n
have rw₄ : HPow.hPow (α := ℤ) (-1) n * (↑n.factorial : ℤ) = (↑n.factorial : ℤ) * HPow.hPow (α := ℤ) (-1) n
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero _),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_self_neg, nsmul_eq_mul,
    Nat.cast_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : HSMul.hSMul (β := ℤ) n.factorial (multichoose (-(↑n : ℤ)) n) = n.factorial • HPow.hPow (α := ℤ) (-1) n
rw₁ : ℕ
rw₂ : smeval (ascPochhammer ℕ n) (-(↑n : ℤ)) = n.factorial • HPow.hPow (α := ℤ) (-1) n
rw₃ : HPow.hPow (α := ℤ) (-1) n * (↑n.factorial : ℤ) = n.factorial • HPow.hPow (α := ℤ) (-1) n
rw₄ : HPow.hPow (α := ℤ) (-1) n * (↑n.factorial : ℤ) = (↑n.factorial : ℤ) * HPow.hPow (α := ℤ) (-1) n
⊢ multichoose (-(↑n : ℤ)) n = HPow.hPow (α := ℤ) (-1) n
have rw₅ : HPow.hPow (α := ℤ) (-1) n * (↑n.factorial : ℤ) = HPow.hPow (α := ℤ) (-1) n * (↑n.factorial : ℤ)
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero _),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_self_neg, nsmul_eq_mul,
    Nat.cast_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) (n + 1)) 0
have rw : HSMul.hSMul (β := ℤ) (n + 1).factorial (multichoose (-(↑n : ℤ)) (n + 1)) = HSMul.hSMul (β := ℤ) (n + 1).factorial 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero _),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_succ_neg, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : HSMul.hSMul (β := ℤ) (n + 1).factorial (multichoose (-(↑n : ℤ)) (n + 1)) = HSMul.hSMul (β := ℤ) (n + 1).factorial 0
rw₁ : ℕ
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) (n + 1)) 0
have rw₂ : smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ)) = HSMul.hSMul (β := ℤ) (n + 1).factorial 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero _),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_succ_neg, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : HSMul.hSMul (β := ℤ) (n + 1).factorial (multichoose (-(↑n : ℤ)) (n + 1)) = HSMul.hSMul (β := ℤ) (n + 1).factorial 0
rw₁ : ℕ
rw₂ : smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ)) = HSMul.hSMul (β := ℤ) (n + 1).factorial 0
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) (n + 1)) 0
have rw₃ : 0 = HSMul.hSMul (β := ℤ) (n + 1).factorial 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero _),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_succ_neg, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n : ℕ
rw : HSMul.hSMul (β := ℤ) (n + 1).factorial (multichoose (-(↑n : ℤ)) (n + 1)) = HSMul.hSMul (β := ℤ) (n + 1).factorial 0
rw₁ : ℕ
rw₂ : smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ)) = HSMul.hSMul (β := ℤ) (n + 1).factorial 0
rw₃ : 0 = HSMul.hSMul (β := ℤ) (n + 1).factorial 0
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) (n + 1)) 0
have rw₄ : Eq (α := ℤ) 0 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero _),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_succ_neg, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n k : ℕ
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) (n + k + 1)) 0
have rw : HSMul.hSMul (β := ℤ) (n + k + 1).factorial (multichoose (-(↑n : ℤ)) (n + k + 1)) =
  HSMul.hSMul (β := ℤ) (n + k + 1).factorial 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + k + 1)),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_neg_add, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n k : ℕ
rw :
  HSMul.hSMul (β := ℤ) (n + k + 1).factorial (multichoose (-(↑n : ℤ)) (n + k + 1)) =
    HSMul.hSMul (β := ℤ) (n + k + 1).factorial 0
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) (n + k + 1)) 0
have rw₁ : smeval (ascPochhammer ℕ (n + k + 1)) (-(↑n : ℤ)) = HSMul.hSMul (β := ℤ) (n + k + 1).factorial 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + k + 1)),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_neg_add, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n k : ℕ
rw :
  HSMul.hSMul (β := ℤ) (n + k + 1).factorial (multichoose (-(↑n : ℤ)) (n + k + 1)) =
    HSMul.hSMul (β := ℤ) (n + k + 1).factorial 0
rw₁ : smeval (ascPochhammer ℕ (n + k + 1)) (-(↑n : ℤ)) = HSMul.hSMul (β := ℤ) (n + k + 1).factorial 0
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) (n + k + 1)) 0
have rw₂ : 0 = HSMul.hSMul (β := ℤ) (n + k + 1).factorial 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + k + 1)),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_neg_add, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n k : ℕ
rw :
  HSMul.hSMul (β := ℤ) (n + k + 1).factorial (multichoose (-(↑n : ℤ)) (n + k + 1)) =
    HSMul.hSMul (β := ℤ) (n + k + 1).factorial 0
rw₁ : smeval (ascPochhammer ℕ (n + k + 1)) (-(↑n : ℤ)) = HSMul.hSMul (β := ℤ) (n + k + 1).factorial 0
rw₂ : 0 = HSMul.hSMul (β := ℤ) (n + k + 1).factorial 0
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) (n + k + 1)) 0
have rw₃ : Eq (α := ℤ) 0 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + k + 1)),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_neg_add, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n k : ℕ
h : n < k
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) k) 0
have rw : HSMul.hSMul (β := ℤ) k.factorial (multichoose (-(↑n : ℤ)) k) = HSMul.hSMul (β := ℤ) k.factorial 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero k),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_neg_of_lt h, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n k : ℕ
h : n < k
rw : HSMul.hSMul (β := ℤ) k.factorial (multichoose (-(↑n : ℤ)) k) = HSMul.hSMul (β := ℤ) k.factorial 0
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) k) 0
have rw₁ : smeval (ascPochhammer ℕ k) (-(↑n : ℤ)) = HSMul.hSMul (β := ℤ) k.factorial 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero k),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_neg_of_lt h, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n k : ℕ
h : n < k
rw : HSMul.hSMul (β := ℤ) k.factorial (multichoose (-(↑n : ℤ)) k) = HSMul.hSMul (β := ℤ) k.factorial 0
rw₁ : smeval (ascPochhammer ℕ k) (-(↑n : ℤ)) = HSMul.hSMul (β := ℤ) k.factorial 0
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) k) 0
have rw₂ : 0 = HSMul.hSMul (β := ℤ) k.factorial 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero k),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_neg_of_lt h, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
n k : ℕ
h : n < k
rw : HSMul.hSMul (β := ℤ) k.factorial (multichoose (-(↑n : ℤ)) k) = HSMul.hSMul (β := ℤ) k.factorial 0
rw₁ : smeval (ascPochhammer ℕ k) (-(↑n : ℤ)) = HSMul.hSMul (β := ℤ) k.factorial 0
rw₂ : 0 = HSMul.hSMul (β := ℤ) k.factorial 0
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) k) 0
have rw₃ : Eq (α := ℤ) 0 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero k),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_neg_of_lt h, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (multichoose (-(↑n : R)) (n + 1)) 0
have rw : HSMul.hSMul (β := R) (n + 1).factorial (multichoose (-(↑n : R)) (n + 1)) = HSMul.hSMul (β := R) (n + 1).factorial 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + 1)), smul_zero,
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_neg_nat,
    smeval_ascPochhammer_succ_neg n, Int.cast_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
n : ℕ
rw : HSMul.hSMul (β := R) (n + 1).factorial (multichoose (-(↑n : R)) (n + 1)) = HSMul.hSMul (β := R) (n + 1).factorial 0
⊢ Eq.{u_1 + 1} (α := R) (multichoose (-(↑n : R)) (n + 1)) 0
have rw₁ : HSMul.hSMul (β := R) (n + 1).factorial (multichoose (-(↑n : R)) (n + 1)) = 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + 1)), smul_zero,
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_neg_nat,
    smeval_ascPochhammer_succ_neg n, Int.cast_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
n : ℕ
rw : HSMul.hSMul (β := R) (n + 1).factorial (multichoose (-(↑n : R)) (n + 1)) = HSMul.hSMul (β := R) (n + 1).factorial 0
rw₁ : HSMul.hSMul (β := R) (n + 1).factorial (multichoose (-(↑n : R)) (n + 1)) = 0
⊢ Eq.{u_1 + 1} (α := R) (multichoose (-(↑n : R)) (n + 1)) 0
have rw₂ : Eq.{u_1 + 1} (α := R) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : R))) 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + 1)), smul_zero,
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_neg_nat,
    smeval_ascPochhammer_succ_neg n, Int.cast_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
n : ℕ
rw : HSMul.hSMul (β := R) (n + 1).factorial (multichoose (-(↑n : R)) (n + 1)) = HSMul.hSMul (β := R) (n + 1).factorial 0
rw₁ : HSMul.hSMul (β := R) (n + 1).factorial (multichoose (-(↑n : R)) (n + 1)) = 0
rw₂ : Eq.{u_1 + 1} (α := R) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : R))) 0
⊢ Eq.{u_1 + 1} (α := R) (multichoose (-(↑n : R)) (n + 1)) 0
have rw₃ : Eq.{u_1 + 1} (α := R) (↑(smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) : R) 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + 1)), smul_zero,
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_neg_nat,
    smeval_ascPochhammer_succ_neg n, Int.cast_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
n : ℕ
rw : HSMul.hSMul (β := R) (n + 1).factorial (multichoose (-(↑n : R)) (n + 1)) = HSMul.hSMul (β := R) (n + 1).factorial 0
rw₁ : HSMul.hSMul (β := R) (n + 1).factorial (multichoose (-(↑n : R)) (n + 1)) = 0
rw₂ : Eq.{u_1 + 1} (α := R) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : R))) 0
rw₃ : Eq.{u_1 + 1} (α := R) (↑(smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) : R) 0
⊢ Eq.{u_1 + 1} (α := R) (multichoose (-(↑n : R)) (n + 1)) 0
have rw₄ : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + 1)), smul_zero,
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_neg_nat,
    smeval_ascPochhammer_succ_neg n, Int.cast_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
n : ℕ
rw : HSMul.hSMul (β := R) (n + 1).factorial (multichoose (-(↑n : R)) (n + 1)) = HSMul.hSMul (β := R) (n + 1).factorial 0
rw₁ : HSMul.hSMul (β := R) (n + 1).factorial (multichoose (-(↑n : R)) (n + 1)) = 0
rw₂ : Eq.{u_1 + 1} (α := R) (smeval (ascPochhammer ℕ (n + 1)) (-(↑n : R))) 0
rw₃ : Eq.{u_1 + 1} (α := R) (↑(smeval (ascPochhammer ℕ (n + 1)) (-(↑n : ℤ))) : R) 0
rw₄ : Eq.{u_1 + 1} (α := R) (↑0 : R) 0
⊢ Eq.{u_1 + 1} (α := R) (multichoose (-(↑n : R)) (n + 1)) 0
have rw₅ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + 1)), smul_zero,
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_neg_nat,
    smeval_ascPochhammer_succ_neg n, Int.cast_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
n : ℕ
⊢ smeval (ascPochhammer ℤ (n + 1)) r = smeval (ascPochhammer ℕ (n + 1)) r
have simp : smeval (ascPochhammer ℤ n) r * (HAdd.hAdd (α := ℤ[X]) X (↑n : ℤ[X])).smeval r =
  smeval (ascPochhammer ℕ n) r * (HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval r
Tactic: simp only [ascPochhammer_succ_right, smeval_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
n : ℕ
⊢ smeval (ascPochhammer ℤ n) r * (HAdd.hAdd (α := ℤ[X]) X (↑n : ℤ[X])).smeval r =
    smeval (ascPochhammer ℕ n) r * (HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval r
have rw : smeval (ascPochhammer ℕ n) r * (HAdd.hAdd (α := ℤ[X]) X (↑n : ℤ[X])).smeval r =
  smeval (ascPochhammer ℕ n) r * (HAdd.hAdd (α := ℕ[X]) X (↑n : ℕ[X])).smeval r
Tactic: rw [smeval_ascPochhammer_int_ofNat r n]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
n : ℕ
⊢ multichoose r n = multichoose (r + (↑n : R) - 1 - (↑n : R) + 1) n
have e_r : r = r + (↑n : R) - 1 - (↑n : R) + 1
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
n : ℕ
⊢ smeval (descPochhammer ℤ n) r = n.factorial • choose r n
have rw : smeval (ascPochhammer ℤ n) (r + (HSub.hSub (α := ℤ[X]) 1 (↑n : ℤ[X])).smeval r) =
  smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
Tactic: rw [choose, factorial_nsmul_multichoose_eq_ascPochhammer, descPochhammer_eq_ascPochhammer,
    smeval_comp, add_comm_sub, smeval_add, smeval_X, npow_one]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
n : ℕ
⊢ (HSub.hSub (α := ℤ[X]) 1 (↑n : ℤ[X])).smeval r = HSub.hSub (α := R) 1 (↑n : R)
have rw : HSub.hSub (α := ℤ) 1 (↑n : ℤ) • HPow.hPow (β := ℕ) r 0 = HSub.hSub (α := R) 1 (↑n : R)
Tactic: rw [← C_eq_natCast, ← C_1, ← C_sub, smeval_C]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (hypothesis)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
n : ℕ
⊢ smeval (ascPochhammer ℤ n) (r + (HSub.hSub (α := ℤ[X]) 1 (↑n : ℤ[X])).smeval r) =
    smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
have h : (HSub.hSub (α := ℤ[X]) 1 (↑n : ℤ[X])).smeval r = HSub.hSub (α := R) 1 (↑n : R)
Tactic: have h : smeval (1 - n : Polynomial ℤ) r = 1 - n := by
    rw [← C_eq_natCast, ← C_1, ← C_sub, smeval_C]
    simp only [npow_zero, zsmul_one, Int.cast_sub, Int.cast_one, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
n : ℕ
h : (HSub.hSub (α := ℤ[X]) 1 (↑n : ℤ[X])).smeval r = HSub.hSub (α := R) 1 (↑n : R)
⊢ smeval (ascPochhammer ℤ n) (r + (HSub.hSub (α := ℤ[X]) 1 (↑n : ℤ[X])).smeval r) =
    smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
have rw : smeval (ascPochhammer ℤ n) (r + HSub.hSub (α := R) 1 (↑n : R)) = smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
Tactic: rw [h, ascPochhammer_smeval_cast, add_comm_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
n : ℕ
h : (HSub.hSub (α := ℤ[X]) 1 (↑n : ℤ[X])).smeval r = HSub.hSub (α := R) 1 (↑n : R)
rw : smeval (ascPochhammer ℤ n) (r + HSub.hSub (α := R) 1 (↑n : R)) = smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
⊢ smeval (ascPochhammer ℤ n) (r + (HSub.hSub (α := ℤ[X]) 1 (↑n : ℤ[X])).smeval r) =
    smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
have rw₁ : smeval (ascPochhammer ℕ n) (r + HSub.hSub (α := R) 1 (↑n : R)) = smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
Tactic: rw [h, ascPochhammer_smeval_cast, add_comm_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
n : ℕ
h : (HSub.hSub (α := ℤ[X]) 1 (↑n : ℤ[X])).smeval r = HSub.hSub (α := R) 1 (↑n : R)
rw : smeval (ascPochhammer ℤ n) (r + HSub.hSub (α := R) 1 (↑n : R)) = smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
rw₁ : smeval (ascPochhammer ℕ n) (r + HSub.hSub (α := R) 1 (↑n : R)) = smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
⊢ smeval (ascPochhammer ℤ n) (r + (HSub.hSub (α := ℤ[X]) 1 (↑n : ℤ[X])).smeval r) =
    smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
have rw₂ : smeval (ascPochhammer ℕ n) (r + HSub.hSub (α := R) 1 (↑n : R)) =
  smeval (ascPochhammer ℕ n) (r + HSub.hSub (α := R) 1 (↑n : R))
Tactic: rw [h, ascPochhammer_smeval_cast, add_comm_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
n k : ℕ
⊢ Eq.{u_1 + 1} (α := R) (choose (↑n : R) k) (↑(n.choose k) : R)
have rw : HSMul.hSMul (β := R) k.factorial (choose (↑n : R) k) = HSMul.hSMul (β := R) k.factorial (↑(n.choose k) : R)
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero k),
    ← descPochhammer_eq_factorial_smul_choose, nsmul_eq_mul, ← Nat.cast_mul,
    ← Nat.descFactorial_eq_factorial_mul_choose, ← descPochhammer_smeval_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
n k : ℕ
rw : HSMul.hSMul (β := R) k.factorial (choose (↑n : R) k) = HSMul.hSMul (β := R) k.factorial (↑(n.choose k) : R)
⊢ Eq.{u_1 + 1} (α := R) (choose (↑n : R) k) (↑(n.choose k) : R)
have rw₁ : smeval (descPochhammer ℤ k) (↑n : R) = HSMul.hSMul (β := R) k.factorial (↑(n.choose k) : R)
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero k),
    ← descPochhammer_eq_factorial_smul_choose, nsmul_eq_mul, ← Nat.cast_mul,
    ← Nat.descFactorial_eq_factorial_mul_choose, ← descPochhammer_smeval_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
n k : ℕ
rw : HSMul.hSMul (β := R) k.factorial (choose (↑n : R) k) = HSMul.hSMul (β := R) k.factorial (↑(n.choose k) : R)
rw₁ : smeval (descPochhammer ℤ k) (↑n : R) = HSMul.hSMul (β := R) k.factorial (↑(n.choose k) : R)
⊢ Eq.{u_1 + 1} (α := R) (choose (↑n : R) k) (↑(n.choose k) : R)
have rw₂ : smeval (descPochhammer ℤ k) (↑n : R) = HMul.hMul (α := R) (↑k.factorial : R) (↑(n.choose k) : R)
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero k),
    ← descPochhammer_eq_factorial_smul_choose, nsmul_eq_mul, ← Nat.cast_mul,
    ← Nat.descFactorial_eq_factorial_mul_choose, ← descPochhammer_smeval_eq_descFactorial]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
n k : ℕ
rw : HSMul.hSMul (β := R) k.factorial (choose (↑n : R) k) = HSMul.hSMul (β := R) k.factorial (↑(n.choose k) : R)
rw₁ : smeval (descPochhammer ℤ k) (↑n : R) = HSMul.hSMul (β := R) k.factorial (↑(n.choose k) : R)
rw₂ : smeval (descPochhammer ℤ k) (↑n : R) = HMul.hMul (α := R) (↑k.factorial : R) (↑(n.choose k) : R)
⊢ Eq.{u_1 + 1} (α := R) (choose (↑n : R) k) (↑(n.choose k) : R)
have rw₃ : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(k.factorial * n.choose k) : R)
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero k),
    ← descPochhammer_eq_factorial_smul_choose, nsmul_eq_mul, ← Nat.cast_mul,
    ← Nat.descFactorial_eq_factorial_mul_choose, ← descPochhammer_smeval_eq_descFactorial]