Theorem: Real.exp_forth_lt_four_thirds (Ray/Misc/Bounds.lean)

State before:
⊢ (1 / 4).exp < 4 / 3
Tactic:
rw [←Real.exp_one_rpow, one_div, ←@Real.pow_rpow_inv_natCast (4/3) 4 (by norm_num) (by norm_num)]
State after:
⊢ rexp 1 ^ 4⁻¹ < ((4 / 3) ^ 4) ^ (↑4)⁻¹

State before:
⊢ rexp 1 ^ 4⁻¹ < ((4 / 3) ^ 4) ^ (↑4)⁻¹
Tactic:
refine Real.rpow_lt_rpow (Real.exp_pos _).le ?_ (by norm_num)
State after:
⊢ rexp 1 < (4 / 3) ^ 4

State before:
⊢ rexp 1 < (4 / 3) ^ 4
Tactic:
exact _root_.trans Real.exp_one_lt_d9 (by norm_num)
State after:
no goals

State before:
⊢ 0 ≤ 4 / 3
Tactic:
norm_num
State after:
no goals

State before:
⊢ 4 ≠ 0
Tactic:
norm_num
State after:
no goals

State before:
⊢ 0 < 4⁻¹
Tactic:
norm_num
State after:
no goals

State before:
⊢ 2.7182818286 < (4 / 3) ^ 4
Tactic:
norm_num
State after:
no goals