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
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)))
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)))
⊢ 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)) (smeval (R := ℤ) X r - smeval (R := ℤ) (↑k : ℤ[X]) 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)))
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)))
rw₄ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) (smeval (R := ℤ) X r - smeval (R := ℤ) (↑k : ℤ[X]) 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)) (HPow.hPow (β := ℕ) r 1 - smeval (R := ℤ) (↑k : ℤ[X]) 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)))
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)))
rw₄ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) (smeval (R := ℤ) X r - smeval (R := ℤ) (↑k : ℤ[X]) r)) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₅ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) (HPow.hPow (β := ℕ) r 1 - smeval (R := ℤ) (↑k : ℤ[X]) 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)) (HPow.hPow (β := ℕ) r 1 - smeval (R := ℤ) ((C : (a : ℤ) → ℤ[X]) (↑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)))
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)))
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)))
rw₄ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) (smeval (R := ℤ) X r - smeval (R := ℤ) (↑k : ℤ[X]) r)) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₅ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) (HPow.hPow (β := ℕ) r 1 - smeval (R := ℤ) (↑k : ℤ[X]) r)) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₆ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k))
          (HPow.hPow (β := ℕ) r 1 - smeval (R := ℤ) ((C : (a : ℤ) → ℤ[X]) (↑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 •
    (smeval (descPochhammer ℤ k) r *
      smeval (descPochhammer ℤ (n - k))
        (HPow.hPow (β := ℕ) r 1 - HSMul.hSMul (α := ℤ) (↑k : ℤ) (HPow.hPow (β := ℕ) r 0))) =
  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)))
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)))
rw₄ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) (smeval (R := ℤ) X r - smeval (R := ℤ) (↑k : ℤ[X]) r)) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₅ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) (HPow.hPow (β := ℕ) r 1 - smeval (R := ℤ) (↑k : ℤ[X]) r)) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₆ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k))
          (HPow.hPow (β := ℕ) r 1 - smeval (R := ℤ) ((C : (a : ℤ) → ℤ[X]) (↑k : ℤ)) r)) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₇ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k))
          (HPow.hPow (β := ℕ) r 1 - HSMul.hSMul (α := ℤ) (↑k : ℤ) (HPow.hPow (β := ℕ) r 0))) =
    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)) (r - HSMul.hSMul (α := ℤ) (↑k : ℤ) (HPow.hPow (β := ℕ) r 0))) =
  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)))
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)))
rw₄ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) (smeval (R := ℤ) X r - smeval (R := ℤ) (↑k : ℤ[X]) r)) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₅ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) (HPow.hPow (β := ℕ) r 1 - smeval (R := ℤ) (↑k : ℤ[X]) r)) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₆ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k))
          (HPow.hPow (β := ℕ) r 1 - smeval (R := ℤ) ((C : (a : ℤ) → ℤ[X]) (↑k : ℤ)) r)) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₇ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k))
          (HPow.hPow (β := ℕ) r 1 - HSMul.hSMul (α := ℤ) (↑k : ℤ) (HPow.hPow (β := ℕ) r 0))) =
    n.choose k • (smeval (descPochhammer ℤ k) r * smeval (descPochhammer ℤ (n - k)) (r - (↑k : R)))
rw₈ :
  n.choose k •
      (smeval (descPochhammer ℤ k) r *
        smeval (descPochhammer ℤ (n - k)) (r - HSMul.hSMul (α := ℤ) (↑k : ℤ) (HPow.hPow (β := ℕ) r 0))) =
    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)) (r - HSMul.hSMul (α := ℤ) (β := R) (↑k : ℤ) 1)) =
  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 : ℕ
