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

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

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

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

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

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

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

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

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