[GOAL]
n : ℕ
⊢ choose n 0 = 1
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ choose zero 0 = 1
[PROOFSTEP]
rfl
[GOAL]
case succ
n✝ : ℕ
⊢ choose (succ n✝) 0 = 1
[PROOFSTEP]
rfl
[GOAL]
n k : ℕ
hk : n + 1 < k + 1
⊢ choose (n + 1) (k + 1) = 0
[PROOFSTEP]
have hnk : n < k := lt_of_succ_lt_succ hk
[GOAL]
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
⊢ choose (n + 1) (k + 1) = 0
[PROOFSTEP]
have hnk1 : n < k + 1 := lt_of_succ_lt hk
[GOAL]
n k : ℕ
hk : n + 1 < k + 1
hnk : n < k
hnk1 : n < k + 1
⊢ choose (n + 1) (k + 1) = 0
[PROOFSTEP]
rw [choose_succ_succ, choose_eq_zero_of_lt hnk, choose_eq_zero_of_lt hnk1]
[GOAL]
n : ℕ
⊢ choose n n = 1
[PROOFSTEP]
induction n
[GOAL]
case zero
⊢ choose zero zero = 1
[PROOFSTEP]
simp [*, choose, choose_eq_zero_of_lt (lt_succ_self _)]
[GOAL]
case succ
n✝ : ℕ
n_ih✝ : choose n✝ n✝ = 1
⊢ choose (succ n✝) (succ n✝) = 1
[PROOFSTEP]
simp [*, choose, choose_eq_zero_of_lt (lt_succ_self _)]
[GOAL]
n : ℕ
⊢ choose n 1 = n
[PROOFSTEP]
induction n
[GOAL]
case zero
⊢ choose zero 1 = zero
[PROOFSTEP]
simp [*, choose, add_comm]
[GOAL]
case succ
n✝ : ℕ
n_ih✝ : choose n✝ 1 = n✝
⊢ choose (succ n✝) 1 = succ n✝
[PROOFSTEP]
simp [*, choose, add_comm]
[GOAL]
n : ℕ
⊢ (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n
[PROOFSTEP]
rw [← add_mul_div_left, mul_comm 2 n, ← mul_add, add_tsub_cancel_right, mul_comm]
[GOAL]
n : ℕ
⊢ n * (n + 1) / 2 = n * (n - 1 + 2) / 2
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ zero * (zero + 1) / 2 = zero * (zero - 1 + 2) / 2
[PROOFSTEP]
rfl
[GOAL]
case succ
n✝ : ℕ
⊢ succ n✝ * (succ n✝ + 1) / 2 = succ n✝ * (succ n✝ - 1 + 2) / 2
[PROOFSTEP]
rfl
[GOAL]
case H
n : ℕ
⊢ 0 < 2
[PROOFSTEP]
apply zero_lt_succ
[GOAL]
n : ℕ
⊢ choose n 2 = n * (n - 1) / 2
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
⊢ choose zero 2 = zero * (zero - 1) / 2
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
ih : choose n 2 = n * (n - 1) / 2
⊢ choose (succ n) 2 = succ n * (succ n - 1) / 2
[PROOFSTEP]
rw [triangle_succ n, choose, ih]
[GOAL]
case succ
n : ℕ
ih : choose n 2 = n * (n - 1) / 2
⊢ choose n 1 + n * (n - 1) / 2 = n * (n - 1) / 2 + n
[PROOFSTEP]
simp [add_comm]
[GOAL]
x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 x✝
[PROOFSTEP]
rw [Nat.eq_zero_of_le_zero hk]
[GOAL]
x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 0
[PROOFSTEP]
decide
[GOAL]
n : ℕ
x✝ : 0 ≤ n + 1
⊢ 0 < choose (n + 1) 0
[PROOFSTEP]
simp
[GOAL]
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ 0 < choose (n + 1) (k + 1)
[PROOFSTEP]
rw [choose_succ_succ]
[GOAL]
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ 0 < choose n k + choose n (succ k)
[PROOFSTEP]
exact add_pos_of_pos_of_nonneg (choose_pos (le_of_succ_le_succ hk)) (Nat.zero_le _)
[GOAL]
⊢ succ 0 * choose 0 0 = choose (succ 0) (succ 0) * succ 0
[PROOFSTEP]
decide
[GOAL]
k : ℕ
⊢ succ 0 * choose 0 (k + 1) = choose (succ 0) (succ (k + 1)) * succ (k + 1)
[PROOFSTEP]
simp [choose]
[GOAL]
n : ℕ
⊢ succ (n + 1) * choose (n + 1) 0 = choose (succ (n + 1)) (succ 0) * succ 0
[PROOFSTEP]
simp [choose, mul_succ, succ_eq_add_one, add_comm]
[GOAL]
n k : ℕ
⊢ succ (n + 1) * choose (n + 1) (k + 1) = choose (succ (n + 1)) (succ (k + 1)) * succ (k + 1)
[PROOFSTEP]
rw [choose_succ_succ (succ n) (succ k), add_mul, ← succ_mul_choose_eq n, mul_succ, ← succ_mul_choose_eq n,
  add_right_comm, ← mul_add, ← choose_succ_succ, ← succ_mul]
[GOAL]
x✝ : ℕ
hk : x✝ ≤ 0
⊢ choose 0 x✝ * x✝! * (0 - x✝)! = 0!
[PROOFSTEP]
simp [Nat.eq_zero_of_le_zero hk]
[GOAL]
n : ℕ
x✝ : 0 ≤ n + 1
⊢ choose (n + 1) 0 * 0! * (n + 1 - 0)! = (n + 1)!
[PROOFSTEP]
simp
[GOAL]
n k : ℕ
hk : succ k ≤ n + 1
⊢ choose (n + 1) (succ k) * (succ k)! * (n + 1 - succ k)! = (n + 1)!
[PROOFSTEP]
cases' lt_or_eq_of_le hk with hk₁ hk₁
[GOAL]
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)!
[PROOFSTEP]
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]
[GOAL]
n k : ℕ
hk : succ k ≤ n + 1
hk₁ : succ k < n + 1
⊢ choose n k * (succ k)! * (n - k)! = (k + 1) * n !
[PROOFSTEP]
rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]
[GOAL]
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)!)
[PROOFSTEP]
simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
[GOAL]
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)!
[PROOFSTEP]
have h₁ : (n - k)! = (n - k) * (n - k.succ)! := by rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
[GOAL]
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)!
[PROOFSTEP]
rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
[GOAL]
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)!
[PROOFSTEP]
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]
[GOAL]
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 !
[PROOFSTEP]
rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
[GOAL]
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)!)
[PROOFSTEP]
simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
[GOAL]
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)!
[PROOFSTEP]
have h₃ : k * n ! ≤ n * n ! := Nat.mul_le_mul_right _ (le_of_succ_le_succ hk)
[GOAL]
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)!
[PROOFSTEP]
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]
[GOAL]
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)!
[PROOFSTEP]
rw [hk₁]
[GOAL]
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)!
[PROOFSTEP]
simp [hk₁, mul_comm, choose, tsub_self]
[GOAL]
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
⊢ (n - k)! * (k - s)! * s ! ≠ 0
[PROOFSTEP]
apply_rules [factorial_ne_zero, mul_ne_zero]
[GOAL]
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : (n - k)! * (k - s)! * s ! ≠ 0
⊢ choose n k * choose k s * ((n - k)! * (k - s)! * s !) = choose n k * (choose k s * s ! * (k - s)!) * (n - k)!
[PROOFSTEP]
rw [mul_assoc, mul_assoc, mul_assoc, mul_assoc _ s !, mul_assoc, mul_comm (n - k)!, mul_comm s !]
[GOAL]
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : (n - k)! * (k - s)! * s ! ≠ 0
⊢ choose n k * (choose k s * s ! * (k - s)!) * (n - k)! = n !
[PROOFSTEP]
rw [choose_mul_factorial_mul_factorial hsk, choose_mul_factorial_mul_factorial hkn]
[GOAL]
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : (n - k)! * (k - s)! * s ! ≠ 0
⊢ n ! = choose n s * s ! * (choose (n - s) (k - s) * (k - s)! * (n - s - (k - s))!)
[PROOFSTEP]
rw [choose_mul_factorial_mul_factorial (tsub_le_tsub_right hkn _), choose_mul_factorial_mul_factorial (hsk.trans hkn)]
[GOAL]
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : (n - k)! * (k - s)! * s ! ≠ 0
⊢ choose n s * s ! * (choose (n - s) (k - s) * (k - s)! * (n - s - (k - s))!) =
    choose n s * choose (n - s) (k - s) * ((n - k)! * (k - s)! * s !)
