awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Binomial
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
rw₅ rw₆ : HPow.hPow (α := ℤ) (-1) n * (↑n.factorial : ℤ) = HPow.hPow (α := ℤ) (-1) n * (↑n.factorial : ℤ)
⊢ multichoose (-(↑n : ℤ)) n = 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]

Premises used: Nat.cast_comm, Ring.factorial_nsmul_multichoose_eq_ascPochhammer, nsmul_right_inj, Nat.factorial_ne_zero, nsmul_eq_mul, Ring.smeval_ascPochhammer_self_neg
-- Module: Mathlib.RingTheory.Binomial
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
rw₄ rw₅ : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) (n + 1)) 0

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero _),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_succ_neg, smul_zero]

Premises used: smul_zero, Ring.factorial_nsmul_multichoose_eq_ascPochhammer, nsmul_right_inj, Nat.factorial_ne_zero, Ring.smeval_ascPochhammer_succ_neg
-- Module: Mathlib.RingTheory.Binomial
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
rw₃ rw₄ : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) (n + k + 1)) 0

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + k + 1)),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_neg_add, smul_zero]

Premises used: smul_zero, Ring.factorial_nsmul_multichoose_eq_ascPochhammer, nsmul_right_inj, Nat.factorial_ne_zero, HAdd.hAdd, Ring.smeval_ascPochhammer_neg_add, OfNat.ofNat
-- Module: Mathlib.RingTheory.Binomial
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
rw₃ rw₄ : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ) (multichoose (-(↑n : ℤ)) k) 0

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero k),
    factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_neg_of_lt h, smul_zero]

Premises used: smul_zero, Ring.factorial_nsmul_multichoose_eq_ascPochhammer, nsmul_right_inj, Nat.factorial_ne_zero, Ring.smeval_ascPochhammer_neg_of_lt
-- Module: Mathlib.RingTheory.Binomial
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
rw₅ rw₆ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) (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]

Premises used: Int.cast_zero, Polynomial.smeval_neg_nat, smul_zero, Ring.factorial_nsmul_multichoose_eq_ascPochhammer, nsmul_right_inj, Nat.factorial_ne_zero, HAdd.hAdd, Ring.smeval_ascPochhammer_succ_neg, OfNat.ofNat
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
⊢ smeval (ascPochhammer ℤ 0) r = smeval (ascPochhammer ℕ 0) r

Tactic:
simp only [ascPochhammer_zero, smeval_one]

Premises used: Polynomial.smeval_one, ascPochhammer_zero
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
n : ℕ
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
⊢ smeval (ascPochhammer ℤ (n + 1)) r = smeval (ascPochhammer ℕ (n + 1)) r

Tactic:
simp only [ascPochhammer_succ_right, smeval_mul]

Premises used: Polynomial.smeval_mul, ascPochhammer_succ_right
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
n : ℕ
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
⊢ 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]
-- Module: Mathlib.RingTheory.Binomial
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

Tactic:
simp only [smeval_add, smeval_X, ← C_eq_natCast, smeval_C, natCast_zsmul, nsmul_eq_mul,
      Nat.cast_id]

Premises used: Nat.cast_id, Polynomial.C_eq_natCast, Polynomial.smeval_C, Polynomial.smeval_X, nsmul_eq_mul, Polynomial.smeval_add, natCast_zsmul
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
n : ℕ
e_r : r = r + (↑n : R) - 1 - (↑n : R) + 1
⊢ multichoose r n = multichoose (r + (↑n : R) - 1 - (↑n : R) + 1) n

Tactic:
congr
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
n : ℕ
⊢ r = r + (↑n : R) - 1 - (↑n : R) + 1

Tactic:
abel
-- Module: Mathlib.RingTheory.Binomial
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 (ascPochhammer ℤ n) (r + (HSub.hSub (α := ℤ[X]) 1 (↑n : ℤ[X])).smeval r) =
    smeval (ascPochhammer ℕ n) (r - (↑n : R) + 1)
⊢ smeval (descPochhammer ℤ n) r = n.factorial • choose r n

Tactic:
rw [choose, factorial_nsmul_multichoose_eq_ascPochhammer, descPochhammer_eq_ascPochhammer,
    smeval_comp, add_comm_sub, smeval_add, smeval_X, npow_one]

