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

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

State before:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
h0 : autoParam (b < 2.7182818283 ^ a) _auto✝
⊢ b < exp 1 ^ a
Tactic:
exact _root_.trans h0 (pow_lt_pow_left Real.exp_one_gt_d9 (by norm_num) a0)
State after:
no goals

State before:
a : ℕ
b : ℝ
a0 : autoParam (a ≠ 0) _auto✝
h0 : autoParam (b < 2.7182818283 ^ a) _auto✝
⊢ 0 ≤ 2.7182818283
Tactic:
norm_num
State after:
no goals