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

State before:
⊢ 1.098 < log 3
Tactic:
rw [Real.lt_log_iff_exp_lt (by norm_num)]
State after:
⊢ exp 1.098 < 3

State before:
⊢ exp 1.098 < 3
Tactic:
norm_num
State after:
⊢ (549 / 500).exp < 3

State before:
⊢ (549 / 500).exp < 3
Tactic:
exact exp_div_lt
State after:
no goals

State before:
⊢ 0 < 3
Tactic:
norm_num
State after:
no goals