Theorem: exp_ofNat_lt (Ray/Dynamics/Multibrot/Specific.lean)

State before:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
h0 : autoParam (2.7182818286 ^ a < b) _auto✝
⊢ (↑a).exp < b
Tactic:
rw [←Real.exp_one_pow a]
State after:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
h0 : autoParam (2.7182818286 ^ a < b) _auto✝
⊢ exp 1 ^ a < b

State before:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
h0 : autoParam (2.7182818286 ^ a < b) _auto✝
⊢ exp 1 ^ a < b
Tactic:
exact _root_.trans (pow_lt_pow_left Real.exp_one_lt_d9 (Real.exp_nonneg _) a0) h0
State after:
no goals