Theorem: Real.log1p_small' (Ray/Misc/Bounds.lean)

State before:
x r : ℝ
r1 : r < 1
xr : |x| ≤ r
⊢ |(1 + x).log| ≤ 1 / (1 - r) * |x|
Tactic:
set z := (x : ℂ)
State after:
x r : ℝ
r1 : r < 1
xr : |x| ≤ r
z : ℂ := ↑x
⊢ |(1 + x).log| ≤ 1 / (1 - r) * |x|

State before:
x r : ℝ
r1 : r < 1
xr : |x| ≤ r
z : ℂ := ↑x
⊢ |(1 + x).log| ≤ 1 / (1 - r) * |x|
Tactic:
have zx : abs z = |x| := Complex.abs_ofReal _
State after:
x r : ℝ
r1 : r < 1
xr : |x| ≤ r
z : ℂ := ↑x
zx : Complex.abs z = |x|
⊢ |(1 + x).log| ≤ 1 / (1 - r) * |x|

State before:
x r : ℝ
r1 : r < 1
xr : |x| ≤ r
z : ℂ := ↑x
zx : Complex.abs z = |x|
⊢ |(1 + x).log| ≤ 1 / (1 - r) * |x|
Tactic:
simp only [← Complex.log_ofReal_re, ← zx] at xr ⊢
State after:
x r : ℝ
r1 : r < 1
z : ℂ := ↑x
zx : Complex.abs z = |x|
xr : Complex.abs z ≤ r
⊢ |(↑(1 + x)).log.re| ≤ 1 / (1 - r) * Complex.abs z

State before:
x r : ℝ
r1 : r < 1
z : ℂ := ↑x
zx : Complex.abs z = |x|
xr : Complex.abs z ≤ r
⊢ |(↑(1 + x)).log.re| ≤ 1 / (1 - r) * Complex.abs z
Tactic:
refine _root_.trans (_root_.trans (Complex.abs_re_le_abs _) ?_) (_root_.log1p_small' r1 xr)
State after:
x r : ℝ
r1 : r < 1
z : ℂ := ↑x
zx : Complex.abs z = |x|
xr : Complex.abs z ≤ r
⊢ Complex.abs (↑(1 + x)).log ≤ Complex.abs (1 + z).log

State before:
x r : ℝ
r1 : r < 1
z : ℂ := ↑x
zx : Complex.abs z = |x|
xr : Complex.abs z ≤ r
⊢ Complex.abs (↑(1 + x)).log ≤ Complex.abs (1 + z).log
Tactic:
simp only [Complex.ofReal_add, Complex.ofReal_one, le_refl]
State after:
no goals