awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
h₁ : 0 ≤ ‖cexp x‖
grw grw₁ : ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * (r * ‖y - x‖) ≤ ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * (r * ‖y - x‖)
⊢ ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * (r * ‖y - x‖)

Tactic:
grw [hyx_sq_le]
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
⊢ ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * (r * ‖y - x‖) = (1 + r) * ‖cexp x‖ * ‖y - x‖

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
y₁ : ‖cexp y - cexp x‖ = ‖cexp (x + (y - x)) - cexp x‖
y₂ : ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * (r * ‖y - x‖)
y₃ : ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * (r * ‖y - x‖) = (1 + r) * ‖cexp x‖ * ‖y - x‖
⊢ ‖cexp y - cexp x‖ ≤ (1 + r) * ‖cexp x‖ * ‖y - x‖

Tactic:
calc
    ‖exp y - exp x‖ = ‖exp (x + (y - x)) - exp x‖ := by nth_rw 1 [hy_eq]
    _ ≤ ‖y - x‖ * ‖exp x‖ + ‖exp x‖ * ‖y - x‖ ^ 2 := h_sq (y - x) (hyx.le.trans hr_le)
    _ ≤ ‖y - x‖ * ‖exp x‖ + ‖exp x‖ * (r * ‖y - x‖) := by grw [hyx_sq_le]
    _ = (1 + r) * ‖exp x‖ * ‖y - x‖ := by ring

Premises used: Norm.norm, HMul.hMul, HSub.hSub, LT.lt.le, HAdd.hAdd, Complex.exp, LE.le.trans, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
x y : ℂ
⊢ dist y x < 1 → dist (cexp y) (cexp x) ≤ 2 * ‖cexp x‖ * dist y x

Tactic:
simpa [dist_eq_norm, one_add_one_eq_two] using locally_lipschitz_exp zero_le_one le_rfl x y

Premises used: Complex.locally_lipschitz_exp, dist_eq_norm, le_rfl, one_add_one_eq_two, zero_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
s : Set ℂ
⊢ ContinuousOn cexp s

Tactic:
continuous_exp.continuousOn

Premises used: Continuous.continuousOn, Complex.continuous_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
inl :
  IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ cexp x - ∑ i ∈ Finset.range 0, x ^ i / (↑i ! : ℂ)) fun (x : ℂ) ↦
    HPow.hPow (β := ℕ) x 0
inr :
  ∀ (hn : 0 < n),
    IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)) fun (x : ℂ) ↦ x ^ n
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)) fun (x : ℂ) ↦ x ^ n

Tactic:
rcases eq_zero_or_pos n with rfl | hn

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ cexp x - ∑ i ∈ Finset.range 0, x ^ i / (↑i ! : ℂ)) fun (x : ℂ) ↦
    HPow.hPow (β := ℕ) x 0

Tactic:
simpa using continuous_exp.continuousAt.norm.isBoundedUnder_le

Premises used: Filter.Tendsto.isBoundedUnder_le, Complex.continuous_exp, Continuous.continuousAt, ContinuousAt.norm
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
hn : 0 < n
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)) fun (x : ℂ) ↦ x ^ n

Tactic:
.of_bound (n.succ / (n ! * n)) ?_

Premises used: HMul.hMul, HDiv.hDiv, Nat.cast, Nat.factorial, Asymptotics.IsBigO.of_bound, Nat.succ
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
hn : 0 < n
inr :
  ∀ᶠ (x : ℂ) in 𝓝 0,
    ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)‖ ≤
      (↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ) * ‖x ^ n‖
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)) fun (x : ℂ) ↦ x ^ n

Tactic:
refine .of_bound (n.succ / (n ! * n)) ?_
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
hn : 0 < n
inr :
  ∃ (i : ℝ),
    0 < i ∧
      ∀ ⦃x : ℂ⦄,
        Membership.mem (γ := Set ℂ) {y : ℂ | ‖y‖ < i} x →
          ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)‖ ≤
            (↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ) * ‖x ^ n‖
⊢ ∀ᶠ (x : ℂ) in 𝓝 0,
    ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)‖ ≤
      (↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ) * ‖x ^ n‖

Tactic:
rw [NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff]

Premises used: Filter.HasBasis.eventually_iff, NormedAddGroup.nhds_zero_basis_norm_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
hn : 0 < n
⊢ ∃ (i : ℝ),
    0 < i ∧
      ∀ ⦃x : ℂ⦄,
        Membership.mem (γ := Set ℂ) {y : ℂ | ‖y‖ < i} x →
          ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)‖ ≤
            (↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ) * ‖x ^ n‖

