no goals
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ eval (n + 1) (pochhammer ℕ 0) = Nat.ascFactorial n 0
rw [pochhammer_zero, eval_one, Nat.ascFactorial_zero]
S : Type u
inst✝ : Semiring S
n t : ℕ
⊢ Nat.ascFactorial n t * eval (n + 1) (X + ↑t) = Nat.ascFactorial n (t + 1)
S : Type u
inst✝ : Semiring S
n t : ℕ
⊢ eval (n + 1) (pochhammer ℕ (t + 1)) = Nat.ascFactorial n (t + 1)
rw [pochhammer_succ_right, eval_mul, pochhammer_nat_eq_ascFactorial n t]
S : Type u
inst✝ : Semiring S
n t : ℕ
⊢ Nat.ascFactorial n t * (n + 1 + t) = Nat.ascFactorial n (t + 1)
S : Type u
inst✝ : Semiring S
n t : ℕ
⊢ Nat.ascFactorial n t * eval (n + 1) (X + ↑t) = Nat.ascFactorial n (t + 1)
simp only [eval_add, eval_X, eval_nat_cast, Nat.cast_id]
no goals
S : Type u
inst✝ : Semiring S
n t : ℕ
⊢ Nat.ascFactorial n t * (n + 1 + t) = Nat.ascFactorial n (t + 1)
rw [Nat.ascFactorial_succ, add_right_comm, mul_comm]