case inl
t : ℝ
ht' : t ≤ ↑0
⊢ (1 - t / ↑0) ^ 0 ≤ exp (-t)

case inr
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ (1 - t / ↑n) ^ n ≤ exp (-t)
n : ℕ
t : ℝ
ht' : t ≤ ↑n
⊢ (1 - t / ↑n) ^ n ≤ exp (-t)
rcases eq_or_ne n 0 with (rfl | hn)
case h.e'_3.h.e'_5
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ 1 - t / ↑n = -(t / ↑n) + 1

case h.e'_4
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ exp (-t) = exp (-(t / ↑n)) ^ n

case inr
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ 0 ≤ -(t / ↑n) + 1
case inr
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ (1 - t / ↑n) ^ n ≤ exp (-t)
convert pow_le_pow_of_le_left ?_ (add_one_le_exp (-(t / n))) n using 2
case inl
t : ℝ
ht' : t ≤ ↑0
⊢ t ≤ 0
case inl
t : ℝ
ht' : t ≤ ↑0
⊢ (1 - t / ↑0) ^ 0 ≤ exp (-t)
simp
no goals
case inl
t : ℝ
ht' : t ≤ ↑0
⊢ t ≤ 0
rwa [Nat.cast_zero] at ht'
no goals
case h.e'_3.h.e'_5
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ 1 - t / ↑n = -(t / ↑n) + 1
abel
case h.e'_4
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ exp (-t) = exp (↑n * -(t / ↑n))
case h.e'_4
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ exp (-t) = exp (-(t / ↑n)) ^ n
rw [← Real.exp_nat_mul]
case h.e'_4.e_x
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ -t = ↑n * -(t / ↑n)
case h.e'_4
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ exp (-t) = exp (↑n * -(t / ↑n))
congr 1
case h.e'_4.e_x
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ t * ↑n = ↑n * t
case h.e'_4.e_x
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ -t = ↑n * -(t / ↑n)
field_simp [(Nat.cast_ne_zero (R := ℝ)).mpr hn]
no goals
case h.e'_4.e_x
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ t * ↑n = ↑n * t
ring_nf
case inr
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ 0 < ↑n
case inr
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ 0 ≤ -(t / ↑n) + 1
rwa [add_comm, ← sub_eq_add_neg, sub_nonneg, div_le_one]
no goals
case inr
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ 0 < ↑n
positivity