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

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

State before:
⊢ exp 1.386 < 4
Tactic:
norm_num
State after:
⊢ (693 / 500).exp < 4

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

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