case inl
r n : ℕ
b : r ≤ n
⊢ choose n r ≤ choose n (n / 2)

case inr
r n : ℕ
b : r > n
⊢ choose n r ≤ choose n (n / 2)
r n : ℕ
⊢ choose n r ≤ choose n (n / 2)
cases' le_or_gt r n with b b
case inl.inl
r n : ℕ
b : r ≤ n
a : r ≤ n / 2
⊢ choose n r ≤ choose n (n / 2)

case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ choose n r ≤ choose n (n / 2)
case inl
r n : ℕ
b : r ≤ n
⊢ choose n r ≤ choose n (n / 2)
cases' le_or_lt r (n / 2) with a h
no goals
case inl.inl
r n : ℕ
b : r ≤ n
a : r ≤ n / 2
⊢ choose n r ≤ choose n (n / 2)
apply choose_le_middle_of_le_half_left a
case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ choose n (n - r) ≤ choose n (n / 2)
case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ choose n r ≤ choose n (n / 2)
rw [← choose_symm b]
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n - r ≤ n / 2
case inl.inr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ choose n (n - r) ≤ choose n (n / 2)
apply choose_le_middle_of_le_half_left
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n < r * 2
⊢ n - r ≤ n / 2
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n / 2 < r
⊢ n - r ≤ n / 2
rw [div_lt_iff_lt_mul' zero_lt_two] at h
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n < r * 2
⊢ n ≤ r * 2
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n < r * 2
⊢ n - r ≤ n / 2
rw [le_div_iff_mul_le' zero_lt_two, tsub_mul, tsub_le_iff_tsub_le, mul_two,
  add_tsub_cancel_right]
no goals
case inl.inr.hr
r n : ℕ
b : r ≤ n
h : n < r * 2
⊢ n ≤ r * 2
exact le_of_lt h
case inr
r n : ℕ
b : r > n
⊢ 0 ≤ choose n (n / 2)
case inr
r n : ℕ
b : r > n
⊢ choose n r ≤ choose n (n / 2)
rw [choose_eq_zero_of_lt b]
no goals
case inr
r n : ℕ
b : r > n
⊢ 0 ≤ choose n (n / 2)
apply zero_le