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

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

State before:
⊢ exp 0.693 < 2
Tactic:
norm_num
State after:
⊢ (693 / 1000).exp < 2

State before:
⊢ (693 / 1000).exp < 2
Tactic:
exact exp_div_lt
State after:
no goals

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