Tactic:
⟨1, one_pos, fun x hx ↦ ?_⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat, one_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
hn : 0 < n
inr :
  ∀ (x : ℂ) (hx : Membership.mem (γ := Set ℂ) {y : ℂ | ‖y‖ < 1} x),
    ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)‖ ≤
      (↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ) * ‖x ^ n‖
⊢ ∃ (i : ℝ),
    0 < i ∧
      ∀ ⦃x : ℂ⦄,
        Membership.mem (γ := Set ℂ) {y : ℂ | ‖y‖ < i} x →
          ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)‖ ≤
            (↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ) * ‖x ^ n‖

Tactic:
refine ⟨1, one_pos, fun x hx ↦ ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
hn : 0 < n
x : ℂ
hx : Membership.mem (γ := Set ℂ) {y : ℂ | ‖y‖ < 1} x
⊢ ‖cexp x - ∑ m ∈ Finset.range n, x ^ m / (↑m ! : ℂ)‖ ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ))⁻¹)

Tactic:
exp_bound hx.out.le hn

Premises used: Membership.mem.out, LT.lt.le, Complex.exp_bound
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
hn : 0 < n
x : ℂ
hx : Membership.mem (γ := Set ℂ) {y : ℂ | ‖y‖ < 1} x
h :
  (↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ) * ‖x ^ n‖ =
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ))⁻¹)
⊢ ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)‖ ≤ (↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ) * ‖x ^ n‖

Tactic:
convert! exp_bound hx.out.le hn using 1

Premises used: Membership.mem.out, LT.lt.le, Complex.exp_bound
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
hn : 0 < n
x : ℂ
hx : Membership.mem (γ := Set ℂ) {y : ℂ | ‖y‖ < 1} x
⊢ (↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ) * ‖x ^ n‖ =
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ))⁻¹)

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
⊢ IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ cexp x - ∑ i ∈ Finset.range (n + 1), x ^ i / (↑i ! : ℂ))
    fun (x : ℂ) ↦ x ^ n

Tactic:
(exp_sub_sum_range_isBigO_pow (n + 1)).trans_isLittleO <| isLittleO_pow_pow n.lt_succ_self

Premises used: Asymptotics.isLittleO_pow_pow, Nat.lt_succ_self, Complex.exp_sub_sum_range_isBigO_pow, HAdd.hAdd, Asymptotics.IsBigO.trans_isLittleO, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : α → ℂ
z : ℂ
hf : Tendsto f l (𝓝 z)
⊢ Tendsto (fun (x : α) ↦ cexp (f x)) l (𝓝 (cexp z))

Tactic:
(continuous_exp.tendsto _).comp hf

Premises used: Complex.continuous_exp, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℂ
s : Set α
x : α
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (Y := ℂ) (fun (y : α) ↦ cexp (f y)) s x

Tactic:
h.cexp

Premises used: ContinuousWithinAt, Filter.Tendsto.cexp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℂ
x : α
h : ContinuousAt f x
⊢ ContinuousAt (Y := ℂ) (fun (y : α) ↦ cexp (f y)) x

Tactic:
h.cexp

Premises used: ContinuousAt, Filter.Tendsto.cexp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℂ
s : Set α
h : ContinuousOn f s
⊢ ContinuousOn (Y := ℂ) (fun (y : α) ↦ cexp (f y)) s

Tactic:
fun x hx => (h x hx).cexp

Premises used: ContinuousOn, ContinuousWithinAt.cexp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℂ
h : Continuous[inst, _] f
⊢ Continuous[inst, _] fun (y : α) ↦ cexp (f y)

Tactic:
continuous_iff_continuousAt.2 fun _ => h.continuousAt.cexp

Premises used: Iff.mpr, ContinuousAt.cexp, Continuous.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
a : ℝ
⊢ Continuous cexp

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
a : ℝ
⊢ Continuous (cexp - 1)

Tactic:
have : Continuous (cexp - 1) := Continuous.sub (by fun_prop) continuous_one
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
a : ℝ
this : Continuous (cexp - 1)
rw :
  ∀
    (this :
      ∀ (a : ℂ),
        ∀ ε > 0,
          ∀ᶠ (x : ℂ) in 𝓝 a, dist (HSub.hSub (β := (z : ℂ) → ℂ) cexp 1 x) (HSub.hSub (β := (z : ℂ) → ℂ) cexp 1 a) < ε),
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ (x : ℂ),
          Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x →
            ∀ (y : ℂ), Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y → dist x y < δ → dist (cexp x) (cexp y) < ε
