awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
⊢ AnalyticAt ℂ L.relation x
have pos : ∀ (hx : x ∈ L.lattice), AnalyticAt ℂ L.relation x
Tactic: by_cases hx : x ∈ L.lattice
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
pos : ∀ (hx : x ∈ L.lattice), AnalyticAt ℂ L.relation x
⊢ AnalyticAt ℂ L.relation x
have neg : ∀ (hx : x ∉ L.lattice), AnalyticAt ℂ L.relation x
Tactic: by_cases hx : x ∈ L.lattice
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ AnalyticAt ℂ L.relation x
have pos : ∀ (x : ↥L.lattice), AnalyticAt ℂ L.relation (↑x : ℂ)
Tactic: lift x to L.lattice using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
x : ↥L.lattice
⊢ AnalyticAt ℂ L.relation (↑x : ℂ)
have this : AnalyticAt ℂ L.relation 0
Tactic: have := L.analyticAt_relation_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
x : ↥L.lattice
this : AnalyticAt ℂ L.relation 0
⊢ AnalyticAt ℂ L.relation (↑x : ℂ)
have this₁ : AnalyticAt ℂ L.relation ((↑x : ℂ) - (↑x : ℂ))
Tactic: rw [← sub_self x.1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ↥L.lattice
this : AnalyticAt ℂ L.relation ((↑x : ℂ) - (↑x : ℂ))
⊢ AnalyticAt ℂ L.relation (↑x : ℂ)
have h : L.relation = L.relation ∘ fun (x_1 : ℂ) ↦ x_1 - (↑x : ℂ)
Tactic: convert! this.comp (f := (· - x.1)) (by fun_prop)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ↥L.lattice
this : AnalyticAt ℂ L.relation ((↑x : ℂ) - (↑x : ℂ))
⊢ L.relation = L.relation ∘ fun (x_1 : ℂ) ↦ x_1 - (↑x : ℂ)
have h : ∀ (a : ℂ), L.relation a = (L.relation ∘ fun (x_1 : ℂ) ↦ x_1 - (↑x : ℂ)) a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) x
have this : AnalyticAt ℂ ℘'[L] x
Tactic: have := L.analyticOnNhd_derivWeierstrassP _ hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
this : AnalyticAt ℂ ℘'[L] x
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) x
have this₁ : AnalyticAt ℂ ℘[L] x
Tactic: have := L.analyticOnNhd_weierstrassP _ hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ AnalyticAt ℂ L.relation x
have this : AnalyticAt ℂ (F := ℂ)
  (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) x
Tactic: have : AnalyticAt ℂ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) x := by
      have := L.analyticOnNhd_derivWeierstrassP _ hx
      have := L.analyticOnNhd_weierstrassP _ hx
      fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
this :
  AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) x
⊢ AnalyticAt ℂ L.relation x
have neg : (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) =ᶠ[𝓝 x]
  L.relation
Tactic: apply this.congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
this :
  AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) x
