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 : 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)
rw₃ : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(k.factorial * 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)) (↑(n.descFactorial 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)
rw₃ : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(k.factorial * n.choose k) : R)
rw₄ : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (↑(n.descFactorial 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)) (smeval (descPochhammer ℤ k) (↑n : 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
r : R
⊢ multichoose (r - (↑0 : R) + 1) 0 = HPow.hPow (β := ℕ) (r + 1) 0
have rw : Nat.factorial 0 • multichoose (r - (↑0 : R) + 1) 0 = Nat.factorial 0 • HPow.hPow (β := ℕ) (r + 1) 0
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero 0)]
-- 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
⊢ choose r 0 = 1
have rw : HPow.hPow (β := ℕ) (r + 1) 0 = 1
Tactic: rw [choose_zero_right', npow_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
r : R
rw : HPow.hPow (β := ℕ) (r + 1) 0 = 1
⊢ choose r 0 = 1
have rw₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [choose_zero_right', npow_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
inst_3 : BinomialRing R
n : ℕ
⊢ Eq.{u_2 + 1} (α := R) (choose 0 (n + 1)) 0
have rw : multichoose (HSub.hSub (α := R) 0 (↑(n + 1) : R) + 1) (n + 1) = 0
Tactic: rw [choose, Nat.cast_succ, zero_sub, neg_add, neg_add_cancel_right, multichoose_succ_neg_natCast]
-- 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
inst_3 : BinomialRing R
n : ℕ
rw : multichoose (HSub.hSub (α := R) 0 (↑(n + 1) : R) + 1) (n + 1) = 0
⊢ Eq.{u_2 + 1} (α := R) (choose 0 (n + 1)) 0
have rw₁ : multichoose (0 - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (n + 1) = 0
Tactic: rw [choose, Nat.cast_succ, zero_sub, neg_add, neg_add_cancel_right, multichoose_succ_neg_natCast]
-- 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
inst_3 : BinomialRing R
n : ℕ
rw : multichoose (HSub.hSub (α := R) 0 (↑(n + 1) : R) + 1) (n + 1) = 0
rw₁ : multichoose (0 - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (n + 1) = 0
⊢ Eq.{u_2 + 1} (α := R) (choose 0 (n + 1)) 0
have rw₂ : multichoose (-HAdd.hAdd (α := R) (↑n : R) 1 + 1) (n + 1) = 0
Tactic: rw [choose, Nat.cast_succ, zero_sub, neg_add, neg_add_cancel_right, multichoose_succ_neg_natCast]
-- 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
inst_3 : BinomialRing R
n : ℕ
rw : multichoose (HSub.hSub (α := R) 0 (↑(n + 1) : R) + 1) (n + 1) = 0
rw₁ : multichoose (0 - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (n + 1) = 0
rw₂ : multichoose (-HAdd.hAdd (α := R) (↑n : R) 1 + 1) (n + 1) = 0
⊢ Eq.{u_2 + 1} (α := R) (choose 0 (n + 1)) 0
have rw₃ : multichoose (HAdd.hAdd (α := R) (-(↑n : R)) (-1) + 1) (n + 1) = 0
Tactic: rw [choose, Nat.cast_succ, zero_sub, neg_add, neg_add_cancel_right, multichoose_succ_neg_natCast]
-- 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
inst_3 : BinomialRing R
n : ℕ
rw : multichoose (HSub.hSub (α := R) 0 (↑(n + 1) : R) + 1) (n + 1) = 0
rw₁ : multichoose (0 - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (n + 1) = 0
rw₂ : multichoose (-HAdd.hAdd (α := R) (↑n : R) 1 + 1) (n + 1) = 0
rw₃ : multichoose (HAdd.hAdd (α := R) (-(↑n : R)) (-1) + 1) (n + 1) = 0
⊢ Eq.{u_2 + 1} (α := R) (choose 0 (n + 1)) 0
have rw₄ : Eq.{u_2 + 1} (α := R) (multichoose (-(↑n : R)) (n + 1)) 0
Tactic: rw [choose, Nat.cast_succ, zero_sub, neg_add, neg_add_cancel_right, multichoose_succ_neg_natCast]
-- 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
inst_3 : BinomialRing R
n : ℕ
rw : multichoose (HSub.hSub (α := R) 0 (↑(n + 1) : R) + 1) (n + 1) = 0
rw₁ : multichoose (0 - HAdd.hAdd (α := R) (↑n : R) 1 + 1) (n + 1) = 0
rw₂ : multichoose (-HAdd.hAdd (α := R) (↑n : R) 1 + 1) (n + 1) = 0
rw₃ : multichoose (HAdd.hAdd (α := R) (-(↑n : R)) (-1) + 1) (n + 1) = 0
rw₄ : Eq.{u_2 + 1} (α := R) (multichoose (-(↑n : R)) (n + 1)) 0
⊢ Eq.{u_2 + 1} (α := R) (choose 0 (n + 1)) 0
have rw₅ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [choose, Nat.cast_succ, zero_sub, neg_add, neg_add_cancel_right, multichoose_succ_neg_natCast]
-- 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
inst_3 : BinomialRing R
k : ℕ
h_pos : 0 < k
⊢ Eq.{u_2 + 1} (α := R) (choose 0 k) 0
have rw : Eq.{u_2 + 1} (α := R) (choose 0 k.pred.succ) 0
Tactic: rw [← Nat.succ_pred_eq_of_pos h_pos, choose_zero_succ]
-- 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
inst_3 : BinomialRing R
k : ℕ
h_pos : 0 < k
rw : Eq.{u_2 + 1} (α := R) (choose 0 k.pred.succ) 0
⊢ Eq.{u_2 + 1} (α := R) (choose 0 k) 0
have rw₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [← Nat.succ_pred_eq_of_pos h_pos, choose_zero_succ]
-- 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
inst_3 : BinomialRing R
k : ℕ
⊢ Eq.{u_2 + 1} (α := R) (choose 0 k) (if k = 0 then 1 else 0)
have pos : ∀ (hk : k = 0), Eq.{u_2 + 1} (α := R) (choose 0 k) 1
Tactic: split_ifs with hk
-- 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
inst_3 : BinomialRing R
k : ℕ
pos : ∀ (hk : k = 0), Eq.{u_2 + 1} (α := R) (choose 0 k) 1
⊢ Eq.{u_2 + 1} (α := R) (choose 0 k) (if k = 0 then 1 else 0)
have neg : ∀ (hk : ¬k = 0), Eq.{u_2 + 1} (α := R) (choose 0 k) 0
Tactic: split_ifs with hk
-- 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
inst_3 : BinomialRing R
k : ℕ
hk : k = 0
⊢ Eq.{u_2 + 1} (α := R) (choose 0 k) 1
have pos : Eq.{u_2 + 1} (α := R) (choose 0 0) 1
Tactic: rw [hk, choose_zero_right]
-- 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
inst_3 : BinomialRing R
k : ℕ
hk : k = 0
pos : Eq.{u_2 + 1} (α := R) (choose 0 0) 1
⊢ Eq.{u_2 + 1} (α := R) (choose 0 k) 1
have pos₁ : Eq.{u_2 + 1} (α := R) 1 1
Tactic: rw [hk, choose_zero_right]
-- 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
inst_3 : BinomialRing R
k : ℕ
hk : ¬k = 0
⊢ Eq.{u_2 + 1} (α := R) (choose 0 k) 0
have neg : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [choose_zero_pos R <| Nat.pos_of_ne_zero hk]
-- 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
⊢ choose r 1 = HPow.hPow (β := ℕ) r 1
have rw : multichoose (r - (↑1 : R) + 1) 1 = HPow.hPow (β := ℕ) r 1
Tactic: rw [choose, Nat.cast_one, sub_add_cancel, multichoose_one_right']
-- 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
rw : multichoose (r - (↑1 : R) + 1) 1 = HPow.hPow (β := ℕ) r 1
⊢ choose r 1 = HPow.hPow (β := ℕ) r 1
have rw₁ : multichoose (r - 1 + 1) 1 = HPow.hPow (β := ℕ) r 1
Tactic: rw [choose, Nat.cast_one, sub_add_cancel, multichoose_one_right']
-- 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
rw : multichoose (r - (↑1 : R) + 1) 1 = HPow.hPow (β := ℕ) r 1
rw₁ : multichoose (r - 1 + 1) 1 = HPow.hPow (β := ℕ) r 1
⊢ choose r 1 = HPow.hPow (β := ℕ) r 1
have rw₂ : multichoose r 1 = HPow.hPow (β := ℕ) r 1
Tactic: rw [choose, Nat.cast_one, sub_add_cancel, multichoose_one_right']
-- 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
rw : multichoose (r - (↑1 : R) + 1) 1 = HPow.hPow (β := ℕ) r 1
rw₁ : multichoose (r - 1 + 1) 1 = HPow.hPow (β := ℕ) r 1
rw₂ : multichoose r 1 = HPow.hPow (β := ℕ) r 1
⊢ choose r 1 = HPow.hPow (β := ℕ) r 1
have rw₃ : HPow.hPow (β := ℕ) r 1 = HPow.hPow (β := ℕ) r 1
Tactic: rw [choose, Nat.cast_one, sub_add_cancel, multichoose_one_right']
-- 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
⊢ choose r 1 = r
have rw : HPow.hPow (β := ℕ) r 1 = r
Tactic: rw [choose_one_right', 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
rw : HPow.hPow (β := ℕ) r 1 = r
⊢ choose r 1 = r
have rw₁ : r = r
Tactic: rw [choose_one_right', 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 : ℕ
⊢ choose (-r) n = Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
have apply : n.factorial • choose (-r) n = n.factorial • Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
Tactic: apply (nsmul_right_inj (Nat.factorial_ne_zero n)).mp
-- 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 : ℕ
⊢ n.factorial • choose (-r) n = n.factorial • Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
have rw : smeval (descPochhammer ℤ n) (-r) = n.factorial • Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
Tactic: rw [← descPochhammer_eq_factorial_smul_choose, smul_comm,
    ← descPochhammer_eq_factorial_smul_choose, descPochhammer_smeval_eq_ascPochhammer,
    show (-r - n + 1) = -(r + n - 1) by abel, ascPochhammer_smeval_neg_eq_descPochhammer]
-- 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 : ℕ
rw : smeval (descPochhammer ℤ n) (-r) = n.factorial • Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
⊢ n.factorial • choose (-r) n = n.factorial • Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
have rw₁ : smeval (descPochhammer ℤ n) (-r) = Int.negOnePow (↑n : ℤ) • n.factorial • choose (r + (↑n : R) - 1) n
Tactic: rw [← descPochhammer_eq_factorial_smul_choose, smul_comm,
    ← descPochhammer_eq_factorial_smul_choose, descPochhammer_smeval_eq_ascPochhammer,
    show (-r - n + 1) = -(r + n - 1) by abel, ascPochhammer_smeval_neg_eq_descPochhammer]
-- 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 : ℕ
rw : smeval (descPochhammer ℤ n) (-r) = n.factorial • Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
rw₁ : smeval (descPochhammer ℤ n) (-r) = Int.negOnePow (↑n : ℤ) • n.factorial • choose (r + (↑n : R) - 1) n
⊢ n.factorial • choose (-r) n = n.factorial • Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
have rw₂ : smeval (descPochhammer ℤ n) (-r) = Int.negOnePow (↑n : ℤ) • smeval (descPochhammer ℤ n) (r + (↑n : R) - 1)
Tactic: rw [← descPochhammer_eq_factorial_smul_choose, smul_comm,
    ← descPochhammer_eq_factorial_smul_choose, descPochhammer_smeval_eq_ascPochhammer,
    show (-r - n + 1) = -(r + n - 1) by abel, ascPochhammer_smeval_neg_eq_descPochhammer]
-- 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 : ℕ
rw : smeval (descPochhammer ℤ n) (-r) = n.factorial • Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
rw₁ : smeval (descPochhammer ℤ n) (-r) = Int.negOnePow (↑n : ℤ) • n.factorial • choose (r + (↑n : R) - 1) n
rw₂ : smeval (descPochhammer ℤ n) (-r) = Int.negOnePow (↑n : ℤ) • smeval (descPochhammer ℤ n) (r + (↑n : R) - 1)
⊢ n.factorial • choose (-r) n = n.factorial • Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
have rw₃ : smeval (ascPochhammer ℕ n) (-r - (↑n : R) + 1) = Int.negOnePow (↑n : ℤ) • smeval (descPochhammer ℤ n) (r + (↑n : R) - 1)
Tactic: rw [← descPochhammer_eq_factorial_smul_choose, smul_comm,
    ← descPochhammer_eq_factorial_smul_choose, descPochhammer_smeval_eq_ascPochhammer,
    show (-r - n + 1) = -(r + n - 1) by abel, ascPochhammer_smeval_neg_eq_descPochhammer]
-- 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 : ℕ
rw : smeval (descPochhammer ℤ n) (-r) = n.factorial • Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
rw₁ : smeval (descPochhammer ℤ n) (-r) = Int.negOnePow (↑n : ℤ) • n.factorial • choose (r + (↑n : R) - 1) n
rw₂ : smeval (descPochhammer ℤ n) (-r) = Int.negOnePow (↑n : ℤ) • smeval (descPochhammer ℤ n) (r + (↑n : R) - 1)
rw₃ :
  smeval (ascPochhammer ℕ n) (-r - (↑n : R) + 1) =
    Int.negOnePow (↑n : ℤ) • smeval (descPochhammer ℤ n) (r + (↑n : R) - 1)
⊢ n.factorial • choose (-r) n = n.factorial • Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
have rw₄ : smeval (ascPochhammer ℕ n) (-(r + (↑n : R) - 1)) =
  Int.negOnePow (↑n : ℤ) • smeval (descPochhammer ℤ n) (r + (↑n : R) - 1)
Tactic: rw [← descPochhammer_eq_factorial_smul_choose, smul_comm,
    ← descPochhammer_eq_factorial_smul_choose, descPochhammer_smeval_eq_ascPochhammer,
    show (-r - n + 1) = -(r + n - 1) by abel, ascPochhammer_smeval_neg_eq_descPochhammer]
-- 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 : ℕ
rw : smeval (descPochhammer ℤ n) (-r) = n.factorial • Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
rw₁ : smeval (descPochhammer ℤ n) (-r) = Int.negOnePow (↑n : ℤ) • n.factorial • choose (r + (↑n : R) - 1) n
rw₂ : smeval (descPochhammer ℤ n) (-r) = Int.negOnePow (↑n : ℤ) • smeval (descPochhammer ℤ n) (r + (↑n : R) - 1)
rw₃ :
  smeval (ascPochhammer ℕ n) (-r - (↑n : R) + 1) =
    Int.negOnePow (↑n : ℤ) • smeval (descPochhammer ℤ n) (r + (↑n : R) - 1)
rw₄ :
  smeval (ascPochhammer ℕ n) (-(r + (↑n : R) - 1)) =
    Int.negOnePow (↑n : ℤ) • smeval (descPochhammer ℤ n) (r + (↑n : R) - 1)
⊢ n.factorial • choose (-r) n = n.factorial • Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
have rw₅ : Int.negOnePow (↑n : ℤ) • smeval (descPochhammer ℤ n) (r + (↑n : R) - 1) =
  Int.negOnePow (↑n : ℤ) • smeval (descPochhammer ℤ n) (r + (↑n : R) - 1)
Tactic: rw [← descPochhammer_eq_factorial_smul_choose, smul_comm,
    ← descPochhammer_eq_factorial_smul_choose, descPochhammer_smeval_eq_ascPochhammer,
    show (-r - n + 1) = -(r + n - 1) by abel, ascPochhammer_smeval_neg_eq_descPochhammer]
-- 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 : ℕ
⊢ choose (-r) n = Int.negOnePow (↑n : ℤ) • multichoose r n
have rw : Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n = Int.negOnePow (↑n : ℤ) • multichoose r n
Tactic: rw [choose_neg, multichoose_eq]
-- 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 : ℕ
rw : Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n = Int.negOnePow (↑n : ℤ) • multichoose r n
⊢ choose (-r) n = Int.negOnePow (↑n : ℤ) • multichoose r n
have rw₁ : Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n = Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
Tactic: rw [choose_neg, multichoose_eq]
-- 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
k : ℕ
⊢ (X * Polynomial.comp (descPochhammer ℤ k) (HSub.hSub (α := ℤ[X]) X 1)).smeval (r + 1) =
    (k + 1) • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ (k + 1)) r
have rw : (X * Polynomial.comp (descPochhammer ℤ k) (HSub.hSub (α := ℤ[X]) X 1)).smeval (r + 1) =
  (k + 1) • smeval (descPochhammer ℤ k) r + (HSub.hSub (α := ℤ[X]) X (↑k : ℤ[X]) * descPochhammer ℤ k).smeval r
Tactic: rw [descPochhammer_succ_right, mul_comm (descPochhammer ℤ k)]
-- 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
k : ℕ
⊢ (X * Polynomial.comp (descPochhammer ℤ k) (HSub.hSub (α := ℤ[X]) X 1)).smeval (r + 1) =
    (k + 1) • smeval (descPochhammer ℤ k) r + (HSub.hSub (α := ℤ[X]) X (↑k : ℤ[X]) * descPochhammer ℤ k).smeval r
have simp : r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
  k • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r +
    (r * smeval (descPochhammer ℤ k) r - smeval (R := ℤ) (↑k : ℤ[X]) r * smeval (descPochhammer ℤ k) r)
Tactic: simp only [smeval_comp, smeval_sub, smeval_mul, smeval_X, smeval_one, npow_one,
    npow_zero, one_smul, add_sub_cancel_right, sub_mul, add_mul, add_smul, one_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
k : ℕ
⊢ r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    k • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - smeval (R := ℤ) (↑k : ℤ[X]) r * smeval (descPochhammer ℤ k) r)
have rw : r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
  k • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r +
    (r * smeval (descPochhammer ℤ k) r -
      smeval (R := ℤ) ((C : (a : ℤ) → ℤ[X]) (↑k : ℤ)) r * smeval (descPochhammer ℤ k) r)
Tactic: rw [← C_eq_natCast, smeval_C, npow_zero, add_comm (k • smeval (descPochhammer ℤ k) r) _,
    add_assoc, add_comm (k • smeval (descPochhammer ℤ k) r) _, ← add_assoc, ← add_sub_assoc,
    nsmul_eq_mul, zsmul_one, Int.cast_natCast, sub_add_cancel, add_comm]
-- 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
k : ℕ
rw :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    k • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r -
        smeval (R := ℤ) ((C : (a : ℤ) → ℤ[X]) (↑k : ℤ)) r * smeval (descPochhammer ℤ k) r)
⊢ r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    k • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - smeval (R := ℤ) (↑k : ℤ[X]) r * smeval (descPochhammer ℤ k) r)
have rw₁ : r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
  k • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r +
    (r * smeval (descPochhammer ℤ k) r -
      HSMul.hSMul (α := ℤ) (↑k : ℤ) (HPow.hPow (β := ℕ) r 0) * smeval (descPochhammer ℤ k) r)
Tactic: rw [← C_eq_natCast, smeval_C, npow_zero, add_comm (k • smeval (descPochhammer ℤ k) r) _,
    add_assoc, add_comm (k • smeval (descPochhammer ℤ k) r) _, ← add_assoc, ← add_sub_assoc,
    nsmul_eq_mul, zsmul_one, Int.cast_natCast, sub_add_cancel, add_comm]
-- 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
k : ℕ
rw :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    k • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r -
        smeval (R := ℤ) ((C : (a : ℤ) → ℤ[X]) (↑k : ℤ)) r * smeval (descPochhammer ℤ k) r)
rw₁ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    k • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r -
        HSMul.hSMul (α := ℤ) (↑k : ℤ) (HPow.hPow (β := ℕ) r 0) * smeval (descPochhammer ℤ k) r)
⊢ r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    k • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - smeval (R := ℤ) (↑k : ℤ[X]) r * smeval (descPochhammer ℤ k) r)
have rw₂ : r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
  k • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r +
    (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r)
Tactic: rw [← C_eq_natCast, smeval_C, npow_zero, add_comm (k • smeval (descPochhammer ℤ k) r) _,
    add_assoc, add_comm (k • smeval (descPochhammer ℤ k) r) _, ← add_assoc, ← add_sub_assoc,
    nsmul_eq_mul, zsmul_one, Int.cast_natCast, sub_add_cancel, add_comm]