Theorem: le_log_abs_z (Ray/Dynamics/Multibrot/Iterates.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ 1.0986 ≤ (Complex.abs z).log
Tactic:
rw [Real.le_log_iff_exp_le (by linarith)]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ exp 1.0986 ≤ Complex.abs z

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ exp 1.0986 ≤ Complex.abs z
Tactic:
refine le_trans ?_ z3
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ exp 1.0986 ≤ 3

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ exp 1.0986 ≤ 3
Tactic:
norm_num
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ (5493 / 5000).exp ≤ 3

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ (5493 / 5000).exp ≤ 3
Tactic:
exact (exp_div_lt).le
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ 0 < Complex.abs z
Tactic:
linarith
State after:
no goals