⊢ (fun (z : ℂ) ↦ HPow.hPow (β := ℕ) (℘'[L] z) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] z) 3 + L.g₂ * ℘[L] z + L.g₃) =ᶠ[𝓝 x]
    L.relation
have h : ∀ (x : ℂ) (hx : x ∈ (↑L.lattice : Set ℂ)ᶜ),
  HPow.hPow (β := ℕ) (℘'[L] x) 2 - 4 * HPow.hPow (β := ℕ) (℘[L] x) 3 + L.g₂ * ℘[L] x + L.g₃ = L.relation x
Tactic: filter_upwards [L.isClosed_lattice.isOpen_compl.mem_nhds hx] with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
⊢ L.relation = 0
have h : ∀ (x : ℂ), L.relation x = 0 x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (hypothesis)
Goal:
L : PeriodPair
x : ℂ
⊢ L.relation x = 0 x
have this : Differentiable ℂ L.relation
Tactic: have : Differentiable ℂ L.relation := fun x ↦ (L.analyticAt_relation x).differentiableAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass (goal)
Goal:
L : PeriodPair
x : ℂ
this : Differentiable ℂ L.relation
z w : ℂ
hw : w ∈ L.lattice
⊢ L.relation (z + w) = L.relation z
have lift : ∀ (w : ↥L.lattice), L.relation (z + (↑w : ℂ)) = L.relation z
Tactic: lift w to L.lattice using hw
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖cexp (x + z) - cexp x - z * cexp x‖ = ‖cexp x * (cexp z - 1 - z)‖
have e_a : cexp (x + z) - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ cexp (x + z) - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)
have e_a : cexp x * cexp z - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)
Tactic: rw [exp_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
⊢ ‖cexp y - cexp x‖ ≤ (1 + r) * ‖cexp x‖ * ‖y - x‖
have hy_eq : y = x + (y - x)
Tactic: have hy_eq : y = x + (y - x) := by abel
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ r * ‖y - x‖
have rw : ‖y - x‖ * ‖y - x‖ ≤ r * ‖y - x‖
Tactic: rw [pow_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖cexp y - cexp x‖ ≤ (1 + r) * ‖cexp x‖ * ‖y - x‖
have hyx_sq_le : HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ r * ‖y - x‖
Tactic: have hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖ := by
    rw [pow_two]
    exact mul_le_mul hyx.le le_rfl (norm_nonneg _) hr_nonneg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
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‖
z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
have this : ‖cexp (x + z) - cexp x - z • cexp x‖ ≤ ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
Tactic: have : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2 := exp_bound_sq x z hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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‖
z : ℂ
hz : ‖z‖ ≤ 1
this : ‖cexp (x + z) - cexp x - z • cexp x‖ ≤ ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
⊢ ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
have rw : ‖cexp (x + z) - cexp x‖ - ‖z • cexp x‖ ≤ ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
Tactic: rw [← sub_le_iff_le_add', ← norm_smul z]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
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‖
⊢ ‖cexp y - cexp x‖ ≤ (1 + r) * ‖cexp x‖ * ‖y - x‖
have h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖cexp (x + z) - cexp x‖ ≤ ‖z‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖z‖ 2
Tactic: have h_sq : ∀ z, ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2 := by
    intro z hz
    have : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2 := exp_bound_sq x z hz
    rw [← sub_le_iff_le_add', ← norm_smul z]
    exact (norm_sub_norm_le _ _).trans this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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
⊢ ‖cexp y - cexp x‖ = ‖cexp (x + (y - x)) - cexp x‖
have nth_rw : ‖cexp (x + (y - x)) - cexp x‖ = ‖cexp (x + (y - x)) - cexp x‖
Tactic: nth_rw 1 [hy_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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‖ * HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * (r * ‖y - x‖)
have h₁ : 0 ≤ ‖cexp x‖
Tactic: grw [hyx_sq_le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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‖
⊢ ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * (r * ‖y - x‖)
have grw : ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * (r * ‖y - x‖) ≤ ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * (r * ‖y - x‖)
Tactic: grw [hyx_sq_le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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
⊢ ‖cexp y - cexp x‖ ≤ (1 + r) * ‖cexp x‖ * ‖y - x‖
have y₁ : ‖cexp y - cexp x‖ = ‖cexp (x + (y - x)) - cexp 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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‖
⊢ ‖cexp y - cexp x‖ ≤ (1 + r) * ‖cexp x‖ * ‖y - x‖
have y₂ : ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * HPow.hPow (β := ℕ) ‖y - x‖ 2 ≤ ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * (r * ‖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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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‖)
⊢ ‖cexp y - cexp x‖ ≤ (1 + r) * ‖cexp x‖ * ‖y - x‖
have y₃ : ‖y - x‖ * ‖cexp x‖ + ‖cexp x‖ * (r * ‖y - 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
n : ℕ
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)) fun (x : ℂ) ↦ x ^ n
have inl : IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ cexp x - ∑ i ∈ Finset.range 0, x ^ i / (↑i ! : ℂ)) fun (x : ℂ) ↦
  HPow.hPow (β := ℕ) x 0
Tactic: rcases eq_zero_or_pos n with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
n : ℕ
inl :
  IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ cexp x - ∑ i ∈ Finset.range 0, x ^ i / (↑i ! : ℂ)) fun (x : ℂ) ↦
    HPow.hPow (β := ℕ) x 0
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)) fun (x : ℂ) ↦ x ^ n
have inr : ∀ (hn : 0 < 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
n : ℕ
hn : 0 < n
⊢ IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)) fun (x : ℂ) ↦ x ^ n
have inr : ∀ᶠ (x : ℂ) in 𝓝 0,
  ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)‖ ≤ (↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ) * ‖x ^ n‖
Tactic: refine .of_bound (n.succ / (n ! * n)) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
n : ℕ
hn : 0 < n
⊢ ∀ᶠ (x : ℂ) in 𝓝 0,
    ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)‖ ≤
      (↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ) * ‖x ^ n‖
