-- Mathlib/RingTheory/Binomial.lean
theorem ascPochhammer_smeval_neg_eq_descPochhammer (r : R) (k : ℕ) :
    (ascPochhammer ℕ k).smeval (-r) = Int.negOnePow k • (descPochhammer ℤ k).smeval r

Proof state:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
ih : (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r
⊢ (↑k).negOnePow • (descPochhammer ℤ k).smeval r * (X + ↑k).smeval (-r) =
    (↑(k + 1)).negOnePow • ((descPochhammer ℤ k).smeval r * (X + -↑k).smeval r)

Tactic:
have h : (X + (k : ℕ[X])).smeval (-r) = - (X + (-k : ℤ[X])).smeval r := by
  simp [smeval_natCast, add_comm]

Result:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
ih : (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r
h : (X + ↑k).smeval (-r) = -(X + -↑k).smeval r
⊢ (↑k).negOnePow • (descPochhammer ℤ k).smeval r * (X + ↑k).smeval (-r) =
    (↑(k + 1)).negOnePow • ((descPochhammer ℤ k).smeval r * (X + -↑k).smeval r)

Proof state:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
ih : (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r
⊢ (ascPochhammer ℕ (k + 1)).smeval (-r) = (↑(k + 1)).negOnePow • (descPochhammer ℤ (k + 1)).smeval r

Tactic:
simp only [ascPochhammer_succ_right, smeval_mul, ih, descPochhammer_succ_right, sub_eq_add_neg]

Result:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
ih : (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r
⊢ (↑k).negOnePow • (descPochhammer ℤ k).smeval r * (X + ↑k).smeval (-r) =
    (↑(k + 1)).negOnePow • ((descPochhammer ℤ k).smeval r * (X + -↑k).smeval r)

Proof state:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
ih : (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r
⊢ (X + ↑k).smeval (-r) = -(X + -↑k).smeval r

Tactic:
simp [smeval_natCast, add_comm]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
⊢ (ascPochhammer ℕ 0).smeval (-r) = (↑0).negOnePow • (descPochhammer ℤ 0).smeval r

Tactic:
simp

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
ih : (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r
h : (X + ↑k).smeval (-r) = -(X + -↑k).smeval r
⊢ (↑k).negOnePow • (descPochhammer ℤ k).smeval r * (X + ↑k).smeval (-r) =
    (↑(k + 1)).negOnePow • ((descPochhammer ℤ k).smeval r * (X + -↑k).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]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (ascPochhammer ℕ k).smeval (-r) = (↑k).negOnePow • (descPochhammer ℤ k).smeval r

Tactic:
induction k with
| zero => simp
| succ k ih =>
  simp only [ascPochhammer_succ_right, smeval_mul, ih, descPochhammer_succ_right, sub_eq_add_neg]
  have h : (X + (k : ℕ[X])).smeval (-r) = - (X + (-k : ℤ[X])).smeval r := by
    simp [smeval_natCast, add_comm]
  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]

Result:
no goals