Premises used: npow_one, Ring.factorial_nsmul_multichoose_eq_ascPochhammer, Polynomial.smeval_X, descPochhammer_eq_ascPochhammer, Ring.choose, add_comm_sub, Polynomial.smeval_comp, Polynomial.smeval_add
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
n : ℕ
rw : HSub.hSub (α := ℤ) 1 (↑n : ℤ) • HPow.hPow (β := ℕ) r 0 = HSub.hSub (α := R) 1 (↑n : R)
⊢ (HSub.hSub (α := ℤ[X]) 1 (↑n : ℤ[X])).smeval r = HSub.hSub (α := R) 1 (↑n : R)

Tactic:
rw [← C_eq_natCast, ← C_1, ← C_sub, smeval_C]

Premises used: Polynomial.C_1, Polynomial.C_eq_natCast, Polynomial.smeval_C, Polynomial.C_sub
-- Module: Mathlib.RingTheory.Binomial
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 (α := ℤ) 1 (↑n : ℤ) • HPow.hPow (β := ℕ) r 0 = HSub.hSub (α := R) 1 (↑n : R)

Tactic:
simp only [npow_zero, zsmul_one, Int.cast_sub, Int.cast_one, Int.cast_natCast]

Premises used: Int.cast_natCast, Int.cast_sub, npow_zero, zsmul_one, Int.cast_one
-- Module: Mathlib.RingTheory.Binomial
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)

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]
-- Module: Mathlib.RingTheory.Binomial
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)
rw₂ rw₃ :
  smeval (ascPochhammer ℕ n) (r + HSub.hSub (α := R) 1 (↑n : R)) =
    smeval (ascPochhammer ℕ n) (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)

Tactic:
rw [h, ascPochhammer_smeval_cast, add_comm_sub]

Premises used: Polynomial.ascPochhammer_smeval_cast, add_comm_sub
-- Module: Mathlib.RingTheory.Binomial
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)
rw₅ rw₆ : Eq.{u_1 + 1} (α := R) (smeval (descPochhammer ℤ k) (↑n : R)) (smeval (descPochhammer ℤ k) (↑n : R))
⊢ Eq.{u_1 + 1} (α := R) (choose (↑n : R) k) (↑(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]

Premises used: Polynomial.descPochhammer_smeval_eq_descFactorial, nsmul_right_inj, Nat.factorial_ne_zero, Nat.cast_mul, nsmul_eq_mul, Ring.descPochhammer_eq_factorial_smul_choose, Nat.descFactorial_eq_factorial_mul_choose
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
rw : Nat.factorial 0 • multichoose (r - (↑0 : R) + 1) 0 = Nat.factorial 0 • HPow.hPow (β := ℕ) (r + 1) 0
⊢ multichoose (r - (↑0 : R) + 1) 0 = HPow.hPow (β := ℕ) (r + 1) 0

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero 0)]

Premises used: nsmul_right_inj, Nat.factorial_ne_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
r : R
⊢ Nat.factorial 0 • multichoose (r - (↑0 : R) + 1) 0 = Nat.factorial 0 • HPow.hPow (β := ℕ) (r + 1) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Binomial
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ choose r 0 = 1

