Theorem: Nat.choose_le_two_pow (ExponentialRamsey/Prereq/Mathlib/Data/Nat/Choose/Sum.lean)

State before:
n k : ℕ
⊢ choose n k ≤ 2 ^ n
Tactic:
cases' le_or_lt k n with h h
State after:
case inl
n k : ℕ
h : k ≤ n
⊢ choose n k ≤ 2 ^ n

case inr
n k : ℕ
h : n < k
⊢ choose n k ≤ 2 ^ n

State before:
case inr
n k : ℕ
h : n < k
⊢ choose n k ≤ 2 ^ n
Tactic:
rw [choose_eq_zero_of_lt h]
State after:
case inr
n k : ℕ
h : n < k
⊢ 0 ≤ 2 ^ n

State before:
case inr
n k : ℕ
h : n < k
⊢ 0 ≤ 2 ^ n
Tactic:
exact zero_le'
State after:
no goals

State before:
case inl
n k : ℕ
h : k ≤ n
⊢ choose n k ≤ 2 ^ n
Tactic:
rw [← sum_range_choose n]
State after:
case inl
n k : ℕ
h : k ≤ n
⊢ choose n k ≤ Finset.sum (range (n + 1)) fun m => choose n m

State before:
case inl
n k : ℕ
h : k ≤ n
⊢ choose n k ≤ Finset.sum (range (n + 1)) fun m => choose n m
Tactic:
refine' single_le_sum (fun _ _ => zero_le') _
State after:
case inl
n k : ℕ
h : k ≤ n
⊢ k ∈ range (n + 1)

State before:
case inl
n k : ℕ
h : k ≤ n
⊢ k ∈ range (n + 1)
Tactic:
rwa [mem_range_succ_iff]
State after:
no goals