[PROOFSTEP]
rw [tsub_tsub_tsub_cancel_right hsk, mul_assoc, mul_left_comm s !, mul_assoc, mul_comm (k - s)!, mul_comm s !,
  mul_right_comm, ← mul_assoc]
[GOAL]
n k : ℕ
hk : k ≤ n
⊢ choose n k = n ! / (k ! * (n - k)!)
[PROOFSTEP]
rw [← choose_mul_factorial_mul_factorial hk, mul_assoc]
[GOAL]
n k : ℕ
hk : k ≤ n
⊢ choose n k = choose n k * (k ! * (n - k)!) / (k ! * (n - k)!)
[PROOFSTEP]
exact (mul_div_left _ (mul_pos (factorial_pos _) (factorial_pos _))).symm
[GOAL]
i j : ℕ
⊢ choose (i + j) j = (i + j)! / (i ! * j !)
[PROOFSTEP]
rw [choose_eq_factorial_div_factorial (Nat.le_add_left j i), add_tsub_cancel_right, mul_comm]
[GOAL]
i j : ℕ
⊢ choose (i + j) j * i ! * j ! = (i + j)!
[PROOFSTEP]
rw [← choose_mul_factorial_mul_factorial (Nat.le_add_left _ _), add_tsub_cancel_right, mul_right_comm]
[GOAL]
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n !
[PROOFSTEP]
rw [← choose_mul_factorial_mul_factorial hk, mul_assoc]
[GOAL]
n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ choose n k * (k ! * (n - k)!)
[PROOFSTEP]
exact dvd_mul_left _ _
[GOAL]
i j : ℕ
⊢ i ! * j ! ∣ (i + j)!
[PROOFSTEP]
suffices : i ! * (i + j - i)! ∣ (i + j)!
[GOAL]
i j : ℕ
this : i ! * (i + j - i)! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!
[PROOFSTEP]
rwa [add_tsub_cancel_left i j] at this 
[GOAL]
case this
i j : ℕ
⊢ i ! * (i + j - i)! ∣ (i + j)!
[PROOFSTEP]
exact factorial_mul_factorial_dvd_factorial (Nat.le_add_right _ _)
[GOAL]
n k : ℕ
hk : k ≤ n
⊢ choose n (n - k) = choose n k
[PROOFSTEP]
rw [choose_eq_factorial_div_factorial hk, choose_eq_factorial_div_factorial (Nat.sub_le _ _), tsub_tsub_cancel_of_le hk,
  mul_comm]
