awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ 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 =
  smeval (descPochhammer ℤ k) r + k • 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]
-- 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)
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)
rw₃ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r + k • smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * 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 =
  smeval (descPochhammer ℤ k) r +
    (k • 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]
-- 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)
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)
rw₃ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r + k • smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r)
rw₄ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r +
      (k • smeval (descPochhammer ℤ k) r +
        (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * 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 =
  smeval (descPochhammer ℤ k) r +
    (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r +
      k • 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)
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)
rw₃ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r + k • smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r)
rw₄ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r +
      (k • smeval (descPochhammer ℤ k) r +
        (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r))
rw₅ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r +
        k • 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 =
  smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r) +
    k • 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)
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)
rw₃ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r + k • smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r)
rw₄ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r +
      (k • smeval (descPochhammer ℤ k) r +
        (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r))
rw₅ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r +
        k • smeval (descPochhammer ℤ k) r)
rw₆ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r +
        (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r) +
      k • 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 =
  smeval (descPochhammer ℤ k) r + r * smeval (descPochhammer ℤ k) r -
      HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r +
    k • 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)
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)
rw₃ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r + k • smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r)
rw₄ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r +
      (k • smeval (descPochhammer ℤ k) r +
        (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r))
rw₅ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r +
      (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r +
        k • smeval (descPochhammer ℤ k) r)
rw₆ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r +
        (r * smeval (descPochhammer ℤ k) r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r) +
      k • smeval (descPochhammer ℤ k) r
rw₇ :
  r * smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ k) r =
    smeval (descPochhammer ℤ k) r + r * smeval (descPochhammer ℤ k) r -
        HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r +
      k • 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 =
  smeval (descPochhammer ℤ k) r + r * smeval (descPochhammer ℤ k) r -
      HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1 * smeval (descPochhammer ℤ k) r +
    (↑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_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : BinomialRing R
inst_3 : NatPowAssoc R
r : R
k : ℕ
⊢ choose (r + 1) (k + 1) = choose r k + choose r (k + 1)
have rw : (k + 1).factorial • choose (r + 1) (k + 1) = (k + 1).factorial • (choose r k + choose r (k + 1))
Tactic: rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1))]
-- 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
k : ℕ
⊢ (k + 1).factorial • choose (r + 1) (k + 1) = (k + 1).factorial • (choose r k + choose r (k + 1))
have simp : smeval (descPochhammer ℤ (k + 1)) (r + 1) = (k + 1).factorial • choose r k + smeval (descPochhammer ℤ (k + 1)) r
Tactic: simp only [smul_add, ← descPochhammer_eq_factorial_smul_choose]
-- 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
k : ℕ
⊢ smeval (descPochhammer ℤ (k + 1)) (r + 1) = (k + 1).factorial • choose r k + smeval (descPochhammer ℤ (k + 1)) r
have rw : smeval (descPochhammer ℤ (k + 1)) (r + 1) = ((k + 1) * k.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]
-- 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
k : ℕ
rw :
  smeval (descPochhammer ℤ (k + 1)) (r + 1) = ((k + 1) * k.factorial) • choose r k + smeval (descPochhammer ℤ (k + 1)) r
⊢ smeval (descPochhammer ℤ (k + 1)) (r + 1) = (k + 1).factorial • choose r k + smeval (descPochhammer ℤ (k + 1)) r
have rw₁ : smeval (descPochhammer ℤ (k + 1)) (r + 1) = (k + 1) • k.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]
-- 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
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
⊢ smeval (descPochhammer ℤ (k + 1)) (r + 1) = (k + 1).factorial • choose r k + smeval (descPochhammer ℤ (k + 1)) r
have rw₂ : smeval (descPochhammer ℤ (k + 1)) (r + 1) =
  (k + 1) • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ (k + 1)) r
Tactic: rw [Nat.factorial_succ, mul_smul,
    ← descPochhammer_eq_factorial_smul_choose r, descPochhammer_succ_succ_smeval r k]
-- 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
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
⊢ smeval (descPochhammer ℤ (k + 1)) (r + 1) = (k + 1).factorial • choose r k + smeval (descPochhammer ℤ (k + 1)) r
have rw₃ : (k + 1) • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ (k + 1)) r =
  (k + 1) • smeval (descPochhammer ℤ k) r + smeval (descPochhammer ℤ (k + 1)) r