⊢ UniformContinuousOn cexp {x : ℂ | x.re ≤ a}

Tactic:
rw [Metric.uniformContinuousOn_iff, Metric.continuous_iff'] at *

Premises used: Metric.uniformContinuousOn_iff, Metric.continuous_iff'
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
a : ℝ
this :
  ∀ (a : ℂ),
    ∀ ε > 0, ∀ᶠ (x : ℂ) in 𝓝 a, dist (HSub.hSub (β := (z : ℂ) → ℂ) cexp 1 x) (HSub.hSub (β := (z : ℂ) → ℂ) cexp 1 a) < ε
ε : ℝ
hε : ε > 0
⊢ ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε

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

Premises used: Pi.one_apply, gt_iff_lt, dist_sub_eq_dist_add_right, sub_add_cancel, Pi.sub_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
⊢ 0 < ε / (2 * Real.exp a)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
⊢ 0 < ε / (2 * Real.exp a)

Tactic:
have ha : 0 < ε / (2 * Real.exp a) := by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, dist (cexp x) (cexp 0) < ε / (2 * Real.exp a)

Tactic:
have H := this 0 (ε / (2 * Real.exp a)) ha
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
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)
⊢ ∃ ε_1 > 0, ∀ ⦃y : ℂ⦄, dist y 0 < ε_1 → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)

Tactic:
rw [Metric.eventually_nhds_iff] at H

Premises used: Metric.eventually_nhds_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
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)
obtain :
  ∀ (δ : ℝ) (hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)),
    ∃ δ > 0,
      ∀ (x : ℂ),
        Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x →
          ∀ (y : ℂ), Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y → dist x y < δ → dist (cexp x) (cexp y) < ε
⊢ ∃ δ > 0,
    ∀ (x : ℂ),
      Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x →
        ∀ (y : ℂ), Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y → dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
obtain ⟨δ, hδ⟩ := H
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
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) (cexp 0) < ε / (2 * Real.exp a)
⊢ ∃ δ > 0,
    ∀ (x : ℂ),
      Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x →
        ∀ (y : ℂ), Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y → dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
⟨δ, hδ.1, ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
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) (cexp 0) < ε / (2 * Real.exp a)
refine :
  ∀ (x : ℂ),
    Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x →
      ∀ (y : ℂ), Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y → dist x y < δ → dist (cexp x) (cexp y) < ε
⊢ ∃ δ > 0,
    ∀ (x : ℂ),
      Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x →
        ∀ (y : ℂ), Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y → dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
refine ⟨δ, hδ.1, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
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) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
_ :
  Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x →
    ∀ (y : ℂ), Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y → dist x y < δ → dist (cexp x) (cexp y) < ε
⊢ Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x →
    ∀ (y : ℂ), Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y → dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
_
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
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) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
h : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x
y : ℂ
hy : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y
hxy : dist x y < δ
⊢ dist (x - y) 0 < δ

Tactic:
simpa only [dist_eq_norm, sub_zero] using hxy

Premises used: dist_eq_norm, sub_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
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) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
h : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x
y : ℂ
hy : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y
hxy : dist x y < δ
⊢ dist (cexp (x - y)) (cexp 0) < ε / (2 * Real.exp a)

Tactic:
have h3 := hδ.2 (y := x - y) (by simpa only [dist_eq_norm, sub_zero] using hxy)
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
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) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
h : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x
y : ℂ
hy : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y
hxy : dist x y < δ
h3 : dist (cexp (x - y)) (cexp 0) < ε / (2 * Real.exp a)
rw :
  ∀ (hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)) (x : ℂ),
    Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x →
      ∀ (y : ℂ) (hy : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y) (hxy : ‖x - y‖ < δ)
        (h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)), ‖cexp x - cexp y‖ < ε
⊢ dist (cexp x) (cexp y) < ε

Tactic:
rw [dist_eq_norm, exp_zero] at *

Premises used: dist_eq_norm, Complex.exp_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
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 : ℂ
h : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x
y : ℂ
hy : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
rw : cexp x - cexp y = cexp (y + (x - y)) - cexp y
⊢ cexp x - cexp y = cexp y * (cexp (x - y) - 1)

Tactic:
rw [mul_sub_one, ← exp_add]

