S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(descFactorial a b) = ↑(descFactorial (a - (b - 1) + b - 1) b)
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(descFactorial a b) = Polynomial.eval (↑(a - (b - 1))) (pochhammer S b)
rw [← pochhammer_eval_cast, pochhammer_nat_eq_descFactorial]
case zero
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(descFactorial a zero) = ↑(descFactorial (a - (zero - 1) + zero - 1) zero)

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))
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(descFactorial a b) = ↑(descFactorial (a - (b - 1) + b - 1) b)
induction' b with b
no goals
case zero
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(descFactorial a zero) = ↑(descFactorial (a - (zero - 1) + zero - 1) zero)
simp
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))
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))
simp_rw [add_succ, succ_sub_one]
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))

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))
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))
obtain h | h := le_total a b
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
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))
rw [descFactorial_of_lt (lt_succ_of_le h), descFactorial_of_lt (lt_succ_of_le _)]
no goals
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
rw [tsub_eq_zero_iff_le.mpr h, zero_add]
no goals
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))
rw [tsub_add_cancel_of_le h]