Tactic: rw [Nat.factorial_succ, mul_smul,
    ← descPochhammer_eq_factorial_smul_choose r, descPochhammer_succ_succ_smeval r k]
-- 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 k : ℕ
hkn : k ≤ n
⊢ n.choose k • choose r n = choose r k * choose (r - (↑k : R)) (n - k)
have rw : n.choose k • smeval (descPochhammer ℤ n) r =
  n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
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]
-- 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 k : ℕ
hkn : k ≤ n
⊢ n.choose k • smeval (descPochhammer ℤ n) r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
have 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)))
Tactic: nth_rw 2 [← Nat.sub_add_cancel hkn]
-- 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 k : ℕ
hkn : k ≤ n
⊢ n.choose k • smeval (descPochhammer ℤ (n - k + k)) r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
have rw : n.choose k • smeval (descPochhammer ℤ (k + (n - k))) r =
  n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
Tactic: rw [add_comm, ← descPochhammer_mul, smeval_mul, smeval_comp, smeval_sub, smeval_X,
    ← C_eq_natCast, smeval_C, npow_one, npow_zero, zsmul_one, Int.cast_natCast, nsmul_eq_mul]
-- 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 k : ℕ
hkn : k ≤ n
rw :
  n.choose k • smeval (descPochhammer ℤ (k + (n - k))) r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
⊢ n.choose k • smeval (descPochhammer ℤ (n - k + k)) r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
have rw₁ : n.choose k •
    (descPochhammer ℤ k * Polynomial.comp (descPochhammer ℤ (n - k)) (HSub.hSub (α := ℤ[X]) X (↑k : ℤ[X]))).smeval r =
  n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
Tactic: rw [add_comm, ← descPochhammer_mul, smeval_mul, smeval_comp, smeval_sub, smeval_X,
    ← C_eq_natCast, smeval_C, npow_one, npow_zero, zsmul_one, Int.cast_natCast, nsmul_eq_mul]
-- 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 k : ℕ
hkn : k ≤ n
rw :
  n.choose k • smeval (descPochhammer ℤ (k + (n - k))) r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₁ :
  n.choose k •
      (descPochhammer ℤ k * Polynomial.comp (descPochhammer ℤ (n - k)) (HSub.hSub (α := ℤ[X]) X (↑k : ℤ[X]))).smeval r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
⊢ n.choose k • smeval (descPochhammer ℤ (n - k + k)) r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
have rw₂ : n.choose k •
    (smeval (descPochhammer ℤ k) r *
      (Polynomial.comp (descPochhammer ℤ (n - k)) (HSub.hSub (α := ℤ[X]) X (↑k : ℤ[X]))).smeval r) =
  n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
Tactic: rw [add_comm, ← descPochhammer_mul, smeval_mul, smeval_comp, smeval_sub, smeval_X,
    ← C_eq_natCast, smeval_C, npow_one, npow_zero, zsmul_one, Int.cast_natCast, nsmul_eq_mul]
-- 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 k : ℕ
hkn : k ≤ n
rw :
  n.choose k • smeval (descPochhammer ℤ (k + (n - k))) r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₁ :
  n.choose k •
      (descPochhammer ℤ k * Polynomial.comp (descPochhammer ℤ (n - k)) (HSub.hSub (α := ℤ[X]) X (↑k : ℤ[X]))).smeval r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₂ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        (Polynomial.comp (descPochhammer ℤ (n - k)) (HSub.hSub (α := ℤ[X]) X (↑k : ℤ[X]))).smeval r) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
⊢ n.choose k • smeval (descPochhammer ℤ (n - k + k)) r =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
have rw₃ : n.choose k •
    (smeval (descPochhammer ℤ k) r *
      smeval (descPochhammer ℤ (n - k)) ((HSub.hSub (α := ℤ[X]) X (↑k : ℤ[X])).smeval r)) =
  n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
Tactic: rw [add_comm, ← descPochhammer_mul, smeval_mul, smeval_comp, smeval_sub, smeval_X,
    ← C_eq_natCast, smeval_C, npow_one, npow_zero, zsmul_one, Int.cast_natCast, nsmul_eq_mul]