no goals
S✝ : Type u
inst✝¹ : Semiring S✝
S : Type u_1
inst✝ : Semiring S
n : ℕ
k : S
⊢ eval k (pochhammer S (n + 1)) = eval k (pochhammer S n) * (k + ↑n)
rw [pochhammer_succ_right, mul_add, eval_add, eval_mul_X, ← Nat.cast_comm, ← C_eq_nat_cast,
  eval_C_mul, Nat.cast_comm, ← mul_add]