R : Type ?u.162350
n : ℕ
t : choose (2 * n + 1) n ≤ ∑ i in range (n + 1), choose (2 * n + 1) i
⊢ choose (2 * n + 1) n ≤ 4 ^ n
R : Type ?u.162350
n : ℕ
⊢ choose (2 * n + 1) n ≤ 4 ^ n
have t : choose (2 * n + 1) n ≤ ∑ i in range (n + 1), choose (2 * n + 1) i :=
  single_le_sum (fun x _ ↦ by linarith) (self_mem_range_succ n)
no goals
R : Type ?u.162350
n : ℕ
t : choose (2 * n + 1) n ≤ ∑ i in range (n + 1), choose (2 * n + 1) i
⊢ choose (2 * n + 1) n ≤ 4 ^ n
simpa [sum_range_choose_halfway n] using t
no goals
R : Type ?u.162350
n x : ℕ
x✝ : x ∈ range (n + 1)
⊢ 0 ≤ choose (2 * n + 1) x
linarith