Theorem: Real.abs_log_one_add_le (Ray/Dynamics/Multibrot/Log1p.lean)

State before:
x : ℝ
x1 : |x| < 1
⊢ |(1 + x).log| ≤ -(1 - |x|).log
Tactic:
have h := Complex.abs_log_one_add_le (z := x) ?_
State after:
case refine_2
x : ℝ
x1 : |x| < 1
h : Complex.abs (1 + ↑x).log ≤ -(1 - Complex.abs ↑x).log
⊢ |(1 + x).log| ≤ -(1 - |x|).log

case refine_1
x : ℝ
x1 : |x| < 1
⊢ Complex.abs ↑x < 1

State before:
case refine_2
x : ℝ
x1 : |x| < 1
h : Complex.abs (1 + ↑x).log ≤ -(1 - Complex.abs ↑x).log
⊢ |(1 + x).log| ≤ -(1 - |x|).log
Tactic:
rw [←Complex.ofReal_one, ←Complex.ofReal_add, ←Complex.ofReal_log, Complex.abs_ofReal,
  Complex.abs_ofReal] at h
State after:
case refine_2
x : ℝ
x1 : |x| < 1
h : |(1 + x).log| ≤ -(1 - |x|).log
⊢ |(1 + x).log| ≤ -(1 - |x|).log

case refine_2
x : ℝ
x1 : |x| < 1
h : Complex.abs (↑(1 + x)).log ≤ -(1 - Complex.abs ↑x).log
⊢ 0 ≤ 1 + x

State before:
case refine_2
x : ℝ
x1 : |x| < 1
h : |(1 + x).log| ≤ -(1 - |x|).log
⊢ |(1 + x).log| ≤ -(1 - |x|).log
Tactic:
exact h
State after:
no goals

State before:
case refine_2
x : ℝ
x1 : |x| < 1
h : Complex.abs (↑(1 + x)).log ≤ -(1 - Complex.abs ↑x).log
⊢ 0 ≤ 1 + x
Tactic:
simp only [abs_lt] at x1
State after:
case refine_2
x : ℝ
h : Complex.abs (↑(1 + x)).log ≤ -(1 - Complex.abs ↑x).log
x1 : -1 < x ∧ x < 1
⊢ 0 ≤ 1 + x

State before:
case refine_2
x : ℝ
h : Complex.abs (↑(1 + x)).log ≤ -(1 - Complex.abs ↑x).log
x1 : -1 < x ∧ x < 1
⊢ 0 ≤ 1 + x
Tactic:
linarith
State after:
no goals

State before:
case refine_1
x : ℝ
x1 : |x| < 1
⊢ Complex.abs ↑x < 1
Tactic:
simpa only [Complex.abs_ofReal]
State after:
no goals