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

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

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ (5 / 8) ^ n * r ≤ r
Tactic:
trans (1:ℝ) ^ n * r
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ (5 / 8) ^ n * r ≤ 1 ^ n * r

f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ 1 ^ n * r ≤ r

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ (5 / 8) ^ n * r ≤ 1 ^ n * r

f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ 1 ^ n * r ≤ r
Tactic:
bound
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ 1 ^ n * r ≤ r

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ 1 ^ n * r ≤ r
Tactic:
simp only [one_pow, one_mul, le_refl]
State after:
no goals