no goals
x✝ : ℕ
hk : x✝ ≤ 0
⊢ choose 0 x✝ * x✝! * (0 - x✝)! = 0!
simp [Nat.eq_zero_of_le_zero hk]
no goals
n : ℕ
x✝ : 0 ≤ n + 1
⊢ choose (n + 1) 0 * 0! * (n + 1 - 0)! = (n + 1)!
simp
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!

case inr
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k = n + 1
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
n k : ℕ
hk : succ k ≤ n + 1
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
cases' lt_or_eq_of_le hk with hk₁ hk₁
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
have h : choose n k * k.succ ! * (n - k)! = (k + 1) * n ! := by
  rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)];
    simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - succ k)!
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
have h₁ : (n - k)! = (n - k) * (n - k.succ)! := by
  rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - succ k)!
h₂ : choose n (succ k) * (succ k)! * ((n - k) * (n - succ k)!) = (n - k) * n !
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - succ k)!
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
have h₂ : choose n (succ k) * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n ! := by
  rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)];
    simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - succ k)!
h₂ : choose n (succ k) * (succ k)! * ((n - k) * (n - succ k)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - succ k)!
h₂ : choose n (succ k) * (succ k)! * ((n - k) * (n - succ k)!) = (n - k) * n !
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
have h₃ : k * n ! ≤ n * n ! := Nat.mul_le_mul_right _ (le_of_succ_le_succ hk)
no goals
case inl
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - succ k)!
h₂ : choose n (succ k) * (succ k)! * ((n - k) * (n - succ k)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
rw [choose_succ_succ, add_mul, add_mul, succ_sub_succ, h, h₁, h₂, add_mul, tsub_mul,
  factorial_succ, ← add_tsub_assoc_of_le h₃, add_assoc, ← add_mul, add_tsub_cancel_left,
  add_comm]
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
⊢ choose n k * (succ k)! * (n - k)! = (k + 1) * (choose n k * k ! * (n - k)!)
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
⊢ choose n k * (succ k)! * (n - k)! = (k + 1) * n !
rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]
no goals
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
⊢ choose n k * (succ k)! * (n - k)! = (k + 1) * (choose n k * k ! * (n - k)!)
simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
no goals
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
⊢ (n - k)! = (n - k) * (n - succ k)!
rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - succ k)!
⊢ choose n (succ k) * (succ k)! * ((n - k) * (n - succ k)!) = (n - k) * (choose n (succ k) * (succ k)! * (n - succ k)!)
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - succ k)!
⊢ choose n (succ k) * (succ k)! * ((n - k) * (n - succ k)!) = (n - k) * n !
rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
no goals
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
h : choose n k * (succ k)! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - succ k)!
⊢ choose n (succ k) * (succ k)! * ((n - k) * (n - succ k)!) = (n - k) * (choose n (succ k) * (succ k)! * (n - succ k)!)
simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
case inr
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k = n + 1
⊢ choose (n + 1) (n + 1) * (n + 1)! * (n + 1 - (n + 1))! = (n + 1)!
case inr
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k = n + 1
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
rw [hk₁]
no goals
case inr
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k = n + 1
⊢ choose (n + 1) (n + 1) * (n + 1)! * (n + 1 - (n + 1))! = (n + 1)!
simp [hk₁, mul_comm, choose, tsub_self]