x : ℝ
hx this : abs' x ≤ 1
⊢ abs' (exp x - 1) ≤ 2 * abs' x
x : ℝ
hx : abs' x ≤ 1
⊢ abs' (exp x - 1) ≤ 2 * abs' x
have : abs' x ≤ 1 := by exact_mod_cast hx
x : ℝ
hx this✝ : abs' x ≤ 1
this : ↑Complex.abs (Complex.exp ↑x - 1) ≤ 2 * ↑Complex.abs ↑x
⊢ abs' (exp x - 1) ≤ 2 * abs' x
x : ℝ
hx this : abs' x ≤ 1
⊢ abs' (exp x - 1) ≤ 2 * abs' x
have := Complex.abs_exp_sub_one_le (x := x) (by simpa using this)
x : ℝ
hx this✝ : abs' x ≤ 1
this : abs' (exp x - 1) ≤ 2 * abs' x
⊢ abs' (exp x - 1) ≤ 2 * abs' x
x : ℝ
hx this✝ : abs' x ≤ 1
this : ↑Complex.abs (Complex.exp ↑x - 1) ≤ 2 * ↑Complex.abs ↑x
⊢ abs' (exp x - 1) ≤ 2 * abs' x
rw [← ofReal_exp, ← ofReal_one, ← ofReal_sub, abs_ofReal, abs_ofReal] at this
no goals
x : ℝ
hx this✝ : abs' x ≤ 1
this : abs' (exp x - 1) ≤ 2 * abs' x
⊢ abs' (exp x - 1) ≤ 2 * abs' x
exact this
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ abs' x ≤ 1
exact_mod_cast hx
no goals
x : ℝ
hx this : abs' x ≤ 1
⊢ ↑Complex.abs ↑x ≤ 1
simpa using this