⊢ (n + k).choose k • choose (r + (↑k : R)) (n + k) = choose (r + (↑k : R)) k * choose r n
have rw : choose (r + (↑k : R)) k * choose (r + (↑k : R) - (↑k : R)) (n + k - 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]
-- 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 : ℕ
rw : choose (r + (↑k : R)) k * choose (r + (↑k : R) - (↑k : R)) (n + k - k) = 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
have rw₁ : choose (r + (↑k : R)) k * choose (r + (↑k : R) - (↑k : R)) n = 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]
-- 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 : ℕ
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
⊢ (n + k).choose k • choose (r + (↑k : R)) (n + k) = choose (r + (↑k : R)) k * choose r n
have rw₂ : choose (r + (↑k : R)) k * choose r n = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Field R
inst_1 : CharZero R
a : R
n : ℕ
⊢ choose a n = HSMul.hSMul (α := R) (↑n.factorial : R)⁻¹ (smeval (descPochhammer ℤ n) a)
have ha : Ne.{u_1 + 1} (α := R) (↑n.factorial : R) 0
Tactic: rw [Ring.descPochhammer_eq_factorial_smul_choose, ← Nat.cast_smul_eq_nsmul R, inv_smul_smul₀]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  smeval (descPochhammer ℤ k) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
⊢ smeval (descPochhammer ℤ (k + 1)) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ (k + 1),
      (↑((k + 1).choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
have succ : Eq.{u_1 + 1} (α := R)
  (∑ i ∈ @antidiagonal _ Nat.instAddMonoid _ k,
    (r + s - HSMul.hSMul (β := R) k 1) *
      ((↑(k.choose i.1) : R) * (smeval (descPochhammer ℤ i.1) r * smeval (descPochhammer ℤ i.2) s)))
  (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ k,
    ((↑(k.choose x.1) : R) * (smeval (descPochhammer ℤ x.1) r * smeval (descPochhammer ℤ (x.2 + 1)) s) +
      (↑(k.choose x.2) : R) * (smeval (descPochhammer ℤ (x.1 + 1)) r * smeval (descPochhammer ℤ x.2) s)))
Tactic: rw [descPochhammer_succ_right, mul_comm, smeval_mul, sum_antidiagonal_choose_succ_mul
      fun i j => ((descPochhammer ℤ i).smeval r * (descPochhammer ℤ j).smeval s),
      ← sum_add_distrib, smeval_sub, smeval_X, smeval_natCast, pow_zero, pow_one, ih, mul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  smeval (descPochhammer ℤ k) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
⊢ Eq.{u_1 + 1} (α := R)
    (∑ i ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (r + s - HSMul.hSMul (β := R) k 1) *
        ((↑(k.choose i.1) : R) * (smeval (descPochhammer ℤ i.1) r * smeval (descPochhammer ℤ i.2) s)))
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      ((↑(k.choose x.1) : R) * (smeval (descPochhammer ℤ x.1) r * smeval (descPochhammer ℤ (x.2 + 1)) s) +
        (↑(k.choose x.2) : R) * (smeval (descPochhammer ℤ (x.1 + 1)) r * smeval (descPochhammer ℤ x.2) s)))
have succ : ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ k,
  (r + s - HSMul.hSMul (β := R) k 1) *
      ((↑(k.choose x.1) : R) * (smeval (descPochhammer ℤ x.1) r * smeval (descPochhammer ℤ x.2) s)) =
    (↑(k.choose x.1) : R) * (smeval (descPochhammer ℤ x.1) r * smeval (descPochhammer ℤ (x.2 + 1)) s) +
      (↑(k.choose x.2) : R) * (smeval (descPochhammer ℤ (x.1 + 1)) r * smeval (descPochhammer ℤ x.2) s)
Tactic: refine sum_congr rfl ?_
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (hypothesis)
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  smeval (descPochhammer ℤ k) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
ij : ℕ × ℕ
hij : ij ∈ @antidiagonal _ Nat.instAddMonoid _ k
⊢ (r + s - HSMul.hSMul (β := R) k 1) *
      ((↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)) =
    (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ (ij.2 + 1)) s) +
      (↑(k.choose ij.2) : R) * (smeval (descPochhammer ℤ (ij.1 + 1)) r * smeval (descPochhammer ℤ ij.2) s)
have hdx : smeval (descPochhammer ℤ ij.1) r * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s =
  (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s * smeval (descPochhammer ℤ ij.1) r
Tactic: have hdx : (descPochhammer ℤ ij.1).smeval r * (X - (ij.2 : ℤ[X])).smeval s =
        (X - (ij.2 : ℤ[X])).smeval s * (descPochhammer ℤ ij.1).smeval r := by
      refine (commute_iff_eq ((descPochhammer ℤ ij.1).smeval r)
        ((X - (ij.2 : ℤ[X])).smeval s)).mp ?_
      exact smeval_commute ℤ (descPochhammer ℤ ij.1) (X - (ij.2 : ℤ[X])) h
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  smeval (descPochhammer ℤ k) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
ij : ℕ × ℕ
hij : ij ∈ @antidiagonal _ Nat.instAddMonoid _ k
hdx :
  smeval (descPochhammer ℤ ij.1) r * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s =
    (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s * smeval (descPochhammer ℤ ij.1) r
⊢ (r + s - HSMul.hSMul (β := R) k 1) *
      ((↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)) =
    (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ (ij.2 + 1)) s) +
      (↑(k.choose ij.2) : R) * (smeval (descPochhammer ℤ (ij.1 + 1)) r * smeval (descPochhammer ℤ ij.2) s)
have succ : (r + s - HSMul.hSMul (β := R) k 1) *
    ((↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)) =
  (↑(k.choose ij.1) : R) *
      ((HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s * smeval (descPochhammer ℤ ij.1) r *
        smeval (descPochhammer ℤ ij.2) s) +
    (↑(k.choose ij.2) : R) *
      ((HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r * smeval (descPochhammer ℤ ij.1) r *
        smeval (descPochhammer ℤ ij.2) s)
Tactic: rw [descPochhammer_succ_right, mul_comm, smeval_mul, descPochhammer_succ_right, mul_comm,
      smeval_mul, ← mul_assoc ((descPochhammer ℤ ij.1).smeval r), hdx]
-- Lean 4 proof step from Mathlib.RingTheory.Binomial (goal)
Goal:
R : Type u_1
inst : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  smeval (descPochhammer ℤ k) (r + s) =
    ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
ij : ℕ × ℕ
hij : ij ∈ @antidiagonal _ Nat.instAddMonoid _ k
hdx :
  smeval (descPochhammer ℤ ij.1) r * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s =
    (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s * smeval (descPochhammer ℤ ij.1) r
⊢ (r + s - HSMul.hSMul (β := R) k 1) *
      ((↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)) =
    (↑(k.choose ij.1) : R) *
        ((HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s * smeval (descPochhammer ℤ ij.1) r *
          smeval (descPochhammer ℤ ij.2) s) +
      (↑(k.choose ij.2) : R) *
        ((HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r * smeval (descPochhammer ℤ ij.1) r *
          smeval (descPochhammer ℤ ij.2) s)
have succ : (r + s - HSMul.hSMul (β := R) k 1) * (↑(k.choose ij.1) : R) *
    (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s) =
  (↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s *
      (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s) +
    (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r *
      (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s)
Tactic: simp only [mul_assoc _ ((descPochhammer ℤ ij.1).smeval r) _,
      ← mul_assoc _ _ (((descPochhammer ℤ ij.1).smeval r) * _)]