n k : ℕ
⊢ k ! * choose (n + k) k = k ! * (ascFactorial n k / k !)
n k : ℕ
⊢ choose (n + k) k = ascFactorial n k / k !
apply mul_left_cancel₀ (factorial_ne_zero k)
n k : ℕ
⊢ ascFactorial n k = k ! * (ascFactorial n k / k !)
n k : ℕ
⊢ k ! * choose (n + k) k = k ! * (ascFactorial n k / k !)
rw [← ascFactorial_eq_factorial_mul_choose]
no goals
n k : ℕ
⊢ ascFactorial n k = k ! * (ascFactorial n k / k !)
exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm