[GOAL]
S : Type u
inst✝ : Semiring S
⊢ pochhammer S 1 = X
[PROOFSTEP]
simp [pochhammer]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ pochhammer S (n + 1) = X * comp (pochhammer S n) (X + 1)
[PROOFSTEP]
rw [pochhammer]
[GOAL]
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
⊢ map f (pochhammer S n) = pochhammer T n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
⊢ map f (pochhammer S Nat.zero) = pochhammer T Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
ih : map f (pochhammer S n) = pochhammer T n
⊢ map f (pochhammer S (Nat.succ n)) = pochhammer T (Nat.succ n)
[PROOFSTEP]
simp [ih, pochhammer_succ_left, map_comp]
[GOAL]
S : Type u
inst✝ : Semiring S
n k : ℕ
⊢ ↑(eval k (pochhammer ℕ n)) = eval (↑k) (pochhammer S n)
[PROOFSTEP]
rw [← pochhammer_map (algebraMap ℕ S), eval_map, ← eq_natCast (algebraMap ℕ S), eval₂_at_nat_cast, Nat.cast_id,
  eq_natCast]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ eval 0 (pochhammer S n) = if n = 0 then 1 else 0
[PROOFSTEP]
cases n
[GOAL]
case zero
S : Type u
inst✝ : Semiring S
⊢ eval 0 (pochhammer S Nat.zero) = if Nat.zero = 0 then 1 else 0
[PROOFSTEP]
simp
[GOAL]
case succ
S : Type u
inst✝ : Semiring S
n✝ : ℕ
⊢ eval 0 (pochhammer S (Nat.succ n✝)) = if Nat.succ n✝ = 0 then 1 else 0
[PROOFSTEP]
simp [X_mul, Nat.succ_ne_zero, pochhammer_succ_left]
[GOAL]
S : Type u
inst✝ : Semiring S
⊢ eval 0 (pochhammer S 0) = 1
[PROOFSTEP]
simp
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
h : n ≠ 0
⊢ eval 0 (pochhammer S n) = 0
[PROOFSTEP]
simp [pochhammer_eval_zero, h]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ pochhammer S (n + 1) = pochhammer S n * (X + ↑n)
[PROOFSTEP]
suffices h : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + (n : ℕ[X]))
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
h : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
⊢ pochhammer S (n + 1) = pochhammer S n * (X + ↑n)
[PROOFSTEP]
apply_fun Polynomial.map (algebraMap ℕ S) at h 
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
h : map (algebraMap ℕ S) (pochhammer ℕ (n + 1)) = map (algebraMap ℕ S) (pochhammer ℕ n * (X + ↑n))
⊢ pochhammer S (n + 1) = pochhammer S n * (X + ↑n)
[PROOFSTEP]
simpa only [pochhammer_map, Polynomial.map_mul, Polynomial.map_add, map_X, Polynomial.map_nat_cast] using h
[GOAL]
case h
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case h.zero
S : Type u
inst✝ : Semiring S
⊢ pochhammer ℕ (Nat.zero + 1) = pochhammer ℕ Nat.zero * (X + ↑Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case h.succ
S : Type u
inst✝ : Semiring S
n : ℕ
ih : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
⊢ pochhammer ℕ (Nat.succ n + 1) = pochhammer ℕ (Nat.succ n) * (X + ↑(Nat.succ n))
[PROOFSTEP]
conv_lhs =>
  rw [pochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← pochhammer_succ_left, add_comp, X_comp, nat_cast_comp,
    add_assoc, add_comm (1 : ℕ[X]), ← Nat.cast_succ]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
ih : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
| pochhammer ℕ (Nat.succ n + 1)
[PROOFSTEP]
rw [pochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← pochhammer_succ_left, add_comp, X_comp, nat_cast_comp, add_assoc,
    add_comm (1 : ℕ[X]), ← Nat.cast_succ]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
ih : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
| pochhammer ℕ (Nat.succ n + 1)
[PROOFSTEP]
rw [pochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← pochhammer_succ_left, add_comp, X_comp, nat_cast_comp, add_assoc,
    add_comm (1 : ℕ[X]), ← Nat.cast_succ]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
ih : pochhammer ℕ (n + 1) = pochhammer ℕ n * (X + ↑n)
| pochhammer ℕ (Nat.succ n + 1)
[PROOFSTEP]
rw [pochhammer_succ_left, ih, mul_comp, ← mul_assoc, ← pochhammer_succ_left, add_comp, X_comp, nat_cast_comp, add_assoc,
  add_comm (1 : ℕ[X]), ← Nat.cast_succ]
[GOAL]
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)
[PROOFSTEP]
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]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ comp (pochhammer S (n + 1)) (X + 1) = pochhammer S (n + 1) + (n + 1) • comp (pochhammer S n) (X + 1)
[PROOFSTEP]
suffices (pochhammer ℕ (n + 1)).comp (X + 1) = pochhammer ℕ (n + 1) + (n + 1) * (pochhammer ℕ n).comp (X + 1) by
  simpa [map_comp] using congr_arg (Polynomial.map (Nat.castRingHom S)) this
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
this : comp (pochhammer ℕ (n + 1)) (X + 1) = pochhammer ℕ (n + 1) + (↑n + 1) * comp (pochhammer ℕ n) (X + 1)
⊢ comp (pochhammer S (n + 1)) (X + 1) = pochhammer S (n + 1) + (n + 1) • comp (pochhammer S n) (X + 1)
[PROOFSTEP]
simpa [map_comp] using congr_arg (Polynomial.map (Nat.castRingHom S)) this
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ comp (pochhammer ℕ (n + 1)) (X + 1) = pochhammer ℕ (n + 1) + (↑n + 1) * comp (pochhammer ℕ n) (X + 1)
[PROOFSTEP]
nth_rw 2 [pochhammer_succ_left]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ comp (pochhammer ℕ (n + 1)) (X + 1) = X * comp (pochhammer ℕ n) (X + 1) + (↑n + 1) * comp (pochhammer ℕ n) (X + 1)
[PROOFSTEP]
rw [← add_mul, pochhammer_succ_right ℕ n, mul_comp, mul_comm, add_comp, X_comp, nat_cast_comp, add_comm, ← add_assoc]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (↑n + X + 1) * comp (pochhammer ℕ n) (X + 1) = (X + (↑n + 1)) * comp (pochhammer ℕ n) (X + 1)
[PROOFSTEP]
ring
[GOAL]
S : Type u
inst✝ : Semiring S
p q : S[X]
n : ℕ
⊢ comp (p * (X + ↑n)) q = comp p q * (q + ↑n)
[PROOFSTEP]
rw [mul_add, add_comp, mul_X_comp, ← Nat.cast_comm, nat_cast_mul_comp, Nat.cast_comm, mul_add]
[GOAL]
S : Type u
inst✝ : Semiring S
n m : ℕ
⊢ pochhammer S n * comp (pochhammer S m) (X + ↑n) = pochhammer S (n + m)
[PROOFSTEP]
induction' m with m ih
[GOAL]
case zero
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ pochhammer S n * comp (pochhammer S Nat.zero) (X + ↑n) = pochhammer S (n + Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case succ
S : Type u
inst✝ : Semiring S
n m : ℕ
ih : pochhammer S n * comp (pochhammer S m) (X + ↑n) = pochhammer S (n + m)
⊢ pochhammer S n * comp (pochhammer S (Nat.succ m)) (X + ↑n) = pochhammer S (n + Nat.succ m)
[PROOFSTEP]
rw [pochhammer_succ_right, Polynomial.mul_X_add_nat_cast_comp, ← mul_assoc, ih, Nat.succ_eq_add_one, ← add_assoc,
  pochhammer_succ_right, Nat.cast_add, add_assoc]
[GOAL]
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ eval (n + 1) (pochhammer ℕ 0) = Nat.ascFactorial n 0
[PROOFSTEP]
rw [pochhammer_zero, eval_one, Nat.ascFactorial_zero]
[GOAL]
S : Type u
inst✝ : Semiring S
n t : ℕ
⊢ eval (n + 1) (pochhammer ℕ (t + 1)) = Nat.ascFactorial n (t + 1)
[PROOFSTEP]
rw [pochhammer_succ_right, eval_mul, pochhammer_nat_eq_ascFactorial n t]
[GOAL]
S : Type u
inst✝ : Semiring S
n t : ℕ
⊢ Nat.ascFactorial n t * eval (n + 1) (X + ↑t) = Nat.ascFactorial n (t + 1)
[PROOFSTEP]
simp only [eval_add, eval_X, eval_nat_cast, Nat.cast_id]
[GOAL]
S : Type u
inst✝ : Semiring S
n t : ℕ
⊢ Nat.ascFactorial n t * (n + 1 + t) = Nat.ascFactorial n (t + 1)
[PROOFSTEP]
rw [Nat.ascFactorial_succ, add_right_comm, mul_comm]
[GOAL]
S : Type u
inst✝ : Semiring S
a b : ℕ
⊢ eval a (pochhammer ℕ b) = Nat.descFactorial (a + b - 1) b
[PROOFSTEP]
cases' b with b
[GOAL]
case zero
S : Type u
inst✝ : Semiring S
a : ℕ
⊢ eval a (pochhammer ℕ Nat.zero) = Nat.descFactorial (a + Nat.zero - 1) Nat.zero
[PROOFSTEP]
rw [Nat.descFactorial_zero, pochhammer_zero, Polynomial.eval_one]
[GOAL]
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)
[PROOFSTEP]
rw [Nat.add_succ, Nat.succ_sub_succ, tsub_zero]
[GOAL]
case succ
S : Type u
inst✝ : Semiring S
a b : ℕ
⊢ eval a (pochhammer ℕ (Nat.succ b)) = Nat.descFactorial (a + b) (Nat.succ b)
[PROOFSTEP]
cases a
[GOAL]
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)
[PROOFSTEP]
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]
[GOAL]
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)
[PROOFSTEP]
rw [Nat.succ_add, ← Nat.add_succ, Nat.add_descFactorial_eq_ascFactorial, pochhammer_nat_eq_ascFactorial]
[GOAL]
S : Type u_1
inst✝ : StrictOrderedSemiring S
n : ℕ
s : S
h : 0 < s
⊢ 0 < eval s (pochhammer S n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
⊢ 0 < eval s (pochhammer S Nat.zero)
[PROOFSTEP]
simp only [Nat.zero_eq, pochhammer_zero, eval_one]
[GOAL]
case zero
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
case succ
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (pochhammer S n)
⊢ 0 < eval s (pochhammer S (Nat.succ n))
[PROOFSTEP]
rw [pochhammer_succ_right, mul_add, eval_add, ← Nat.cast_comm, eval_nat_cast_mul, eval_mul_X, Nat.cast_comm, ← mul_add]
[GOAL]
case succ
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (pochhammer S n)
⊢ 0 < eval s (pochhammer S n) * (s + ↑n)
[PROOFSTEP]
exact mul_pos ih (lt_of_lt_of_le h ((le_add_iff_nonneg_right _).mpr (Nat.cast_nonneg n)))
[GOAL]
S✝ : Type u_1
inst✝¹ : Semiring S✝
r n✝ : ℕ
S : Type u_2
inst✝ : Semiring S
n : ℕ
⊢ eval 1 (pochhammer S n) = ↑n !
[PROOFSTEP]
rw_mod_cast [pochhammer_nat_eq_ascFactorial, Nat.zero_ascFactorial]
[GOAL]
S✝ : Type u_1
inst✝¹ : Semiring S✝
r✝ n✝ : ℕ
S : Type u_2
inst✝ : Semiring S
r n : ℕ
⊢ ↑r ! * eval (↑r + 1) (pochhammer S n) = ↑(r + n)!
[PROOFSTEP]
rw_mod_cast [pochhammer_nat_eq_ascFactorial, Nat.factorial_mul_ascFactorial]
[GOAL]
S : Type u_1
inst✝ : Semiring S
r✝ n r : ℕ
⊢ 0 * eval (0 + 1) (pochhammer ℕ r) = (0 + r) * eval 0 (pochhammer ℕ r)
[PROOFSTEP]
by_cases h : r = 0
[GOAL]
case pos
S : Type u_1
inst✝ : Semiring S
r✝ n r : ℕ
h : r = 0
⊢ 0 * eval (0 + 1) (pochhammer ℕ r) = (0 + r) * eval 0 (pochhammer ℕ r)
[PROOFSTEP]
simp only [h, zero_mul, zero_add]
[GOAL]
case neg
S : Type u_1
inst✝ : Semiring S
r✝ n r : ℕ
h : ¬r = 0
⊢ 0 * eval (0 + 1) (pochhammer ℕ r) = (0 + r) * eval 0 (pochhammer ℕ r)
[PROOFSTEP]
simp only [pochhammer_eval_zero, zero_mul, if_neg h, mul_zero]
[GOAL]
S : Type u_1
inst✝ : Semiring S
r✝ n r k : ℕ
⊢ (k + 1) * eval (k + 1 + 1) (pochhammer ℕ r) = (k + 1 + r) * eval (k + 1) (pochhammer ℕ r)
[PROOFSTEP]
simp only [pochhammer_nat_eq_ascFactorial, Nat.succ_ascFactorial, add_right_comm]
[GOAL]
S : Type u_1
inst✝ : Semiring S
r✝ n✝ r n : ℕ
⊢ ↑n * eval (↑n + 1) (pochhammer S r) = (↑n + ↑r) * eval (↑n) (pochhammer S r)
[PROOFSTEP]
exact_mod_cast congr_arg Nat.cast (pochhammer_nat_eval_succ r n)
