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

State before:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ -(1 - 1 / x).log < 0.41
Tactic:
rw [neg_lt, Real.lt_log_iff_exp_lt (lt_of_lt_of_le (by norm_num) le)]
State after:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ (-0.41).exp < 1 - 1 / x

State before:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ (-0.41).exp < 1 - 1 / x
Tactic:
refine lt_of_lt_of_le ?_ le
State after:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ (-0.41).exp < 2 / 3

State before:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ (-0.41).exp < 2 / 3
Tactic:
norm_num
State after:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ (-(41 / 100)).exp < 2 / 3

State before:
x : ℝ
x3 : 3 ≤ x
le : 2 / 3 ≤ 1 - 1 / x
⊢ (-(41 / 100)).exp < 2 / 3
Tactic:
exact exp_neg_div_lt
State after:
no goals

State before:
x : ℝ
x3 : 3 ≤ x
⊢ 2 / 3 ≤ 1 - 1 / x
Tactic:
rw [le_tsub_iff_le_tsub (by norm_num), one_div, inv_le (by positivity)]
State after:
x : ℝ
x3 : 3 ≤ x
⊢ (1 - 2 / 3)⁻¹ ≤ x

x : ℝ
x3 : 3 ≤ x
⊢ 0 < 1 - 2 / 3

x : ℝ
x3 : 3 ≤ x
⊢ 1 / x ≤ 1

State before:
x : ℝ
x3 : 3 ≤ x
⊢ 2 / 3 ≤ 1
Tactic:
norm_num
State after:
no goals

State before:
x : ℝ
x3 : 3 ≤ x
⊢ 0 < x
Tactic:
positivity
State after:
no goals

State before:
x : ℝ
x3 : 3 ≤ x
⊢ (1 - 2 / 3)⁻¹ ≤ x
Tactic:
exact le_trans (by norm_num) x3
State after:
no goals

State before:
x : ℝ
x3 : 3 ≤ x
⊢ (1 - 2 / 3)⁻¹ ≤ 3
Tactic:
norm_num
State after:
no goals

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

State before:
x : ℝ
x3 : 3 ≤ x
⊢ 1 / x ≤ 1
Tactic:
rw [one_div, inv_le_one_iff]
State after:
x : ℝ
x3 : 3 ≤ x
⊢ x ≤ 0 ∨ 1 ≤ x

State before:
x : ℝ
x3 : 3 ≤ x
⊢ x ≤ 0 ∨ 1 ≤ x
Tactic:
right
State after:
case h
x : ℝ
x3 : 3 ≤ x
⊢ 1 ≤ x

State before:
case h
x : ℝ
x3 : 3 ≤ x
⊢ 1 ≤ x
Tactic:
exact le_trans (by norm_num) x3
State after:
no goals

State before:
x : ℝ
x3 : 3 ≤ x
⊢ 1 ≤ 3
Tactic:
norm_num
State after:
no goals

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