no goals
S✝ : Type ?u.29571
inst✝¹ : Semiring S✝
r✝ n✝ : ℕ
S : Type u_1
inst✝ : Semiring S
r n : ℕ
⊢ ↑r ! * eval (↑r + 1) (pochhammer S n) = ↑(r + n)!
rw_mod_cast [pochhammer_nat_eq_ascFactorial, Nat.factorial_mul_ascFactorial]