n k : ℕ
hk : k ≤ n
⊢ choose n k = choose n k * (k ! * (n - k)!) / (k ! * (n - k)!)
n k : ℕ
hk : k ≤ n
⊢ choose n k = n ! / (k ! * (n - k)!)
rw [← choose_mul_factorial_mul_factorial hk, mul_assoc]
no goals
n k : ℕ
hk : k ≤ n
⊢ choose n k = choose n k * (k ! * (n - k)!) / (k ! * (n - k)!)
exact (mul_div_left _ (mul_pos (factorial_pos _) (factorial_pos _))).symm