Tactic:
rw [choose_zero_right', npow_zero]

Premises used: npow_zero, Ring.choose_zero_right'
-- Module: Mathlib.RingTheory.Binomial
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
rw₅ rw₆ : Eq.{u_2 + 1} (α := R) 0 0
⊢ Eq.{u_2 + 1} (α := R) (choose 0 (n + 1)) 0

Tactic:
rw [choose, Nat.cast_succ, zero_sub, neg_add, neg_add_cancel_right, multichoose_succ_neg_natCast]

Premises used: Nat.cast_succ, neg_add, Ring.multichoose_succ_neg_natCast, Ring.choose, neg_add_cancel_right, zero_sub
-- Module: Mathlib.RingTheory.Binomial
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
rw₁ rw₂ : Eq.{u_2 + 1} (α := R) 0 0
⊢ Eq.{u_2 + 1} (α := R) (choose 0 k) 0

Tactic:
rw [← Nat.succ_pred_eq_of_pos h_pos, choose_zero_succ]

Premises used: Nat.succ_pred_eq_of_pos, Ring.choose_zero_succ
-- Module: Mathlib.RingTheory.Binomial
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
neg : ∀ (hk : ¬k = 0), Eq.{u_2 + 1} (α := R) (choose 0 k) 0
⊢ Eq.{u_2 + 1} (α := R) (choose 0 k) (if k = 0 then 1 else 0)

Tactic:
split_ifs with hk
-- Module: Mathlib.RingTheory.Binomial
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
pos₁ pos₂ : Eq.{u_2 + 1} (α := R) 1 1
⊢ Eq.{u_2 + 1} (α := R) (choose 0 k) 1

Tactic:
rw [hk, choose_zero_right]

Premises used: Ring.choose_zero_right
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
inst_3 : BinomialRing R
k : ℕ
hk : ¬k = 0
neg neg₁ : Eq.{u_2 + 1} (α := R) 0 0
⊢ Eq.{u_2 + 1} (α := R) (choose 0 k) 0

Tactic:
rw [choose_zero_pos R <| Nat.pos_of_ne_zero hk]

Premises used: Ring.choose_zero_pos, Nat.pos_of_ne_zero
-- Module: Mathlib.RingTheory.Binomial
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
rw₃ rw₄ : HPow.hPow (β := ℕ) r 1 = HPow.hPow (β := ℕ) r 1
⊢ choose r 1 = HPow.hPow (β := ℕ) r 1

Tactic:
rw [choose, Nat.cast_one, sub_add_cancel, multichoose_one_right']

Premises used: Ring.choose, Ring.multichoose_one_right', sub_add_cancel, Nat.cast_one
-- Module: Mathlib.RingTheory.Binomial
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
rw₁ rw₂ : r = r
⊢ choose r 1 = r

Tactic:
rw [choose_one_right', npow_one]

Premises used: Ring.choose_one_right', npow_one
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
n : ℕ
apply : n.factorial • choose (-r) n = n.factorial • Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
⊢ choose (-r) n = Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n

Tactic:
apply (nsmul_right_inj (Nat.factorial_ne_zero n)).mp

Premises used: nsmul_right_inj, Nat.factorial_ne_zero, Iff.mp
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
n : ℕ
⊢ -r - (↑n : R) + 1 = -(r + (↑n : R) - 1)

Tactic:
abel
-- Module: Mathlib.RingTheory.Binomial
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)
rw₅ rw₆ :
  Int.negOnePow (↑n : ℤ) • smeval (descPochhammer ℤ 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

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]

Premises used: Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer, Ring.descPochhammer_eq_factorial_smul_choose, SMulCommClass.smul_comm, Polynomial.descPochhammer_smeval_eq_ascPochhammer
-- Module: Mathlib.RingTheory.Binomial
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
rw₁ rw₂ : Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n = Int.negOnePow (↑n : ℤ) • choose (r + (↑n : R) - 1) n
⊢ choose (-r) n = Int.negOnePow (↑n : ℤ) • multichoose r n

Tactic:
rw [choose_neg, multichoose_eq]

Premises used: Ring.choose_neg, Ring.multichoose_eq
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
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
⊢ (X * Polynomial.comp (descPochhammer ℤ k) (HSub.hSub (α := ℤ[X]) X 1)).smeval (r + 1) =
    (k + 1) • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ (k + 1)) r

Tactic:
rw [descPochhammer_succ_right, mul_comm (descPochhammer ℤ k)]

Premises used: descPochhammer, descPochhammer_succ_right, Int, mul_comm
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
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)
⊢ (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:
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]

Premises used: add_mul, Polynomial.smeval_sub, npow_one, Polynomial.smeval_mul, npow_zero, Polynomial.smeval_X, one_smul, sub_mul, Polynomial.smeval_one, add_smul, Polynomial.smeval_comp, add_sub_cancel_right, one_mul
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
k : ℕ
rw : (k + 1).factorial • choose (r + 1) (k + 1) = (k + 1).factorial • (choose r k + choose r (k + 1))
⊢ choose (r + 1) (k + 1) = choose r k + choose r (k + 1)

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1))]

Premises used: nsmul_right_inj, Nat.factorial_ne_zero, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
k : ℕ
simp : smeval (descPochhammer ℤ (k + 1)) (r + 1) = (k + 1).factorial • choose r k + smeval (descPochhammer ℤ (k + 1)) r
⊢ (k + 1).factorial • choose (r + 1) (k + 1) = (k + 1).factorial • (choose r k + choose r (k + 1))

Tactic:
simp only [smul_add, ← descPochhammer_eq_factorial_smul_choose]

