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

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

State before:
⊢ 3 < exp 1.099
Tactic:
norm_num
State after:
⊢ 3 < (1099 / 1000).exp

State before:
⊢ 3 < (1099 / 1000).exp
Tactic:
exact lt_exp_div
State after:
no goals

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