awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖x‖ ^ n / (↑n.factorial : ℝ) * ∑ i ∈ range k, ‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i ≤
    ‖x‖ ^ n / (↑n.factorial : ℝ) * 2
have calc_3 : LE.le (α := ℝ) (∑ i ∈ range k, ‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i) 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ LE.le (α := ℝ) (∑ i ∈ range k, ‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i) 2
have calc_3 : LE.le (α := ℝ) (∑ x_1 ∈ range k, (‖x‖ / (↑n.succ : ℝ)) ^ x_1) 2
Tactic: simp_rw [← div_pow]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ LE.le (α := ℝ) (∑ x_1 ∈ range k, (‖x‖ / (↑n.succ : ℝ)) ^ x_1) 2
have calc_3 : 2 * (‖x‖ / (↑n.succ : ℝ) - 1) ≤ (‖x‖ / (↑n.succ : ℝ)) ^ k - 1
Tactic: rw [geom_sum_eq, div_le_iff_of_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
calc_3 : 2 * (‖x‖ / (↑n.succ : ℝ) - 1) ≤ (‖x‖ / (↑n.succ : ℝ)) ^ k - 1
⊢ LE.le (α := ℝ) (∑ x_1 ∈ range k, (‖x‖ / (↑n.succ : ℝ)) ^ x_1) 2
have calc_3₁ : ‖x‖ / (↑n.succ : ℝ) - 1 < 0
Tactic: rw [geom_sum_eq, div_le_iff_of_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
calc_3 : 2 * (‖x‖ / (↑n.succ : ℝ) - 1) ≤ (‖x‖ / (↑n.succ : ℝ)) ^ k - 1
calc_3₁ : ‖x‖ / (↑n.succ : ℝ) - 1 < 0
⊢ LE.le (α := ℝ) (∑ x_1 ∈ range k, (‖x‖ / (↑n.succ : ℝ)) ^ x_1) 2
have calc_3₂ : ‖x‖ / (↑n.succ : ℝ) ≠ 1
Tactic: rw [geom_sum_eq, div_le_iff_of_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 2 * (‖x‖ / (↑n.succ : ℝ) - 1) ≤ (‖x‖ / (↑n.succ : ℝ)) ^ k - 1
have trans : 2 * (‖x‖ / (↑n.succ : ℝ) - 1) ≤ -1
Tactic: trans (-1 : ℝ)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
trans : 2 * (‖x‖ / (↑n.succ : ℝ) - 1) ≤ -1
⊢ 2 * (‖x‖ / (↑n.succ : ℝ) - 1) ≤ (‖x‖ / (↑n.succ : ℝ)) ^ k - 1
have trans₁ : -1 ≤ (‖x‖ / (↑n.succ : ℝ)) ^ k - 1
Tactic: trans (-1 : ℝ)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 2 * (‖x‖ / (↑n.succ : ℝ) - 1) ≤ -1
have linarith : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
linarith : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) → HMul.hMul (α := ℝ) 1 1 = 1
⊢ 2 * (‖x‖ / (↑n.succ : ℝ) - 1) ≤ -1
have linarith₁ : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
linarith : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) → 2 / 2 = 1
⊢ 2 * (‖x‖ / (↑n.succ : ℝ) - 1) ≤ -1
have linarith₂ : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
linarith : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) → 2 / 2 = 1
linarith₂ : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 2 * (‖x‖ / (↑n.succ : ℝ) - 1) ≤ -1
have linarith₃ : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
linarith : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) → 2 / 2 = 1
linarith₂ : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₃ : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) → GT.gt (α := ℝ) 2 0
⊢ 2 * (‖x‖ / (↑n.succ : ℝ) - 1) ≤ -1
have linarith₄ : -1 < 2 * (‖x‖ / (↑n.succ : ℝ) - 1) →
  2 * (‖x‖ / (↑n.succ : ℝ)) - HMul.hMul (α := ℝ) 1 1 +
      (-HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 2 * (1 * (‖x‖ / (↑n.succ : ℝ)) - HMul.hMul (α := ℝ) 1 1)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ -1 ≤ (‖x‖ / (↑n.succ : ℝ)) ^ k - 1
have simp : 0 ≤ ‖x‖ ^ k / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ k
Tactic: simp only [neg_le_sub_iff_le_add, div_pow, Nat.cast_succ, le_add_iff_nonneg_left]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖x‖ / (↑n.succ : ℝ) - 1 < 0
have linarith : 0 ≤ ‖x‖ / (↑n.succ : ℝ) - 1 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
linarith : 0 ≤ ‖x‖ / (↑n.succ : ℝ) - 1 → 2 / 2 = 1
⊢ ‖x‖ / (↑n.succ : ℝ) - 1 < 0
have linarith₁ : 0 ≤ ‖x‖ / (↑n.succ : ℝ) - 1 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
linarith : 0 ≤ ‖x‖ / (↑n.succ : ℝ) - 1 → 2 / 2 = 1
linarith₁ : 0 ≤ ‖x‖ / (↑n.succ : ℝ) - 1 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ ‖x‖ / (↑n.succ : ℝ) - 1 < 0
have linarith₂ : 0 ≤ ‖x‖ / (↑n.succ : ℝ) - 1 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
linarith : 0 ≤ ‖x‖ / (↑n.succ : ℝ) - 1 → 2 / 2 = 1
linarith₁ : 0 ≤ ‖x‖ / (↑n.succ : ℝ) - 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 0 ≤ ‖x‖ / (↑n.succ : ℝ) - 1 → GT.gt (α := ℝ) 2 0
⊢ ‖x‖ / (↑n.succ : ℝ) - 1 < 0
have linarith₃ : 0 ≤ ‖x‖ / (↑n.succ : ℝ) - 1 →
  -1 + (2 * (‖x‖ / (↑n.succ : ℝ)) - HMul.hMul (α := ℝ) 1 1) +
      2 * (HMul.hMul (α := ℝ) 1 0 - (1 * (‖x‖ / (↑n.succ : ℝ)) - HMul.hMul (α := ℝ) 1 1)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖x‖ / (↑n.succ : ℝ) ≠ 1
have linarith : ‖x‖ / (↑n.succ : ℝ) = 1 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
linarith : ‖x‖ / (↑n.succ : ℝ) = 1 → 2 / 2 = 1
⊢ ‖x‖ / (↑n.succ : ℝ) ≠ 1
have linarith₁ : ‖x‖ / (↑n.succ : ℝ) = 1 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
linarith : ‖x‖ / (↑n.succ : ℝ) = 1 → 2 / 2 = 1
linarith₁ : ‖x‖ / (↑n.succ : ℝ) = 1 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ ‖x‖ / (↑n.succ : ℝ) ≠ 1
have linarith₂ : ‖x‖ / (↑n.succ : ℝ) = 1 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
linarith : ‖x‖ / (↑n.succ : ℝ) = 1 → 2 / 2 = 1
linarith₁ : ‖x‖ / (↑n.succ : ℝ) = 1 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ‖x‖ / (↑n.succ : ℝ) = 1 → GT.gt (α := ℝ) 2 0
⊢ ‖x‖ / (↑n.succ : ℝ) ≠ 1
have linarith₃ : ‖x‖ / (↑n.succ : ℝ) = 1 →
  -1 + (2 * (‖x‖ / (↑n.succ : ℝ)) - HMul.hMul (α := ℝ) 1 1) +
      2 * -(1 * (‖x‖ / (↑n.succ : ℝ)) - HMul.hMul (α := ℝ) 1 1) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * ((↑(Nat.succ 2) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 2) : ℝ) (↑2 : ℝ))⁻¹) ≤
    HPow.hPow (β := ℕ) ‖x‖ 2 * 1