[GOAL]
n a b : ℕ
h : n = a + b
⊢ choose n a = choose n b
[PROOFSTEP]
suffices : choose n (n - b) = choose n b
[GOAL]
n a b : ℕ
h : n = a + b
this : choose n (n - b) = choose n b
⊢ choose n a = choose n b
[PROOFSTEP]
rw [h, add_tsub_cancel_right] at this 
[GOAL]
n a b : ℕ
h : n = a + b
this : choose (a + b) a = choose (a + b) b
⊢ choose n a = choose n b
[PROOFSTEP]
rwa [h]
[GOAL]
case this
n a b : ℕ
h : n = a + b
⊢ choose n (n - b) = choose n b
[PROOFSTEP]
exact choose_symm (h ▸ le_add_left _ _)
[GOAL]
m : ℕ
⊢ choose (2 * m + 1) (m + 1) = choose (2 * m + 1) m
[PROOFSTEP]
apply choose_symm_of_eq_add
[GOAL]
case h
m : ℕ
⊢ 2 * m + 1 = m + 1 + m
[PROOFSTEP]
rw [add_comm m 1, add_assoc 1 m m, add_comm (2 * m) 1, two_mul m]
[GOAL]
n k : ℕ
⊢ choose n (k + 1) * (k + 1) = choose n k * (n - k)
[PROOFSTEP]
have e : (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)
[GOAL]
case e
n k : ℕ
⊢ (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)
n k : ℕ
e : (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)
⊢ choose n (k + 1) * (k + 1) = choose n k * (n - k)
[PROOFSTEP]
rw [← right_distrib, ← choose_succ_succ, succ_mul_choose_eq]
[GOAL]
n k : ℕ
e : (n + 1) * choose n k = choose n k * (k + 1) + choose n (k + 1) * (k + 1)
⊢ choose n (k + 1) * (k + 1) = choose n k * (n - k)
[PROOFSTEP]
rw [← tsub_eq_of_eq_add_rev e, mul_comm, ← mul_tsub, add_tsub_add_eq_tsub_right]
[GOAL]
n : ℕ
⊢ choose (n + 1 + 1) (n + 1) = n + 1 + 1
[PROOFSTEP]
rw [choose_succ_succ, choose_succ_self_right n, choose_self]
[GOAL]
n k : ℕ
⊢ choose n k * (n + 1) = choose (n + 1) k * (n + 1 - k)
[PROOFSTEP]
cases k with
| zero => simp
| succ k =>
  obtain hk | hk := le_or_lt (k + 1) (n + 1)
  ·
    rw [choose_succ_succ, add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ, mul_tsub,
      add_tsub_cancel_of_le (Nat.mul_le_mul_left _ hk)]
  · rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), zero_mul, zero_mul]
