-- Mathlib/Analysis/SpecialFunctions/Exp.lean
/-- The complex exponential function is uniformly continuous on left half planes. -/
lemma UniformContinuousOn.cexp (a : ℝ) : UniformContinuousOn exp {x : ℂ | x.re ≤ a}

Proof state:
case intro
a ε : ℝ
hε : ε > 0
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
hya : ‖cexp y‖ ≤ Real.exp a
⊢ ‖(cexp (x - y) - 1) * cexp y‖ < ε

Tactic:
simp only [gt_iff_lt, dist_zero_right, Set.mem_setOf_eq, norm_mul, Complex.norm_exp] at *

Result:
case intro
a ε : ℝ
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
x : ℂ
a✝ : x.re ≤ a
y : ℂ
hy : y.re ≤ a
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
hε : 0 < ε
hδ : 0 < δ ∧ ∀ ⦃y : ℂ⦄, ‖y‖ < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
hya : Real.exp y.re ≤ Real.exp a
⊢ ‖cexp (x - y) - 1‖ * Real.exp y.re < ε

Proof state:
a : ℝ
this : ∀ (a : ℂ), ∀ ε > 0, ∀ᶠ (x : ℂ) in 𝓝 a, dist ((cexp - 1) x) ((cexp - 1) a) < ε
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
simp only [gt_iff_lt, Pi.sub_apply, Pi.one_apply, dist_sub_eq_dist_add_right,
  sub_add_cancel] at this

Result:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
⊢ ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Proof state:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
⊢ ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
have ha : 0 < ε / (2 * Real.exp a) := by positivity

Result:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
⊢ ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Proof state:
a ε : ℝ
hε : ε > 0
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
⊢ ‖cexp y‖ ≤ Real.exp a

Tactic:
simp only [norm_exp, Real.exp_le_exp]

Result:
a ε : ℝ
hε : ε > 0
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
⊢ y.re ≤ a

Proof state:
case intro
a ε : ℝ
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
x : ℂ
a✝ : x.re ≤ a
y : ℂ
hy : y.re ≤ a
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
hε : 0 < ε
hδ : 0 < δ ∧ ∀ ⦃y : ℂ⦄, ‖y‖ < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
hya : Real.exp y.re ≤ Real.exp a
hrr : ε / (2 * Real.exp a) * Real.exp a = ε / 2
⊢ ε / 2 < ε

Tactic:
exact div_two_lt_of_pos hε

Result:
no goals

Proof state:
case intro
a ε : ℝ
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
x : ℂ
a✝ : x.re ≤ a
y : ℂ
hy : y.re ≤ a
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
hε : 0 < ε
hδ : 0 < δ ∧ ∀ ⦃y : ℂ⦄, ‖y‖ < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
hya : Real.exp y.re ≤ Real.exp a
hrr : ε / (2 * Real.exp a) * Real.exp a = ε / 2
⊢ ε / (2 * Real.exp a) * Real.exp a < ε

Tactic:
rw [hrr]

Result:
case intro
a ε : ℝ
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
x : ℂ
a✝ : x.re ≤ a
y : ℂ
hy : y.re ≤ a
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
hε : 0 < ε
hδ : 0 < δ ∧ ∀ ⦃y : ℂ⦄, ‖y‖ < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
hya : Real.exp y.re ≤ Real.exp a
hrr : ε / (2 * Real.exp a) * Real.exp a = ε / 2
⊢ ε / 2 < ε

Proof state:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
⊢ cexp x - cexp y = cexp (y + (x - y)) - cexp y

Tactic:
ring_nf

Result:
no goals

Proof state:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
H : ∀ᶠ (x : ℂ) in 𝓝 0, dist (cexp x) (cexp 0) < ε / (2 * Real.exp a)
⊢ ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
rw [Metric.eventually_nhds_iff] at H

Result:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
H : ∃ ε_1 > 0, ∀ ⦃y : ℂ⦄, dist y 0 < ε_1 → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)
⊢ ∃ δ > 0, ∀ x ∈ {x | x.re ≤ a}, ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Proof state:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
⊢ 0 < ε / (2 * Real.exp a)

Tactic:
positivity

Result:
no goals

Proof state:
case intro
a ε : ℝ
hε : ε > 0
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
⊢ ‖cexp x - cexp y‖ < ε

Tactic:
rw [this, mul_comm]

Result:
case intro
a ε : ℝ
hε : ε > 0
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
hy : y ∈ {x | x.re ≤ a}
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
⊢ ‖(cexp (x - y) - 1) * cexp y‖ < ε

Proof state:
case intro
a ε : ℝ
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
x : ℂ
a✝ : x.re ≤ a
y : ℂ
hy : y.re ≤ a
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
hε : 0 < ε
hδ : 0 < δ ∧ ∀ ⦃y : ℂ⦄, ‖y‖ < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
hya : Real.exp y.re ≤ Real.exp a
⊢ ‖cexp (x - y) - 1‖ * Real.exp y.re < ε

Tactic:
apply lt_of_le_of_lt (mul_le_mul h3.le hya (Real.exp_nonneg y.re) (le_of_lt ha))

Result:
case intro
a ε : ℝ
this✝ : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
x : ℂ
a✝ : x.re ≤ a
y : ℂ
hy : y.re ≤ a
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
hε : 0 < ε
hδ : 0 < δ ∧ ∀ ⦃y : ℂ⦄, ‖y‖ < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
hya : Real.exp y.re ≤ Real.exp a
⊢ ε / (2 * Real.exp a) * Real.exp a < ε