awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Binomial
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)
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)))
⊢ 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)

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]

Premises used: Finset.mul_sum, Finset.sum_antidiagonal_choose_succ_mul, HMul.hMul, Finset.sum_add_distrib, descPochhammer, descPochhammer_succ_right, Polynomial.smeval_sub, Polynomial.smeval_natCast, Polynomial.smeval_mul, Polynomial.smeval_X, Int, pow_zero, pow_one, mul_comm, Polynomial.smeval
-- Module: Mathlib.RingTheory.Binomial
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)))

Tactic:
sum_congr rfl ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Binomial
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)
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)
⊢ 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:
refine sum_congr rfl ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Binomial
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
⊢ 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:
(commute_iff_eq ((descPochhammer ℤ ij.1).smeval r)
        ((X - (ij.2 : ℤ[X])).smeval s)).mp ?_

Premises used: descPochhammer, commute_iff_eq, Int, Prod.fst, Iff.mp, Polynomial.smeval
-- Module: Mathlib.RingTheory.Binomial
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
⊢ Commute (smeval (descPochhammer ℤ ij.1) r) ((HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s)

Tactic:
smeval_commute ℤ (descPochhammer ℤ ij.1) (X - (ij.2 : ℤ[X])) h

Premises used: Polynomial.smeval_commute, descPochhammer, HSub.hSub, Int, Nat.cast, Prod.fst, Polynomial.X, Prod.snd
-- Module: Mathlib.RingTheory.Binomial
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
⊢ Commute (smeval (descPochhammer ℤ ij.1) r) ((HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s)

Tactic:
exact smeval_commute ℤ (descPochhammer ℤ ij.1) (X - (ij.2 : ℤ[X])) h

Premises used: Polynomial.smeval_commute, descPochhammer, HSub.hSub, Int, Nat.cast, Prod.fst, Polynomial.X, Prod.snd
-- Module: Mathlib.RingTheory.Binomial
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
⊢ 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
-- Module: Mathlib.RingTheory.Binomial
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
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)
⊢ (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)

Tactic:
rw [descPochhammer_succ_right, mul_comm, smeval_mul, descPochhammer_succ_right, mul_comm,
      smeval_mul, ← mul_assoc ((descPochhammer ℤ ij.1).smeval r), hdx]

Premises used: descPochhammer, mul_assoc, descPochhammer_succ_right, Polynomial.smeval_mul, Int, Prod.fst, mul_comm, Polynomial.smeval
-- Module: Mathlib.RingTheory.Binomial
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
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)
⊢ (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) * _)]

Premises used: HMul.hMul, descPochhammer, mul_assoc, Int, Prod.fst, Polynomial.smeval
-- Module: Mathlib.RingTheory.Binomial
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
simp :
  (r + s - HSMul.hSMul (β := R) k 1) * (↑(k.choose ij.1) : R) =
    (↑(k.choose ij.1) : R) * (s - HSMul.hSMul (β := R) ij.2 1) +
      (↑(k.choose ij.2) : R) * (r - HSMul.hSMul (β := R) ij.1 1)
⊢ (r + s - HSMul.hSMul (β := R) k 1) * (↑(k.choose ij.1) : R) =
    (↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s +
      (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r

Tactic:
simp only [smeval_sub, smeval_X, pow_one, smeval_natCast, pow_zero]

Premises used: Polynomial.smeval_sub, Polynomial.smeval_natCast, Polynomial.smeval_X, pow_zero, pow_one
-- Module: Mathlib.RingTheory.Binomial
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
rw :
  (r + s - (HSMul.hSMul (β := R) ij.1 1 + HSMul.hSMul (β := R) ij.2 1)) * (↑((ij.1 + ij.2).choose ij.1) : R) =
    (s - HSMul.hSMul (β := R) ij.2 1 + (r - HSMul.hSMul (β := R) ij.1 1)) * (↑((ij.1 + ij.2).choose ij.1) : R)
⊢ (r + s - HSMul.hSMul (β := R) k 1) * (↑(k.choose ij.1) : R) =
    (↑(k.choose ij.1) : R) * (s - HSMul.hSMul (β := R) ij.2 1) +
      (↑(k.choose ij.2) : R) * (r - HSMul.hSMul (β := R) ij.1 1)

Tactic:
rw [← Nat.choose_symm_of_eq_add (List.Nat.mem_antidiagonal.mp hij).symm,
        (List.Nat.mem_antidiagonal.mp hij).symm, ← mul_add, Nat.cast_comm, add_smul]

Premises used: Nat.cast_comm, add_smul, Iff.mp, List.Nat.mem_antidiagonal, mul_add, Eq.symm, Nat.choose_symm_of_eq_add
-- Module: Mathlib.RingTheory.Binomial
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) ij.1 1 + HSMul.hSMul (β := R) ij.2 1)) * (↑((ij.1 + ij.2).choose ij.1) : R) =
    (s - HSMul.hSMul (β := R) ij.2 1 + (r - HSMul.hSMul (β := R) ij.1 1)) * (↑((ij.1 + ij.2).choose ij.1) : R)