have hbc : (↑(Nat.succ 2) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 2) : ℝ) (↑2 : ℝ))⁻¹ ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * 1 = HPow.hPow (β := ℕ) ‖x‖ 2
have rw : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)‖ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / (↑m.factorial : ℝ)
have rw : (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤
  Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / (↑m.factorial : ℝ)
Tactic: rw [← CauSeq.lim_const (abv := norm) (∑ m ∈ range n, _), Complex.exp, sub_eq_add_neg,
    ← CauSeq.lim_neg, CauSeq.lim_add, ← lim_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤
    Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / (↑m.factorial : ℝ)
have refine : ∀ (j : ℕ) (hj : j ≥ n),
  (↑(cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))) : ℕ → ℝ) j ≤
    (↑(const abs (Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / (↑m.factorial : ℝ))) : ℕ → ℝ) j
Tactic: refine CauSeq.lim_le (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖HSub.hSub (α := ℂ) (∑ m ∈ range j, x ^ m / (↑m.factorial : ℂ)) (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ))‖ ≤
    HSub.hSub (α := ℝ) (∑ m ∈ range j, ‖x‖ ^ m / (↑m.factorial : ℝ)) (∑ m ∈ range n, ‖x‖ ^ m / (↑m.factorial : ℝ))
have rw : norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
  ∑ k ∈ range j with n ≤ k, ‖x‖ ^ k / (↑k.factorial : ℝ)