[GOAL]
n k : ℕ
⊢ choose n k * (n + 1) = choose (n + 1) k * (n + 1 - k)
[PROOFSTEP]
cases k with
| zero => simp
| succ k =>
  obtain hk | hk := le_or_lt (k + 1) (n + 1)
  ·
    rw [choose_succ_succ, add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ, mul_tsub,
      add_tsub_cancel_of_le (Nat.mul_le_mul_left _ hk)]
  · rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), zero_mul, zero_mul]
[GOAL]
case zero
n : ℕ
⊢ choose n zero * (n + 1) = choose (n + 1) zero * (n + 1 - zero)
[PROOFSTEP]

| zero => simp
[GOAL]
case zero
n : ℕ
⊢ choose n zero * (n + 1) = choose (n + 1) zero * (n + 1 - zero)
[PROOFSTEP]
simp
[GOAL]
case succ
n k : ℕ
⊢ choose n (succ k) * (n + 1) = choose (n + 1) (succ k) * (n + 1 - succ k)
[PROOFSTEP]

| succ k =>
  obtain hk | hk := le_or_lt (k + 1) (n + 1)
  ·
    rw [choose_succ_succ, add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ, mul_tsub,
      add_tsub_cancel_of_le (Nat.mul_le_mul_left _ hk)]
  · rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), zero_mul, zero_mul]
[GOAL]
case succ
n k : ℕ
⊢ choose n (succ k) * (n + 1) = choose (n + 1) (succ k) * (n + 1 - succ k)
[PROOFSTEP]
obtain hk | hk := le_or_lt (k + 1) (n + 1)
[GOAL]
case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ choose n (succ k) * (n + 1) = choose (n + 1) (succ k) * (n + 1 - succ k)
[PROOFSTEP]
rw [choose_succ_succ, add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ, mul_tsub,
  add_tsub_cancel_of_le (Nat.mul_le_mul_left _ hk)]
