Theorem: Nat.choose_le_pow_left (ExponentialRamsey/Prereq/Mathlib/Data/Nat/Choose/Basic.lean)

State before:
s t : ℕ
⊢ choose s t ≤ (s + 1 - t) ^ t
Tactic:
cases' le_or_lt t s with h h
State after:
case inl
s t : ℕ
h : t ≤ s
⊢ choose s t ≤ (s + 1 - t) ^ t

case inr
s t : ℕ
h : s < t
⊢ choose s t ≤ (s + 1 - t) ^ t

State before:
case inr
s t : ℕ
h : s < t
⊢ choose s t ≤ (s + 1 - t) ^ t
Tactic:
rw [choose_eq_zero_of_lt h]
State after:
case inr
s t : ℕ
h : s < t
⊢ 0 ≤ (s + 1 - t) ^ t

State before:
case inr
s t : ℕ
h : s < t
⊢ 0 ≤ (s + 1 - t) ^ t
Tactic:
exact zero_le'
State after:
no goals

State before:
case inl
s t : ℕ
h : t ≤ s
⊢ choose s t ≤ (s + 1 - t) ^ t
Tactic:
obtain ⟨s, rfl⟩ := exists_add_of_le h
State after:
case inl.intro
t s : ℕ
h : t ≤ t + s
⊢ choose (t + s) t ≤ (t + s + 1 - t) ^ t

State before:
case inl.intro
t s : ℕ
h : t ≤ t + s
⊢ choose (t + s) t ≤ (t + s + 1 - t) ^ t
Tactic:
refine (choose_add_le_pow_left t s).trans ?_
State after:
case inl.intro
t s : ℕ
h : t ≤ t + s
⊢ (s + 1) ^ t ≤ (t + s + 1 - t) ^ t

State before:
case inl.intro
t s : ℕ
h : t ≤ t + s
⊢ (s + 1) ^ t ≤ (t + s + 1 - t) ^ t
Tactic:
rw [add_assoc, Nat.add_sub_cancel_left]
State after:
no goals