Theorem: neg_log_one_sub_le_two (Ray/Dynamics/Multibrot/Log1p.lean)

State before:
x : ℝ
x2 : x ≤ 1 / 2
⊢ -(1 - x).log ≤ 2
Tactic:
apply le_trans (Real.neg_log_one_sub_mono x2 (by linarith)) ?_
State after:
x : ℝ
x2 : x ≤ 1 / 2
⊢ -(1 - 1 / 2).log ≤ 2

State before:
x : ℝ
x2 : x ≤ 1 / 2
⊢ -(1 - 1 / 2).log ≤ 2
Tactic:
rw [neg_le, Real.le_log_iff_exp_le]
State after:
x : ℝ
x2 : x ≤ 1 / 2
⊢ (-2).exp ≤ 1 - 1 / 2

x : ℝ
x2 : x ≤ 1 / 2
⊢ 0 < 1 - 1 / 2

State before:
x : ℝ
x2 : x ≤ 1 / 2
⊢ 1 / 2 < 1
Tactic:
linarith
State after:
no goals

State before:
x : ℝ
x2 : x ≤ 1 / 2
⊢ (-2).exp ≤ 1 - 1 / 2
Tactic:
exact (exp_neg_ofNat_lt).le
State after:
no goals

State before:
x : ℝ
x2 : x ≤ 1 / 2
⊢ 0 < 1 - 1 / 2
Tactic:
norm_num
State after:
no goals