-- Module: Mathlib.RingTheory.Binomial
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Pow R ℕ
inst_2 : NatPowAssoc R
r : R
k : ℕ
ih : smeval (ascPochhammer ℕ k) (-r) = Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r
h : (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) = -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r
succ :
  Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * -(HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₁ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₂ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    (HAdd.hAdd (α := ℤ) (↑k : ℤ) (↑1 : ℤ)).negOnePow •
      (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₃ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    (HAdd.hAdd (α := ℤ) (↑k : ℤ) 1).negOnePow •
      (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₄ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₅ :
  -(Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r) * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -(Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r))
succ₆ :
  -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) • smeval (descPochhammer ℤ k) r) *
      (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -(Int.negOnePow (↑k : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r))
succ₇ :
  -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) • smeval (descPochhammer ℤ k) r) *
      (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) •
        (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r))
succ₈ :
  -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) • smeval (descPochhammer ℤ k) r) *
      (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r =
    -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) • smeval (descPochhammer ℤ k) r *
        (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
succ₉ succ₁₀ :
  -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) • smeval (descPochhammer ℤ k) r *
        (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r) =
    -((↑(Int.negOnePow (↑k : ℤ)) : ℤ) • smeval (descPochhammer ℤ k) r *
        (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)
⊢ Int.negOnePow (↑k : ℤ) • smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℕ[X]) X (↑k : ℕ[X])).smeval (-r) =
    Int.negOnePow (↑(k + 1) : ℤ) • (smeval (descPochhammer ℤ k) r * (HAdd.hAdd (α := ℤ[X]) X (-(↑k : ℤ[X]))).smeval r)

Tactic:
rw [h, ← neg_mul_comm, Int.natCast_add, Int.natCast_one, Int.negOnePow_succ, Units.neg_smul,
      Units.smul_def, Units.smul_def, ← smul_mul_assoc, neg_mul]

Premises used: Int.natCast_add, smul_mul_assoc, Int.natCast_one, Units.neg_smul, Units.smul_def, neg_mul_comm, neg_mul, Int.negOnePow_succ