Theorem: iter_large (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ (b - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
Tactic:
induction' n with n h
State after:
case zero
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (b - 1) ^ 0 * Complex.abs z ≤ Complex.abs ((f' d c)^[0] z)

case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs ((f' d c)^[n + 1] z)

State before:
case zero
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (b - 1) ^ 0 * Complex.abs z ≤ Complex.abs ((f' d c)^[0] z)
Tactic:
simp only [Nat.zero_eq, pow_zero, one_mul, Function.iterate_zero_apply, le_refl]
State after:
no goals

State before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs ((f' d c)^[n + 1] z)
Tactic:
simp only [Function.iterate_succ_apply']
State after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c ((f' d c)^[n] z))

State before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c ((f' d c)^[n] z))
Tactic:
generalize hw : (f' d c)^[n] z = w
State after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
w : ℂ
hw : (f' d c)^[n] z = w
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)

State before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs ((f' d c)^[n] z)
w : ℂ
hw : (f' d c)^[n] z = w
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Tactic:
rw [hw] at h
State after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
hw : (f' d c)^[n] z = w
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)

State before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
hw : (f' d c)^[n] z = w
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Tactic:
clear hw
State after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)

State before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Tactic:
have z1 : 1 ≤ abs z := le_trans (by norm_num) (le_trans b2 bz)
State after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)

State before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Tactic:
have b1 : 1 ≤ b - 1 := by linarith
State after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)

State before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Tactic:
have b0 : 0 ≤ b - 1 := by linarith
State after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)

State before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Tactic:
have nd : n + 1 ≤ n * d + 1 := by bound
State after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)

State before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Tactic:
calc abs (w ^ d + c)
  _ ≥ abs (w ^ d) - abs c := by bound
  _ = abs w ^ d - abs c := by rw [Complex.abs.map_pow]
  _ ≥ ((b-1) ^ n * abs z) ^ d - abs c := by bound
  _ = (b-1) ^ (n*d) * abs z ^ d - abs c := by rw [mul_pow, pow_mul]
  _ ≥ (b-1) ^ (n*d) * abs z ^ 2 - abs c := by bound
  _ = (b-1) ^ (n*d) * (abs z * abs z) - abs c := by rw [pow_two]
  _ ≥ (b-1) ^ (n*d) * (b * abs z) - abs c := by bound
  _ = (b-1) ^ (n*d) * (b-1) * abs z + ((b-1) ^ (n*d) * abs z - abs c) := by ring
  _ = (b-1) ^ (n*d + 1) * abs z + ((b-1) ^ (n * d) * abs z - abs c) := by rw [pow_succ]
  _ ≥ (b-1) ^ (n + 1) * abs z + (1 * abs z - abs c) := by bound
  _ = (b-1) ^ (n + 1) * abs z + (abs z - abs c) := by rw [one_mul]
  _ ≥ (b-1) ^ (n + 1) * abs z := by bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
⊢ 1 ≤ 2
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
⊢ 1 ≤ b - 1
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
⊢ 0 ≤ b - 1
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
⊢ n + 1 ≤ n * d + 1
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ Complex.abs (w ^ d + c) ≥ Complex.abs (w ^ d) - Complex.abs c
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ Complex.abs (w ^ d) - Complex.abs c = Complex.abs w ^ d - Complex.abs c
Tactic:
rw [Complex.abs.map_pow]
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ Complex.abs w ^ d - Complex.abs c ≥ ((b - 1) ^ n * Complex.abs z) ^ d - Complex.abs c
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ ((b - 1) ^ n * Complex.abs z) ^ d - Complex.abs c = (b - 1) ^ (n * d) * Complex.abs z ^ d - Complex.abs c
Tactic:
rw [mul_pow, pow_mul]
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n * d) * Complex.abs z ^ d - Complex.abs c ≥ (b - 1) ^ (n * d) * Complex.abs z ^ 2 - Complex.abs c
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n * d) * Complex.abs z ^ 2 - Complex.abs c =
    (b - 1) ^ (n * d) * (Complex.abs z * Complex.abs z) - Complex.abs c
Tactic:
rw [pow_two]
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n * d) * (Complex.abs z * Complex.abs z) - Complex.abs c ≥
    (b - 1) ^ (n * d) * (b * Complex.abs z) - Complex.abs c
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n * d) * (b * Complex.abs z) - Complex.abs c =
    (b - 1) ^ (n * d) * (b - 1) * Complex.abs z + ((b - 1) ^ (n * d) * Complex.abs z - Complex.abs c)
Tactic:
ring
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n * d) * (b - 1) * Complex.abs z + ((b - 1) ^ (n * d) * Complex.abs z - Complex.abs c) =
    (b - 1) ^ (n * d + 1) * Complex.abs z + ((b - 1) ^ (n * d) * Complex.abs z - Complex.abs c)
Tactic:
rw [pow_succ]
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n * d + 1) * Complex.abs z + ((b - 1) ^ (n * d) * Complex.abs z - Complex.abs c) ≥
    (b - 1) ^ (n + 1) * Complex.abs z + (1 * Complex.abs z - Complex.abs c)
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z + (1 * Complex.abs z - Complex.abs c) =
    (b - 1) ^ (n + 1) * Complex.abs z + (Complex.abs z - Complex.abs c)
Tactic:
rw [one_mul]
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z + (Complex.abs z - Complex.abs c) ≥ (b - 1) ^ (n + 1) * Complex.abs z
Tactic:
bound
State after:
no goals