Theorem: exp_factorial_bound_of_ne_zero (ExponentialRamsey/Prereq/Mathlib/Analysis/SpecialFunctions/ExplicitStirling.lean)

State before:
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < rexp x
Tactic:
rw [exp_eq_exp_ℝ]
State after:
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < _root_.exp ℝ x

State before:
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < _root_.exp ℝ x
Tactic:
refine (sum_le_hasSum {n, 0} ?_ (expSeries_div_hasSum_exp ℝ x)).trans_lt' ?_
State after:
case refine_1
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ ∀ i ∉ {n, 0}, 0 ≤ x ^ i / ↑i !

case refine_2
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < Finset.sum {n, 0} fun i => x ^ i / ↑i !

State before:
case refine_2
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < Finset.sum {n, 0} fun i => x ^ i / ↑i !
Tactic:
rw [sum_pair hn]
State after:
case refine_2
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < x ^ n / ↑n ! + x ^ 0 / ↑0!

State before:
case refine_2
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < x ^ n / ↑n ! + x ^ 0 / ↑0!
Tactic:
simp
State after:
no goals

State before:
case refine_1
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ ∀ i ∉ {n, 0}, 0 ≤ x ^ i / ↑i !
Tactic:
intro x _
State after:
case refine_1
n : ℕ
x✝ : ℝ
hx : 0 ≤ x✝
hn : n ≠ 0
x : ℕ
a✝ : x ∉ {n, 0}
⊢ 0 ≤ x✝ ^ x / ↑x !

State before:
case refine_1
n : ℕ
x✝ : ℝ
hx : 0 ≤ x✝
hn : n ≠ 0
x : ℕ
a✝ : x ∉ {n, 0}
⊢ 0 ≤ x✝ ^ x / ↑x !
Tactic:
positivity
State after:
no goals