Theorem: five_eights_pow_lt (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
⊢ r > 0 → n ≠ 0 → (5 / 8) ^ n * r < r
Tactic:
intro rp np
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
np : n ≠ 0
⊢ (5 / 8) ^ n * r < r

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
np : n ≠ 0
⊢ (5 / 8) ^ n * r < r
Tactic:
have h : (5 / 8 : ℝ) ^ n < 1 := pow_lt_one (by norm_num) (by norm_num) np
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
np : n ≠ 0
h : (5 / 8) ^ n < 1
⊢ (5 / 8) ^ n * r < r

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
np : n ≠ 0
h : (5 / 8) ^ n < 1
⊢ (5 / 8) ^ n * r < r
Tactic:
exact lt_of_lt_of_le (mul_lt_mul_of_pos_right h rp) (by simp only [one_mul, le_refl])
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
np : n ≠ 0
⊢ 0 ≤ 5 / 8
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
np : n ≠ 0
⊢ 5 / 8 < 1
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
np : n ≠ 0
h : (5 / 8) ^ n < 1
⊢ 1 * r ≤ r
Tactic:
simp only [one_mul, le_refl]
State after:
no goals