[GOAL]
case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ choose n (succ k) * (n + 1) = choose (n + 1) (succ k) * (n + 1 - succ k)
[PROOFSTEP]
rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), zero_mul, zero_mul]
[GOAL]
n k : ℕ
⊢ ascFactorial n k = k ! * choose (n + k) k
[PROOFSTEP]
rw [mul_comm]
[GOAL]
n k : ℕ
⊢ ascFactorial n k = choose (n + k) k * k !
[PROOFSTEP]
apply mul_right_cancel₀ (factorial_ne_zero (n + k - k))
[GOAL]
n k : ℕ
⊢ ascFactorial n k * (n + k - k)! = choose (n + k) k * k ! * (n + k - k)!
[PROOFSTEP]
rw [choose_mul_factorial_mul_factorial, add_tsub_cancel_right, ← factorial_mul_ascFactorial, mul_comm]
[GOAL]
n k : ℕ
⊢ k ≤ n + k
[PROOFSTEP]
exact Nat.le_add_left k n
[GOAL]
n k : ℕ
⊢ choose (n + k) k = ascFactorial n k / k !
[PROOFSTEP]
apply mul_left_cancel₀ (factorial_ne_zero k)
[GOAL]
n k : ℕ
⊢ k ! * choose (n + k) k = k ! * (ascFactorial n k / k !)
[PROOFSTEP]
rw [← ascFactorial_eq_factorial_mul_choose]
[GOAL]
n k : ℕ
⊢ ascFactorial n k = k ! * (ascFactorial n k / k !)
[PROOFSTEP]
exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm
[GOAL]
n k : ℕ
⊢ descFactorial n k = k ! * choose n k
[PROOFSTEP]
obtain h | h := Nat.lt_or_ge n k
[GOAL]
case inl
n k : ℕ
h : n < k
⊢ descFactorial n k = k ! * choose n k
[PROOFSTEP]
rw [descFactorial_eq_zero_iff_lt.2 h, choose_eq_zero_of_lt h, mul_zero]
[GOAL]
case inr
n k : ℕ
h : n ≥ k
⊢ descFactorial n k = k ! * choose n k
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case inr
n k : ℕ
h : n ≥ k
⊢ descFactorial n k = choose n k * k !
[PROOFSTEP]
apply mul_right_cancel₀ (factorial_ne_zero (n - k))
[GOAL]
case inr
n k : ℕ
h : n ≥ k
⊢ descFactorial n k * (n - k)! = choose n k * k ! * (n - k)!
[PROOFSTEP]
rw [choose_mul_factorial_mul_factorial h, ← factorial_mul_descFactorial h, mul_comm]
[GOAL]
n k : ℕ
⊢ choose n k = descFactorial n k / k !
[PROOFSTEP]
apply mul_left_cancel₀ (factorial_ne_zero k)
[GOAL]
n k : ℕ
⊢ k ! * choose n k = k ! * (descFactorial n k / k !)
[PROOFSTEP]
rw [← descFactorial_eq_factorial_mul_choose]
[GOAL]
n k : ℕ
⊢ descFactorial n k = k ! * (descFactorial n k / k !)
[PROOFSTEP]
exact (Nat.mul_div_cancel' <| factorial_dvd_descFactorial _ _).symm
[GOAL]
r n : ℕ
h : r < n / 2
⊢ choose n r ≤ choose n (r + 1)
[PROOFSTEP]
refine' le_of_mul_le_mul_right _ (lt_tsub_iff_left.mpr (lt_of_lt_of_le h (n.div_le_self 2)))
[GOAL]
r n : ℕ
h : r < n / 2
⊢ choose n r * (n - r) ≤ choose n (r + 1) * (n - r)
[PROOFSTEP]
rw [← choose_succ_right_eq]
[GOAL]
r n : ℕ
h : r < n / 2
⊢ choose n (r + 1) * (r + 1) ≤ choose n (r + 1) * (n - r)
[PROOFSTEP]
apply Nat.mul_le_mul_left
[GOAL]
case h
r n : ℕ
h : r < n / 2
⊢ r + 1 ≤ n - r
[PROOFSTEP]
rw [← Nat.lt_iff_add_one_le, lt_tsub_iff_left, ← mul_two]
[GOAL]
case h
r n : ℕ
h : r < n / 2
⊢ r * 2 < n
[PROOFSTEP]
exact lt_of_lt_of_le (mul_lt_mul_of_pos_right h zero_lt_two) (n.div_mul_le_self 2)
[GOAL]
r n : ℕ
⊢ choose n r ≤ choose n (n / 2)
[PROOFSTEP]
cases' le_or_gt r n with b b
[GOAL]
case inl
r n : ℕ
b : r ≤ n
⊢ choose n r ≤ choose n (n / 2)
[PROOFSTEP]
cases' le_or_lt r (n / 2) with a h
[GOAL]
case inl.inl
r n : ℕ
b : r ≤ n
a : r ≤ n / 2
⊢ choose n r ≤ choose n (n / 2)
[PROOFSTEP]
apply choose_le_middle_of_le_half_left a
[GOAL]
case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ choose n r ≤ choose n (n / 2)
[PROOFSTEP]
rw [← choose_symm b]
[GOAL]
case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ choose n (n - r) ≤ choose n (n / 2)
[PROOFSTEP]
apply choose_le_middle_of_le_half_left
[GOAL]
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n - r ≤ n / 2
[PROOFSTEP]
rw [div_lt_iff_lt_mul' zero_lt_two] at h 
[GOAL]
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n < r * 2
⊢ n - r ≤ n / 2
[PROOFSTEP]
rw [le_div_iff_mul_le' zero_lt_two, tsub_mul, tsub_le_iff_tsub_le, mul_two, add_tsub_cancel_right]
[GOAL]
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n < r * 2
⊢ n ≤ r * 2
[PROOFSTEP]
exact le_of_lt h
[GOAL]
case inr
r n : ℕ
b : r > n
⊢ choose n r ≤ choose n (n / 2)
[PROOFSTEP]
rw [choose_eq_zero_of_lt b]
[GOAL]
case inr
r n : ℕ
b : r > n
⊢ 0 ≤ choose n (n / 2)
[PROOFSTEP]
apply zero_le
[GOAL]
a c : ℕ
⊢ choose a c ≤ choose (succ a) c
[PROOFSTEP]
cases c
[GOAL]
case zero
a : ℕ
⊢ choose a zero ≤ choose (succ a) zero
[PROOFSTEP]
simp [Nat.choose_succ_succ]
[GOAL]
case succ
a n✝ : ℕ
⊢ choose a (succ n✝) ≤ choose (succ a) (succ n✝)
[PROOFSTEP]
simp [Nat.choose_succ_succ]
[GOAL]
a b c : ℕ
⊢ choose a c ≤ choose (a + b) c
[PROOFSTEP]
induction' b with b_n b_ih
[GOAL]
case zero
a c : ℕ
⊢ choose a c ≤ choose (a + zero) c
[PROOFSTEP]
simp
[GOAL]
case succ
a c b_n : ℕ
b_ih : choose a c ≤ choose (a + b_n) c
⊢ choose a c ≤ choose (a + succ b_n) c
[PROOFSTEP]
exact le_trans b_ih (choose_le_succ (a + b_n) c)
[GOAL]
n : ℕ
⊢ multichoose n 0 = 1
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ multichoose zero 0 = 1
[PROOFSTEP]
simp [multichoose]
[GOAL]
case succ
n✝ : ℕ
⊢ multichoose (succ n✝) 0 = 1
[PROOFSTEP]
simp [multichoose]
[GOAL]
k : ℕ
⊢ multichoose 0 (k + 1) = 0
[PROOFSTEP]
simp [multichoose]
[GOAL]
n k : ℕ
⊢ multichoose (n + 1) (k + 1) = multichoose n (k + 1) + multichoose (n + 1) k
[PROOFSTEP]
simp [multichoose]
[GOAL]
k : ℕ
⊢ multichoose 1 k = 1
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
⊢ multichoose 1 zero = 1
[PROOFSTEP]
simp
[GOAL]
case succ
k : ℕ
IH : multichoose 1 k = 1
⊢ multichoose 1 (succ k) = 1
[PROOFSTEP]
simp [multichoose_succ_succ 0 k, IH]
[GOAL]
k : ℕ
⊢ multichoose 2 k = k + 1
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
⊢ multichoose 2 zero = zero + 1
[PROOFSTEP]
simp
[GOAL]
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 2 (succ k) = succ k + 1
[PROOFSTEP]
rw [multichoose, IH]
[GOAL]
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (k + 1) = succ k + 1
[PROOFSTEP]
simp [add_comm, succ_eq_add_one]
[GOAL]
n : ℕ
⊢ multichoose n 1 = n
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
⊢ multichoose zero 1 = zero
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
IH : multichoose n 1 = n
⊢ multichoose (succ n) 1 = succ n
[PROOFSTEP]
simp [multichoose_succ_succ n 0, IH]
[GOAL]
x✝ : ℕ
⊢ multichoose x✝ 0 = choose (x✝ + 0 - 1) 0
[PROOFSTEP]
simp
[GOAL]
k : ℕ
⊢ multichoose 0 (k + 1) = choose (0 + (k + 1) - 1) (k + 1)
[PROOFSTEP]
simp
[GOAL]
n k : ℕ
⊢ multichoose (n + 1) (k + 1) = choose (n + 1 + (k + 1) - 1) (k + 1)
[PROOFSTEP]
have : n + (k + 1) < (n + 1) + (k + 1) := add_lt_add_right (Nat.lt_succ_self _) _
[GOAL]
n k : ℕ
this : n + (k + 1) < n + 1 + (k + 1)
⊢ multichoose (n + 1) (k + 1) = choose (n + 1 + (k + 1) - 1) (k + 1)
[PROOFSTEP]
have : (n + 1) + k < (n + 1) + (k + 1) := add_lt_add_left (Nat.lt_succ_self _) _
[GOAL]
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ multichoose (n + 1) (k + 1) = choose (n + 1 + (k + 1) - 1) (k + 1)
[PROOFSTEP]
erw [multichoose_succ_succ, add_comm, Nat.succ_add_sub_one, ← add_assoc, Nat.choose_succ_succ]
[GOAL]
n k : ℕ
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ multichoose (n + 1) k + multichoose n (k + 1) = choose (n + k) k + choose (n + k) (succ k)
[PROOFSTEP]
simp [multichoose_eq n (k + 1), multichoose_eq (n + 1) k]
[GOAL]
n k : ℕ
x✝ :
  ∀ (y : (_ : ℕ) ×' ℕ),
    (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 y
        { fst := succ n, snd := succ k } →
      multichoose y.1 y.2 = choose (y.1 + y.2 - 1) y.2
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 { fst := n + 1, snd := k }
    { fst := succ n, snd := succ k }
[PROOFSTEP]
{assumption
}
[GOAL]
n k : ℕ
x✝ :
  ∀ (y : (_ : ℕ) ×' ℕ),
    (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 y
        { fst := succ n, snd := succ k } →
      multichoose y.1 y.2 = choose (y.1 + y.2 - 1) y.2
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 { fst := n + 1, snd := k }
    { fst := succ n, snd := succ k }
[PROOFSTEP]
assumption
[GOAL]
n k : ℕ
x✝ :
  ∀ (y : (_ : ℕ) ×' ℕ),
    (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 y
        { fst := succ n, snd := succ k } →
      multichoose y.1 y.2 = choose (y.1 + y.2 - 1) y.2
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 { fst := n, snd := k + 1 }
    { fst := succ n, snd := succ k }
[PROOFSTEP]
{assumption
}
[GOAL]
n k : ℕ
x✝ :
  ∀ (y : (_ : ℕ) ×' ℕ),
    (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 y
        { fst := succ n, snd := succ k } →
      multichoose y.1 y.2 = choose (y.1 + y.2 - 1) y.2
this✝ : n + (k + 1) < n + 1 + (k + 1)
this : n + 1 + k < n + 1 + (k + 1)
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => a + snd) instWellFoundedRelation).1 { fst := n, snd := k + 1 }
    { fst := succ n, snd := succ k }
[PROOFSTEP]
assumption
