n k : ℕ
⊢ ascFactorial n k = choose (n + k) k * k !
n k : ℕ
⊢ ascFactorial n k = k ! * choose (n + k) k
rw [mul_comm]
n k : ℕ
⊢ ascFactorial n k * (n + k - k)! = choose (n + k) k * k ! * (n + k - k)!
n k : ℕ
⊢ ascFactorial n k = choose (n + k) k * k !
apply mul_right_cancel₀ (factorial_ne_zero (n + k - k))
n k : ℕ
⊢ k ≤ n + k
n k : ℕ
⊢ ascFactorial n k * (n + k - k)! = choose (n + k) k * k ! * (n + k - k)!
rw [choose_mul_factorial_mul_factorial, add_tsub_cancel_right, ← factorial_mul_ascFactorial,
  mul_comm]
no goals
n k : ℕ
⊢ k ≤ n + k
exact Nat.le_add_left k n