Tactic:
abel_nf
-- Module: Mathlib.RingTheory.Binomial
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) =
    (↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s +
      (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r

Tactic:
have hl : (r + s - k • 1) * (k.choose ij.1) = (k.choose ij.1) * (X - (ij.2 : ℤ[X])).smeval s +
        ↑(k.choose ij.2) * (X - (ij.1 : ℤ[X])).smeval r := by
      simp only [smeval_sub, smeval_X, pow_one, smeval_natCast, pow_zero]
      rw [← Nat.choose_symm_of_eq_add (List.Nat.mem_antidiagonal.mp hij).symm,
        (List.Nat.mem_antidiagonal.mp hij).symm, ← mul_add, Nat.cast_comm, add_smul]
      abel_nf
-- Module: Mathlib.RingTheory.Binomial
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
hl :
  (r + s - HSMul.hSMul (β := R) k 1) * (↑(k.choose ij.1) : R) =
    (↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval s +
      (↑(k.choose ij.2) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.1 : ℤ[X])).smeval r
succ :
  ((↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval 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) =
    (↑(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)
succ₁ succ₂ :
  ((↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval 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) =
    ((↑(k.choose ij.1) : R) * (HSub.hSub (α := ℤ[X]) X (↑ij.2 : ℤ[X])).smeval 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)
⊢ (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 [hl, ← add_mul]

Premises used: add_mul
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : Ring R
r s : R
k : ℕ
h : Commute r s
zero :
  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)
succ :
  ∀ (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)
⊢ 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)

Tactic:
induction k with
  | zero => simp
  | succ k ih =>
    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]
    refine sum_congr rfl ?_
    intro ij hij -- try to move `descPochhammer`s to right, gather multipliers.
    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
    rw [descPochhammer_succ_right, mul_comm, smeval_mul, descPochhammer_succ_right, mul_comm,
      smeval_mul, ← mul_assoc ((descPochhammer ℤ ij.1).smeval r), hdx]
    simp only [mul_assoc _ ((descPochhammer ℤ ij.1).smeval r) _,
      ← mul_assoc _ _ (((descPochhammer ℤ ij.1).smeval r) * _)]
    have hl : (r + s - k • 1) * (k.choose ij.1) = (k.choose ij.1) * (X - (ij.2 : ℤ[X])).smeval s +
        ↑(k.choose ij.2) * (X - (ij.1 : ℤ[X])).smeval r := by
      simp only [smeval_sub, smeval_X, pow_one, smeval_natCast, pow_zero]
      rw [← Nat.choose_symm_of_eq_add (List.Nat.mem_antidiagonal.mp hij).symm,
        (List.Nat.mem_antidiagonal.mp hij).symm, ← mul_add, Nat.cast_comm, add_smul]
      abel_nf
    rw [hl, ← add_mul]

Premises used: add_mul, Finset.mul_sum, Finset.sum_antidiagonal_choose_succ_mul, HMul.hMul, Finset.sum_add_distrib, descPochhammer, descPochhammer_succ_right, Polynomial.smeval_sub, Polynomial.smeval_natCast, Polynomial.smeval_mul, Polynomial.smeval_X, Int, pow_zero, pow_one, mul_comm, Finset.sum_congr, Polynomial.smeval, rfl
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : Ring R
inst_1 : BinomialRing R
r s : R
k : ℕ
h : Commute r s
rw :
  Eq.{u_1 + 1} (α := R)
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s))
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ k, k.factorial • (choose r x.1 * choose s x.2))
⊢ choose (r + s) k = ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ 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]

