-- Mathlib/RingTheory/Binomial.lean
theorem descPochhammer_smeval_add [Ring R] {r s : R} (k : ℕ) (h: Commute r s) :
    (descPochhammer ℤ k).smeval (r + s) = ∑ ij ∈ antidiagonal k,
    Nat.choose k ij.1 * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)

Proof state:
case succ
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
ij : ℕ × ℕ
hij : ij ∈ antidiagonal k
⊢ (r + s - k • 1) * (↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)) =
    ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ (ij.2 + 1)).smeval s) +
      ↑(k.choose ij.2) * ((descPochhammer ℤ (ij.1 + 1)).smeval r * (descPochhammer ℤ ij.2).smeval s)

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

Result:
case succ
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
ij : ℕ × ℕ
hij : ij ∈ antidiagonal k
hdx : (descPochhammer ℤ ij.1).smeval r * (X - ↑ij.2).smeval s = (X - ↑ij.2).smeval s * (descPochhammer ℤ ij.1).smeval r
⊢ (r + s - k • 1) * (↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)) =
    ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ (ij.2 + 1)).smeval s) +
      ↑(k.choose ij.2) * ((descPochhammer ℤ (ij.1 + 1)).smeval r * (descPochhammer ℤ ij.2).smeval s)

Proof state:
case succ
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
⊢ (descPochhammer ℤ (k + 1)).smeval (r + s) =
    ∑ ij ∈ antidiagonal (k + 1),
      ↑((k + 1).choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval 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]

Result:
case succ
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
⊢ ∑ i ∈ antidiagonal k,
      (r + s - k • 1) * (↑(k.choose i.1) * ((descPochhammer ℤ i.1).smeval r * (descPochhammer ℤ i.2).smeval s)) =
    ∑ x ∈ antidiagonal k,
      (↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ (x.2 + 1)).smeval s) +
        ↑(k.choose x.2) * ((descPochhammer ℤ (x.1 + 1)).smeval r * (descPochhammer ℤ x.2).smeval s))

Proof state:
case succ
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
ij : ℕ × ℕ
hij : ij ∈ antidiagonal k
hdx : (descPochhammer ℤ ij.1).smeval r * (X - ↑ij.2).smeval s = (X - ↑ij.2).smeval s * (descPochhammer ℤ ij.1).smeval r
⊢ (r + s - k • 1) * (↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)) =
    ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ (ij.2 + 1)).smeval s) +
      ↑(k.choose ij.2) * ((descPochhammer ℤ (ij.1 + 1)).smeval r * (descPochhammer ℤ ij.2).smeval 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]

Result:
case succ
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
ij : ℕ × ℕ
hij : ij ∈ antidiagonal k
hdx : (descPochhammer ℤ ij.1).smeval r * (X - ↑ij.2).smeval s = (X - ↑ij.2).smeval s * (descPochhammer ℤ ij.1).smeval r
⊢ (r + s - k • 1) * (↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)) =
    ↑(k.choose ij.1) * ((X - ↑ij.2).smeval s * (descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s) +
      ↑(k.choose ij.2) * ((X - ↑ij.1).smeval r * (descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)