Premises used: Complex.exp_add, mul_sub_one
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
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 : ℂ
h : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x
y : ℂ
hy : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y
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
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
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 : ℂ
h : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x
y : ℂ
hy : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
⊢ cexp x - cexp y = cexp y * (cexp (x - y) - 1)

Tactic:
have : cexp x - cexp y = cexp y * (cexp (x - y) - 1) := by
    rw [mul_sub_one, ← exp_add]
    ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
a ε : ℝ
hε : ε > 0
this_1 : ∀ (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 : ℂ
h : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x
y : ℂ
hy : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
rw : ‖(cexp (x - y) - 1) * cexp y‖ < ε
⊢ ‖cexp x - cexp y‖ < ε

Tactic:
rw [this, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
a ε : ℝ
hε : ε > 0
this_1 : ∀ (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 : ℂ
h : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x
y : ℂ
hy : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y
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:
simpa only [norm_exp, Real.exp_le_exp]

Premises used: Real.exp_le_exp, Complex.norm_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
a ε : ℝ
hε : ε > 0
this_1 : ∀ (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 : ℂ
h : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x
y : ℂ
hy : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y
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:
have hya : ‖cexp y‖ ≤ Real.exp a := by simpa only [norm_exp, Real.exp_le_exp]
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
a ε : ℝ
hε : ε > 0
this_1 : ∀ (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 : ℂ
h : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x
y : ℂ
hy : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y
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
simp :
  ∀ (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 < ε
⊢ ‖(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 *

Premises used: norm_mul, Set.mem_setOf_eq, Complex.norm_exp, gt_iff_lt, dist_zero_right
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
a ε : ℝ
this_1 : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
x : ℂ
h : 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
apply : ε / (2 * Real.exp a) * 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) ha.le)

Premises used: lt_of_le_of_lt, LT.lt.le, Complex.re, mul_le_mul, Real.exp_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
a ε : ℝ
this_1 : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
x : ℂ
h : 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 < ε

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ (Complex.exp (↑x : ℂ)).re

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
s : Set ℝ
⊢ ContinuousOn rexp s

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝 0)
    ((fun (x : ℂ) ↦ Complex.exp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)) ∘ Complex.ofReal)
    ((fun (x : ℂ) ↦ x ^ n) ∘ Complex.ofReal)

Tactic:
have := (Complex.exp_sub_sum_range_isBigO_pow n).comp_tendsto
    (Complex.continuous_ofReal.tendsto' 0 0 rfl)
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
this :
  IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℝ) ↦ Complex.exp (↑x : ℂ) - ∑ i ∈ Finset.range n, (↑x : ℂ) ^ i / (↑i ! : ℂ))
    fun (x : ℝ) ↦ (↑x : ℂ) ^ n
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  ∀
    (this :
      IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : ℝ) ↦ rexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℝ)) fun (x : ℝ) ↦
        x ^ n),
    IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : ℝ) ↦ rexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℝ)) fun (x : ℝ) ↦ x ^ n
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : ℝ) ↦ rexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℝ)) fun (x : ℝ) ↦ x ^ n

Tactic:
norm_cast at this
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : ℝ) ↦ rexp x - ∑ i ∈ Finset.range (n + 1), x ^ i / (↑i ! : ℝ))
    fun (x : ℝ) ↦ x ^ n

Tactic:
(exp_sub_sum_range_isBigO_pow (n + 1)).trans_isLittleO <| isLittleO_pow_pow n.lt_succ_self

Premises used: Asymptotics.isLittleO_pow_pow, Nat.lt_succ_self, HAdd.hAdd, Asymptotics.IsBigO.trans_isLittleO, OfNat.ofNat, Real.exp_sub_sum_range_isBigO_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
z : ℝ
hf : Tendsto f l (𝓝 z)
⊢ Tendsto (fun (x : α) ↦ rexp (f x)) l (𝓝 (rexp z))

Tactic:
(continuous_exp.tendsto _).comp hf

Premises used: Real.exp, Continuous.tendsto, Real.continuous_exp, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
s : Set α
x : α
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (Y := ℝ) (fun (y : α) ↦ rexp (f y)) s x

Tactic:
h.rexp

Premises used: ContinuousWithinAt, Filter.Tendsto.rexp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
x : α
h : ContinuousAt f x
⊢ ContinuousAt (Y := ℝ) (fun (y : α) ↦ rexp (f y)) x

Tactic:
h.rexp

Premises used: ContinuousAt, Filter.Tendsto.rexp