Tactic: rw [sum_range_sub_sum_range hj, sum_range_sub_sum_range hj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    ∑ k ∈ range j with n ≤ k, ‖x‖ ^ k / (↑k.factorial : ℝ)
have refine : Eq (α := ℝ) (∑ i ∈ range j with n ≤ i, ‖x ^ i / (↑i.factorial : ℂ)‖)
  (∑ k ∈ range j with n ≤ k, ‖x‖ ^ k / (↑k.factorial : ℝ))
Tactic: refine (IsAbsoluteValue.abv_sum norm ..).trans_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ Eq (α := ℝ) (∑ i ∈ range j with n ≤ i, ‖x ^ i / (↑i.factorial : ℂ)‖)
    (∑ k ∈ range j with n ≤ k, ‖x‖ ^ k / (↑k.factorial : ℝ))
have e_f : ∀ (i : ℕ), ‖x ^ i / (↑i.factorial : ℂ)‖ = ‖x‖ ^ i / (↑i.factorial : ℝ)
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ HSub.hSub (α := ℝ) (∑ m ∈ range j, ‖x‖ ^ m / (↑m.factorial : ℝ)) (∑ m ∈ range n, ‖x‖ ^ m / (↑m.factorial : ℝ)) ≤
    Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / (↑m.factorial : ℝ)
have h : ∑ m ∈ range j, ‖x‖ ^ m / (↑m.factorial : ℝ) ≤ Real.exp ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ (↑(cauSeqNorm (exp' x - const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))) : ℕ → ℝ) j ≤
    (↑(const abs (Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / (↑m.factorial : ℝ))) : ℕ → ℝ) j
have calc : ‖HSub.hSub (α := ℂ) (∑ m ∈ range j, x ^ m / (↑m.factorial : ℂ)) (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ))‖ ≤
  HSub.hSub (α := ℝ) (∑ m ∈ range j, ‖x‖ ^ m / (↑m.factorial : ℝ)) (∑ m ∈ range n, ‖x‖ ^ m / (↑m.factorial : ℝ))
Tactic: calc ‖(∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial‖
  _ ≤ (∑ m ∈ range j, ‖x‖ ^ m / m.factorial) - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial := by
    rw [sum_range_sub_sum_range hj, sum_range_sub_sum_range hj]
    refine (IsAbsoluteValue.abv_sum norm ..).trans_eq ?_
    congr with i
    simp [Complex.norm_pow, Complex.norm_natCast]
  _ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial := by
    gcongr
    exact Real.sum_le_exp_of_nonneg (norm_nonneg _) _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
calc :
  ‖HSub.hSub (α := ℂ) (∑ m ∈ range j, x ^ m / (↑m.factorial : ℂ)) (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ))‖ ≤
    HSub.hSub (α := ℝ) (∑ m ∈ range j, ‖x‖ ^ m / (↑m.factorial : ℝ)) (∑ m ∈ range n, ‖x‖ ^ m / (↑m.factorial : ℝ))
⊢ (↑(cauSeqNorm (exp' x - const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))) : ℕ → ℝ) j ≤
    (↑(const abs (Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / (↑m.factorial : ℝ))) : ℕ → ℝ) j
have calc₁ : HSub.hSub (α := ℝ) (∑ m ∈ range j, ‖x‖ ^ m / (↑m.factorial : ℝ)) (∑ m ∈ range n, ‖x‖ ^ m / (↑m.factorial : ℝ)) ≤
  Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / (↑m.factorial : ℝ)
Tactic: calc ‖(∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial‖
  _ ≤ (∑ m ∈ range j, ‖x‖ ^ m / m.factorial) - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial := by
    rw [sum_range_sub_sum_range hj, sum_range_sub_sum_range hj]
    refine (IsAbsoluteValue.abv_sum norm ..).trans_eq ?_
    congr with i
    simp [Complex.norm_pow, Complex.norm_natCast]
  _ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial := by
    gcongr
    exact Real.sum_le_exp_of_nonneg (norm_nonneg _) _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
⊢ ‖cexp x‖ ≤ Real.exp ‖x‖
have h : ‖cexp x‖ = ‖cexp x - ∑ m ∈ range 0, x ^ m / (↑m.factorial : ℂ)‖
Tactic: convert! norm_exp_sub_sum_le_exp_norm_sub_sum x 0 using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
h : ‖cexp x‖ = ‖cexp x - ∑ m ∈ range 0, x ^ m / (↑m.factorial : ℂ)‖
⊢ ‖cexp x‖ ≤ Real.exp ‖x‖
have h₁ : Real.exp ‖x‖ = Real.exp ‖x‖ - ∑ m ∈ range 0, ‖x‖ ^ m / (↑m.factorial : ℝ)
Tactic: convert! norm_exp_sub_sum_le_exp_norm_sub_sum x 0 using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)‖ ≤ ‖x‖ ^ n * Real.exp ‖x‖
have rw : (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤ ‖x‖ ^ n * Real.exp ‖x‖
Tactic: rw [← CauSeq.lim_const (abv := norm) (∑ m ∈ range n, _), Complex.exp, sub_eq_add_neg,
    ← CauSeq.lim_neg, CauSeq.lim_add, ← lim_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤ ‖x‖ ^ n * Real.exp ‖x‖
have refine : ∀ (j : ℕ) (hj : j ≥ n),
  (↑(cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))) : ℕ → ℝ) j ≤
    (↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) : ℕ → ℝ) j
Tactic: refine CauSeq.lim_le (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖HSub.hSub (α := ℂ) (∑ m ∈ range j, x ^ m / (↑m.factorial : ℂ)) (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ))‖ ≤
    (↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) : ℕ → ℝ) j
have rw : norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤ (↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) : ℕ → ℝ) j
Tactic: rw [sum_range_sub_sum_range hj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ norm (E := ℂ) (∑ m ∈ range j with n ≤ m, x ^ m / (↑m.factorial : ℂ)) =
    norm (E := ℂ) (∑ m ∈ range j with n ≤ m, x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ)))
have refine : ∀ (m : ℕ) (hm : m ∈ {m ∈ range j | n ≤ m}), x ^ m / (↑m.factorial : ℂ) = x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))
Tactic: refine congr_arg norm (sum_congr rfl fun m hm => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ {m ∈ range j | n ≤ m}
⊢ x ^ m / (↑m.factorial : ℂ) = x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))
have hm₁ : m < j ∧ n ≤ m
Tactic: rw [mem_filter, mem_range] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ x ^ m / (↑m.factorial : ℂ) = x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))
have rw : x ^ m / (↑m.factorial : ℂ) = x ^ n * x ^ (m - n) / (↑m.factorial : ℂ)
Tactic: rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.2]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : m < j ∧ n ≤ m
rw : x ^ m / (↑m.factorial : ℂ) = x ^ n * x ^ (m - n) / (↑m.factorial : ℂ)
⊢ x ^ m / (↑m.factorial : ℂ) = x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))
have rw₁ : x ^ m / (↑m.factorial : ℂ) = x ^ (n + (m - n)) / (↑m.factorial : ℂ)
Tactic: rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.2]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : m < j ∧ n ≤ m
rw : x ^ m / (↑m.factorial : ℂ) = x ^ n * x ^ (m - n) / (↑m.factorial : ℂ)
rw₁ : x ^ m / (↑m.factorial : ℂ) = x ^ (n + (m - n)) / (↑m.factorial : ℂ)
⊢ x ^ m / (↑m.factorial : ℂ) = x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))
have rw₂ : x ^ m / (↑m.factorial : ℂ) = x ^ m / (↑m.factorial : ℂ)
Tactic: rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.2]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ LE.le (α := ℝ) (∑ m ∈ range j with n ≤ m, ‖x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))‖)
    (∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)))
