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

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

State before:
⊢ 4 < exp 1.387
Tactic:
norm_num
State after:
⊢ 4 < (1387 / 1000).exp

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

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