[GOAL]
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(ascFactorial a b) = Polynomial.eval (↑a + 1) (pochhammer S b)
[PROOFSTEP]
rw [← pochhammer_nat_eq_ascFactorial, pochhammer_eval_cast, Nat.cast_add, Nat.cast_one]
[GOAL]
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(descFactorial a b) = Polynomial.eval (↑(a - (b - 1))) (pochhammer S b)
[PROOFSTEP]
rw [← pochhammer_eval_cast, pochhammer_nat_eq_descFactorial]
[GOAL]
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(descFactorial a b) = ↑(descFactorial (a - (b - 1) + b - 1) b)
[PROOFSTEP]
induction' b with b
[GOAL]
case zero
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(descFactorial a zero) = ↑(descFactorial (a - (zero - 1) + zero - 1) zero)
[PROOFSTEP]
simp
[GOAL]
case succ
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
n_ih✝ : ↑(descFactorial a b) = ↑(descFactorial (a - (b - 1) + b - 1) b)
⊢ ↑(descFactorial a (succ b)) = ↑(descFactorial (a - (succ b - 1) + succ b - 1) (succ b))
[PROOFSTEP]
simp_rw [add_succ, succ_sub_one]
[GOAL]
case succ
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
n_ih✝ : ↑(descFactorial a b) = ↑(descFactorial (a - (b - 1) + b - 1) b)
⊢ ↑(descFactorial a (succ b)) = ↑(descFactorial (a - b + b) (succ b))
[PROOFSTEP]
obtain h | h := le_total a b
[GOAL]
case succ.inl
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
n_ih✝ : ↑(descFactorial a b) = ↑(descFactorial (a - (b - 1) + b - 1) b)
h : a ≤ b
⊢ ↑(descFactorial a (succ b)) = ↑(descFactorial (a - b + b) (succ b))
[PROOFSTEP]
rw [descFactorial_of_lt (lt_succ_of_le h), descFactorial_of_lt (lt_succ_of_le _)]
[GOAL]
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
n_ih✝ : ↑(descFactorial a b) = ↑(descFactorial (a - (b - 1) + b - 1) b)
h : a ≤ b
⊢ a - b + b ≤ b
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr h, zero_add]
[GOAL]
case succ.inr
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
n_ih✝ : ↑(descFactorial a b) = ↑(descFactorial (a - (b - 1) + b - 1) b)
h : b ≤ a
⊢ ↑(descFactorial a (succ b)) = ↑(descFactorial (a - b + b) (succ b))
[PROOFSTEP]
rw [tsub_add_cancel_of_le h]
[GOAL]
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑a ! = Polynomial.eval 1 (pochhammer S a)
[PROOFSTEP]
rw [← zero_ascFactorial, cast_ascFactorial, cast_zero, zero_add]
[GOAL]
S : Type u_1
inst✝ : Ring S
a b : ℕ
⊢ ↑(descFactorial a 2) = ↑a * (↑a - 1)
[PROOFSTEP]
rw [cast_descFactorial]
[GOAL]
S : Type u_1
inst✝ : Ring S
a b : ℕ
⊢ Polynomial.eval (↑(a - (2 - 1))) (pochhammer S 2) = ↑a * (↑a - 1)
[PROOFSTEP]
cases a
[GOAL]
case zero
S : Type u_1
inst✝ : Ring S
b : ℕ
⊢ Polynomial.eval (↑(zero - (2 - 1))) (pochhammer S 2) = ↑zero * (↑zero - 1)
[PROOFSTEP]
simp
[GOAL]
case succ
S : Type u_1
inst✝ : Ring S
b n✝ : ℕ
⊢ Polynomial.eval (↑(succ n✝ - (2 - 1))) (pochhammer S 2) = ↑(succ n✝) * (↑(succ n✝) - 1)
[PROOFSTEP]
rw [succ_sub_succ, tsub_zero, cast_succ, add_sub_cancel, pochhammer_succ_right, pochhammer_one, Polynomial.X_mul,
  Polynomial.eval_mul_X, Polynomial.eval_add, Polynomial.eval_X, cast_one, Polynomial.eval_one]
