Theorem: pow_small (Ray/Misc/Bounds.lean)

State before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
⊢ Complex.abs (z ^ w - 1) ≤ 4 * Complex.abs (z - 1) * Complex.abs w
Tactic:
generalize zw : z - 1 = z1
State after:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
⊢ Complex.abs (z ^ w - 1) ≤ 4 * Complex.abs z1 * Complex.abs w

State before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
⊢ Complex.abs (z ^ w - 1) ≤ 4 * Complex.abs z1 * Complex.abs w
Tactic:
have wz : z = 1 + z1 := by rw [← zw]; ring
State after:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs (z ^ w - 1) ≤ 4 * Complex.abs z1 * Complex.abs w

State before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs (z ^ w - 1) ≤ 4 * Complex.abs z1 * Complex.abs w
Tactic:
rw [wz]
State after:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs ((1 + z1) ^ w - 1) ≤ 4 * Complex.abs z1 * Complex.abs w

State before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs ((1 + z1) ^ w - 1) ≤ 4 * Complex.abs z1 * Complex.abs w
Tactic:
refine pow1p_small ?_ ws
State after:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs z1 ≤ 1 / 2

State before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs z1 ≤ 1 / 2
Tactic:
rw [← zw]
State after:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs (z - 1) ≤ 1 / 2

State before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
wz : z = 1 + z1
⊢ Complex.abs (z - 1) ≤ 1 / 2
Tactic:
assumption
State after:
no goals

State before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
⊢ z = 1 + z1
Tactic:
rw [← zw]
State after:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
⊢ z = 1 + (z - 1)

State before:
z w : ℂ
zs : Complex.abs (z - 1) ≤ 1 / 2
ws : Complex.abs w ≤ 1
z1 : ℂ
zw : z - 1 = z1
⊢ z = 1 + (z - 1)
Tactic:
ring
State after:
no goals