Premises used: Ring.descPochhammer_eq_factorial_smul_choose, smul_add
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
k : ℕ
rw :
  smeval (descPochhammer ℤ (k + 1)) (r + 1) = ((k + 1) * k.factorial) • choose r k + smeval (descPochhammer ℤ (k + 1)) r
rw₁ :
  smeval (descPochhammer ℤ (k + 1)) (r + 1) = (k + 1) • k.factorial • choose r k + smeval (descPochhammer ℤ (k + 1)) r
rw₂ :
  smeval (descPochhammer ℤ (k + 1)) (r + 1) =
    (k + 1) • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ (k + 1)) r
rw₃ rw₄ :
  (k + 1) • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ (k + 1)) r =
    (k + 1) • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ (k + 1)) r
⊢ smeval (descPochhammer ℤ (k + 1)) (r + 1) = (k + 1).factorial • choose r k + smeval (descPochhammer ℤ (k + 1)) r

Tactic:
rw [Nat.factorial_succ, mul_smul,
    ← descPochhammer_eq_factorial_smul_choose r, descPochhammer_succ_succ_smeval r k]

Premises used: Nat.factorial_succ, Ring.descPochhammer_eq_factorial_smul_choose, Ring.descPochhammer_succ_succ_smeval, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
rw :
  n.choose k • smeval (descPochhammer ℤ n) r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
⊢ n.choose k • choose r n = choose r k * choose (r - (↑k : R)) (n - k)

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero n),
    nsmul_left_comm, ← descPochhammer_eq_factorial_smul_choose,
    ← Nat.choose_mul_factorial_mul_factorial hkn, ← smul_mul_smul_comm,
    ← descPochhammer_eq_factorial_smul_choose, mul_nsmul',
    ← descPochhammer_eq_factorial_smul_choose, smul_mul_assoc]

Premises used: mul_nsmul', smul_mul_assoc, Nat.choose_mul_factorial_mul_factorial, smul_mul_smul_comm, nsmul_right_inj, Nat.factorial_ne_zero, Ring.descPochhammer_eq_factorial_smul_choose, nsmul_left_comm
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
n k : ℕ
hkn : k ≤ n
nth_rw :
  n.choose k • smeval (descPochhammer ℤ (n - k + k)) r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
⊢ n.choose k • smeval (descPochhammer ℤ n) r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))

Tactic:
nth_rw 2 [← Nat.sub_add_cancel hkn]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
n k : ℕ
rw : choose (r + (↑k : R)) k * choose (r + (↑k : R) - (↑k : R)) (n + k - k) = choose (r + (↑k : R)) k * choose r n
rw₁ : choose (r + (↑k : R)) k * choose (r + (↑k : R) - (↑k : R)) n = choose (r + (↑k : R)) k * choose r n
rw₂ rw₃ : choose (r + (↑k : R)) k * choose r n = choose (r + (↑k : R)) k * choose r n
⊢ (n + k).choose k • choose (r + (↑k : R)) (n + k) = choose (r + (↑k : R)) k * choose r n

Tactic:
rw [choose_smul_choose (r + k) (Nat.le_add_left k n), Nat.add_sub_cancel,
    add_sub_cancel_right]

Premises used: Nat.le_add_left, Nat.cast, HAdd.hAdd, Nat.add_sub_cancel, add_sub_cancel_right, Ring.choose_smul_choose
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : Field R
inst_1 : CharZero R
a : R
n : ℕ
ha : Ne.{u_1 + 1} (α := R) (↑n.factorial : R) 0
⊢ choose a n = HSMul.hSMul (α := R) (↑n.factorial : R)⁻¹ (smeval (descPochhammer ℤ n) a)

Tactic:
rw [Ring.descPochhammer_eq_factorial_smul_choose, ← Nat.cast_smul_eq_nsmul R, inv_smul_smul₀]

Premises used: inv_smul_smul₀, Nat.cast_smul_eq_nsmul, Ring.descPochhammer_eq_factorial_smul_choose
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : Field R
inst_1 : CharZero R
a : R
n : ℕ
⊢ Ne.{u_1 + 1} (α := R) (↑n.factorial : R) 0

Tactic:
simpa using Nat.factorial_ne_zero n

Premises used: Nat.factorial_ne_zero
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Commute r s
⊢ smeval (descPochhammer ℤ 0) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ 0,
      (↑(Nat.choose 0 ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)

Tactic:
simp