have simp_rw : LE.le (α := ℝ) (∑ x_1 ∈ range j with n ≤ x_1, ‖x‖ ^ n * (‖x ^ (x_1 - n)‖ / (↑x_1.factorial : ℝ)))
  (∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)))
Tactic: simp_rw [Complex.norm_mul, Complex.norm_pow, Complex.norm_div, norm_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ LE.le (α := ℝ) (∑ x_1 ∈ range j with n ≤ x_1, ‖x‖ ^ n * (‖x ^ (x_1 - n)‖ / (↑x_1.factorial : ℝ)))
    (∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)))
have h : ∀ (i : ℕ) (hi : i ∈ {m ∈ range j | n ≤ m}), ‖x ^ (i - n)‖ ≤ ‖x‖ ^ (i - n)
Tactic: gcongr with i hi
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
h : ∀ (i : ℕ) (hi : i ∈ {m ∈ range j | n ≤ m}), ‖x ^ (i - n)‖ ≤ ‖x‖ ^ (i - n)
⊢ LE.le (α := ℝ) (∑ x_1 ∈ range j with n ≤ x_1, ‖x‖ ^ n * (‖x ^ (x_1 - n)‖ / (↑x_1.factorial : ℝ)))
    (∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)))
have h₁ : ∀ (i : ℕ) (hi : i ∈ {m ∈ range j | n ≤ m}), i - n ≤ i
Tactic: gcongr with i hi
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
hi : i ∈ {m ∈ range j | n ≤ m}
⊢ ‖x ^ (i - n)‖ ≤ ‖x‖ ^ (i - n)
have h : ‖x‖ ^ (i - n) ≤ ‖x‖ ^ (i - n)
Tactic: rw [Complex.norm_pow]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)) =
    ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)
