case pos
S : Type ?u.31829
inst✝ : Semiring S
r✝ n r : ℕ
h : r = 0
⊢ 0 * eval (0 + 1) (pochhammer ℕ r) = (0 + r) * eval 0 (pochhammer ℕ r)

case neg
S : Type ?u.31829
inst✝ : Semiring S
r✝ n r : ℕ
h : ¬r = 0
⊢ 0 * eval (0 + 1) (pochhammer ℕ r) = (0 + r) * eval 0 (pochhammer ℕ r)
S : Type ?u.31829
inst✝ : Semiring S
r✝ n r : ℕ
⊢ 0 * eval (0 + 1) (pochhammer ℕ r) = (0 + r) * eval 0 (pochhammer ℕ r)
by_cases h : r = 0
no goals
case pos
S : Type ?u.31829
inst✝ : Semiring S
r✝ n r : ℕ
h : r = 0
⊢ 0 * eval (0 + 1) (pochhammer ℕ r) = (0 + r) * eval 0 (pochhammer ℕ r)
simp only [h, zero_mul, zero_add]
no goals
case neg
S : Type ?u.31829
inst✝ : Semiring S
r✝ n r : ℕ
h : ¬r = 0
⊢ 0 * eval (0 + 1) (pochhammer ℕ r) = (0 + r) * eval 0 (pochhammer ℕ r)
simp only [pochhammer_eval_zero, zero_mul, if_neg h, mul_zero]
no goals
S : Type ?u.31829
inst✝ : Semiring S
r✝ n r k : ℕ
⊢ (k + 1) * eval (k + 1 + 1) (pochhammer ℕ r) = (k + 1 + r) * eval (k + 1) (pochhammer ℕ r)
simp only [pochhammer_nat_eq_ascFactorial, Nat.succ_ascFactorial, add_right_comm]