Premises used: Ring.descPochhammer_smeval_add, nsmul_right_inj, Nat.factorial_ne_zero, Finset.smul_sum, Ring.descPochhammer_eq_factorial_smul_choose
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : Ring R
inst_1 : BinomialRing R
r s : R
k : ℕ
h : Commute r s
⊢ Eq.{u_1 + 1} (α := R)
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s))
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ k, k.factorial • (choose r x.1 * choose s x.2))

Tactic:
sum_congr rfl ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : Ring R
inst_1 : BinomialRing R
r s : R
k : ℕ
h : Commute r s
refine :
  ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ k,
    (↑(k.choose x.1) : R) * (smeval (descPochhammer ℤ x.1) r * smeval (descPochhammer ℤ x.2) s) =
      k.factorial • (choose r x.1 * choose s x.2)
⊢ Eq.{u_1 + 1} (α := R)
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ k,
      (↑(k.choose ij.1) : R) * (smeval (descPochhammer ℤ ij.1) r * smeval (descPochhammer ℤ ij.2) s))
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ k, k.factorial • (choose r x.1 * choose s x.2))

Tactic:
refine sum_congr rfl ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : Ring R
inst_1 : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ k
rw :
  (↑(k.choose x.1) : R) * (smeval (descPochhammer ℤ x.1) r * smeval (descPochhammer ℤ x.2) s) =
    HMul.hMul (α := R) (↑(k.choose x.1) : R) (↑x.1.factorial : R) * (choose r x.1 * x.2.factorial • choose s x.2)
⊢ (↑(k.choose x.1) : R) * (smeval (descPochhammer ℤ x.1) r * smeval (descPochhammer ℤ x.2) 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]

Premises used: mul_assoc, Nat.choose_mul_factorial_mul_factorial, Nat.cast, Prod.fst, Nat.cast_mul, Nat.factorial, Finset.antidiagonal.fst_le, Iff.mp, List.Nat.mem_antidiagonal, tsub_eq_of_eq_add_rev, nsmul_eq_mul, Eq.symm, Prod.snd, Nat.cast_commute
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : Ring R
inst_1 : BinomialRing R
r s : R
k : ℕ
h : Commute r s
x : ℕ × ℕ
hx : x ∈ @antidiagonal _ Nat.instAddMonoid _ k
⊢ (↑(k.choose x.1) : R) * (smeval (descPochhammer ℤ x.1) r * smeval (descPochhammer ℤ x.2) s) =
    HMul.hMul (α := R) (↑(k.choose x.1) : R) (↑x.1.factorial : R) * (choose r x.1 * x.2.factorial • choose s x.2)

Tactic:
simp [mul_assoc, descPochhammer_eq_factorial_smul_choose]

Premises used: mul_assoc, Ring.descPochhammer_eq_factorial_smul_choose
-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_2
S : Type u_3
F : Type u_4
inst : Ring R
inst_1 : Ring S
inst_2 : BinomialRing R
inst_3 : BinomialRing S
inst_4 : FunLike F R S
inst_5 : RingHomClass F R S
f : F
a : R
n : ℕ
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) (choose a n) : S) (choose ((f : (a : R) → S) a) n : S)

Tactic:
simpa using Ring.map_multichoose f (a - n + 1) n

Premises used: Ring.map_multichoose, HSub.hSub, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
⊢ ¬IsUnit p

Tactic:
simpa only [Associates.isUnit_iff_eq_one] using hp.1

Premises used: And.left, Associates.isUnit_iff_eq_one
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = a * b
ha : a = p
⊢ p = p * b

Tactic:
rw [ha] at h
-- Module: Mathlib.RingTheory.ChainOfDivisors
Goal:
M : Type u_1
inst : CommMonoidWithZero M
inst_1 : IsCancelMulZero M
p : Associates M
h₁ : p ≠ 0
hp : IsAtom p
a b : Associates M
h : p = a * b
ha : a = p
h₂ : p = p * b
⊢ a = p

Tactic:
rw [ha] at h