case zero
S : Type u
inst✝ : Semiring S
a : ℕ
⊢ eval a (pochhammer ℕ Nat.zero) = Nat.descFactorial (a + Nat.zero - 1) Nat.zero

case succ
S : Type u
inst✝ : Semiring S
a b : ℕ
⊢ eval a (pochhammer ℕ (Nat.succ b)) = Nat.descFactorial (a + Nat.succ b - 1) (Nat.succ b)
S : Type u
inst✝ : Semiring S
a b : ℕ
⊢ eval a (pochhammer ℕ b) = Nat.descFactorial (a + b - 1) b
cases' b with b
case succ
S : Type u
inst✝ : Semiring S
a b : ℕ
⊢ eval a (pochhammer ℕ (Nat.succ b)) = Nat.descFactorial (a + b) (Nat.succ b)
case succ
S : Type u
inst✝ : Semiring S
a b : ℕ
⊢ eval a (pochhammer ℕ (Nat.succ b)) = Nat.descFactorial (a + Nat.succ b - 1) (Nat.succ b)
rw [Nat.add_succ, Nat.succ_sub_succ, tsub_zero]
case succ.zero
S : Type u
inst✝ : Semiring S
b : ℕ
⊢ eval Nat.zero (pochhammer ℕ (Nat.succ b)) = Nat.descFactorial (Nat.zero + b) (Nat.succ b)

case succ.succ
S : Type u
inst✝ : Semiring S
b n✝ : ℕ
⊢ eval (Nat.succ n✝) (pochhammer ℕ (Nat.succ b)) = Nat.descFactorial (Nat.succ n✝ + b) (Nat.succ b)
case succ
S : Type u
inst✝ : Semiring S
a b : ℕ
⊢ eval a (pochhammer ℕ (Nat.succ b)) = Nat.descFactorial (a + b) (Nat.succ b)
cases a
no goals
case zero
S : Type u
inst✝ : Semiring S
a : ℕ
⊢ eval a (pochhammer ℕ Nat.zero) = Nat.descFactorial (a + Nat.zero - 1) Nat.zero
rw [Nat.descFactorial_zero, pochhammer_zero, Polynomial.eval_one]
no goals
case succ.zero
S : Type u
inst✝ : Semiring S
b : ℕ
⊢ eval Nat.zero (pochhammer ℕ (Nat.succ b)) = Nat.descFactorial (Nat.zero + b) (Nat.succ b)
simp only [Nat.zero_eq, ne_eq, Nat.succ_ne_zero, not_false_iff, pochhammer_ne_zero_eval_zero,
zero_add, Nat.descFactorial_succ, le_refl, tsub_eq_zero_of_le, zero_mul]
no goals
case succ.succ
S : Type u
inst✝ : Semiring S
b n✝ : ℕ
⊢ eval (Nat.succ n✝) (pochhammer ℕ (Nat.succ b)) = Nat.descFactorial (Nat.succ n✝ + b) (Nat.succ b)
rw [Nat.succ_add, ← Nat.add_succ, Nat.add_descFactorial_eq_ascFactorial,
  pochhammer_nat_eq_ascFactorial]