have 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‖
Tactic: rw [NormedAddGroup.nhds_zero_basis_norm_lt.eventually_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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‖
have 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‖
Tactic: refine ⟨1, one_pos, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
n : ℕ
hn : 0 < n
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‖
have h : (↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ) * ‖x ^ n‖ =
  ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n ! : ℝ) (↑n : ℝ))⁻¹)
Tactic: convert! exp_bound hx.out.le hn using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
a : ℝ
⊢ UniformContinuousOn cexp {x : ℂ | x.re ≤ a}
have this : Continuous (cexp - 1)
Tactic: have : Continuous (cexp - 1) := Continuous.sub (by fun_prop) continuous_one
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
a : ℝ
this : Continuous (cexp - 1)
⊢ UniformContinuousOn cexp {x : ℂ | x.re ≤ a}
have 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) < ε
Tactic: rw [Metric.uniformContinuousOn_iff, Metric.continuous_iff'] at *
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
a : ℝ
this :
  ∀ (a : ℂ),
    ∀ ε > 0, ∀ᶠ (x : ℂ) in 𝓝 a, dist (HSub.hSub (β := (z : ℂ) → ℂ) cexp 1 x) (HSub.hSub (β := (z : ℂ) → ℂ) cexp 1 a) < ε
ε : ℝ
hε : ε > 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) < ε
have this₁ : ∀ (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp 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) < ε
have ha : 0 < ε / (2 * Real.exp a)
Tactic: have ha : 0 < ε / (2 * Real.exp a) := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 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) < ε
have H : ∀ᶠ (x : ℂ) in 𝓝 0, dist (cexp x) (cexp 0) < ε / (2 * Real.exp a)
Tactic: have H := this 0 (ε / (2 * Real.exp a)) ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
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)
⊢ ∃ δ > 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) < ε
have H₁ : ∃ ε_1 > 0, ∀ ⦃y : ℂ⦄, dist y 0 < ε_1 → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)
Tactic: rw [Metric.eventually_nhds_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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)
⊢ ∃ δ > 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) < ε
have 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) < ε
Tactic: obtain ⟨δ, hδ⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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) < ε
have 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) < ε
Tactic: refine ⟨δ, hδ.1, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
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) (cexp y) < ε
have h3 : 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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)
⊢ dist (cexp x) (cexp y) < ε
have 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‖ < ε
Tactic: rw [dist_eq_norm, exp_zero] at *
Cleared hypotheses: hδ, x, h, y, hy, hxy, h3
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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)
have rw : cexp x - cexp y = cexp (y + (x - y)) - cexp y
Tactic: rw [mul_sub_one, ← exp_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
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‖ < ε
have this₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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 x - cexp y‖ < ε
have rw : ‖(cexp (x - y) - 1) * cexp y‖ < ε
Tactic: rw [this, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
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 (x - y) - 1) * cexp y‖ < ε
have hya : ‖cexp y‖ ≤ Real.exp a
Tactic: have hya : ‖cexp y‖ ≤ Real.exp a := by simpa only [norm_exp, Real.exp_le_exp]