no goals
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(choose a b) = Polynomial.eval (↑(a - (b - 1))) (pochhammer K b) / ↑b !
rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
  mul_comm, ← descFactorial_eq_factorial_mul_choose, ← cast_descFactorial]