-- Mathlib/Data/Nat/Factorial/Cast.lean
theorem cast_descFactorial :
    (a.descFactorial b : S) = (ascPochhammer S b).eval (a - (b - 1) : S)

Proof state:
case succ.inl
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : a ≤ b
⊢ ↑(a.descFactorial (b + 0).succ) = ↑((a - b + b).descFactorial (b + 0).succ)

Tactic:
rw [descFactorial_of_lt (lt_succ_of_le h), descFactorial_of_lt (lt_succ_of_le _)]

Result:
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : a ≤ b
⊢ a - b + b ≤ b

Proof state:
case succ.inr
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : b ≤ a
⊢ ↑(a.descFactorial (b + 0).succ) = ↑((a - b + b).descFactorial (b + 0).succ)

Tactic:
rw [tsub_add_cancel_of_le h]

Result:
no goals

Proof state:
case zero
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(a.descFactorial 0) = ↑((a - (0 - 1) + 0 - 1).descFactorial 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
⊢ ↑(a.descFactorial (b + 1)) = ↑((a - (b + 1 - 1) + (b + 1) - 1).descFactorial (b + 1))

Tactic:
simp_rw [add_succ, Nat.add_one_sub_one]

Result:
case succ
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
⊢ ↑(a.descFactorial (b + 0).succ) = ↑((a - b + b).descFactorial (b + 0).succ)

Proof state:
case succ
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
⊢ ↑(a.descFactorial (b + 0).succ) = ↑((a - b + b).descFactorial (b + 0).succ)

Tactic:
obtain h | h := le_total a b

Result:
case succ.inl
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : a ≤ b
⊢ ↑(a.descFactorial (b + 0).succ) = ↑((a - b + b).descFactorial (b + 0).succ)

case succ.inr
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : b ≤ a
⊢ ↑(a.descFactorial (b + 0).succ) = ↑((a - b + b).descFactorial (b + 0).succ)

Proof state:
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
h : a ≤ b
⊢ a - b + b ≤ b

Tactic:
rw [tsub_eq_zero_iff_le.mpr h, zero_add]

Result:
no goals

Proof state:
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)

Tactic:
induction' b with b

Result:
case zero
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(a.descFactorial 0) = ↑((a - (0 - 1) + 0 - 1).descFactorial 0)

case succ
S : Type u_1
inst✝ : Semiring S
a b✝ b : ℕ
a✝ : ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)
⊢ ↑(a.descFactorial (b + 1)) = ↑((a - (b + 1 - 1) + (b + 1) - 1).descFactorial (b + 1))

Proof state:
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(a.descFactorial b) = Polynomial.eval (↑(a - (b - 1))) (ascPochhammer S b)

Tactic:
rw [← ascPochhammer_eval_cast, ascPochhammer_nat_eq_descFactorial]

Result:
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(a.descFactorial b) = ↑((a - (b - 1) + b - 1).descFactorial b)