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

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
⊢ ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s) =
    ∑ x ∈ antidiagonal k, k.factorial • (choose r x.1 * choose s x.2)

Tactic:
refine sum_congr rfl ?_

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
⊢ ∀ x ∈ antidiagonal k,
    ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
      k.factorial • (choose r x.1 * choose s x.2)

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
⊢ ∀ x ∈ antidiagonal k,
    ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
      k.factorial • (choose r x.1 * choose s x.2)

Tactic:
intro x hx

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    k.factorial • (choose r x.1 * choose s x.2)

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    k.factorial • (choose r x.1 * choose s x.2)

Tactic:
rw [← Nat.choose_mul_factorial_mul_factorial (antidiagonal.fst_le hx),
  tsub_eq_of_eq_add_rev (List.Nat.mem_antidiagonal.mp hx).symm, mul_assoc, nsmul_eq_mul,
  Nat.cast_mul, Nat.cast_mul, ← mul_assoc _ (x.1.factorial : R), mul_assoc _ (x.2.factorial : R),
  ← mul_assoc (x.2.factorial : R), Nat.cast_commute x.2.factorial,
  mul_assoc _ (x.2.factorial : R), ← nsmul_eq_mul x.2.factorial]

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    ↑(k.choose x.1) * ↑x.1.factorial * (choose r x.1 * x.2.factorial • choose s x.2)

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
⊢ choose (r + s) k = ∑ ij ∈ antidiagonal k, choose r ij.1 * choose s ij.2

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero k),
  ← descPochhammer_eq_factorial_smul_choose, smul_sum, descPochhammer_smeval_add _ h]

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
⊢ ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s) =
    ∑ x ∈ antidiagonal k, k.factorial • (choose r x.1 * choose s x.2)

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ ↑(k.choose x.1) * ((descPochhammer ℤ x.1).smeval r * (descPochhammer ℤ x.2).smeval s) =
    ↑(k.choose x.1) * ↑x.1.factorial * (choose r x.1 * x.2.factorial • choose s x.2)

Tactic:
simp [mul_assoc, descPochhammer_eq_factorial_smul_choose]

Result:
no goals