case e_a
z✝ y x✝ : ℝ
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ exp (x + z) - exp x - z * exp x = exp x * (exp z - 1 - z)
z✝ y x✝ : ℝ
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖exp (x + z) - exp x - z * exp x‖ = ‖exp x * (exp z - 1 - z)‖
congr
case e_a
z✝ y x✝ : ℝ
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ exp x * exp z - exp x - z * exp x = exp x * (exp z - 1 - z)
case e_a
z✝ y x✝ : ℝ
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ exp (x + z) - exp x - z * exp x = exp x * (exp z - 1 - z)
rw [exp_add]
no goals
case e_a
z✝ y x✝ : ℝ
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ exp x * exp z - exp x - z * exp x = exp x * (exp z - 1 - z)
ring