have rw : ‖x‖ ^ n * ∑ i ∈ range j with n ≤ i, ‖x‖ ^ (i - n) / (↑(i - n).factorial : ℝ) =
  ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)
Tactic: rw [← mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ) =
    ‖x‖ ^ n * ∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ)
have e_a : Eq (α := ℝ) (∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ))
  (∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ Eq (α := ℝ) (∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ))
    (∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ))
have e_a : ∀ (a : ℕ) (ha : a ∈ range (j - n)), (fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha ∈ {m ∈ range j | n ≤ m}
Tactic: refine (sum_bij (fun m hm ↦ m + n) ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
e_a : ∀ (a : ℕ) (ha : a ∈ range (j - n)), (fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha ∈ {m ∈ range j | n ≤ m}
⊢ Eq (α := ℝ) (∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ))
    (∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ))
have e_a₁ : ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ range (j - n)) (a₂ : ℕ) (ha₂ : a₂ ∈ range (j - n)),
  Eq (α := ℕ) ((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a₁ ha₁)
      ((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a₂ ha₂) →
    a₁ = a₂
Tactic: refine (sum_bij (fun m hm ↦ m + n) ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
e_a : ∀ (a : ℕ) (ha : a ∈ range (j - n)), (fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha ∈ {m ∈ range j | n ≤ m}
e_a₁ :
  ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ range (j - n)) (a₂ : ℕ) (ha₂ : a₂ ∈ range (j - n)),
    Eq (α := ℕ) ((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a₁ ha₁)
        ((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a₂ ha₂) →
      a₁ = a₂
⊢ Eq (α := ℝ) (∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ))
    (∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ))
have e_a₂ : ∀ b ∈ {m ∈ range j | n ≤ m}, ∃ (a : ℕ) (ha : a ∈ range (j - n)), (fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha = b
Tactic: refine (sum_bij (fun m hm ↦ m + n) ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
e_a : ∀ (a : ℕ) (ha : a ∈ range (j - n)), (fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha ∈ {m ∈ range j | n ≤ m}
e_a₁ :
  ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ range (j - n)) (a₂ : ℕ) (ha₂ : a₂ ∈ range (j - n)),
    Eq (α := ℕ) ((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a₁ ha₁)
        ((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a₂ ha₂) →
      a₁ = a₂
e_a₂ :
  ∀ b ∈ {m ∈ range j | n ≤ m},
    ∃ (a : ℕ) (ha : a ∈ range (j - n)), (fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha = b
⊢ Eq (α := ℝ) (∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ))
    (∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ))
have e_a₃ : ∀ (a : ℕ) (ha : a ∈ range (j - n)),
  ‖x‖ ^ a / (↑a.factorial : ℝ) =
    ‖x‖ ^ ((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha - n) /
      (↑((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha - n).factorial : ℝ)
Tactic: refine (sum_bij (fun m hm ↦ m + n) ?_ ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b ∈ {m ∈ range j | n ≤ m}
⊢ ∃ (a : ℕ) (ha : a ∈ range (j - n)), (fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha = b
have e_a : ∃ a < j - n, a + n = b
Tactic: simp only [mem_range, exists_prop]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b ∈ {m ∈ range j | n ≤ m}
⊢ ∃ a < j - n, a + n = b
have hb₁ : b < j ∧ n ≤ b
Tactic: simp only [mem_filter, mem_range] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
⊢ ∃ a < j - n, a + n = b
have e_a : b - n < j - n
Tactic: refine ⟨b - n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
e_a : b - n < j - n
⊢ ∃ a < j - n, a + n = b
have e_a₁ : b - n + n = b
Tactic: refine ⟨b - n, ?_, ?_⟩