-- Mathlib/Data/Complex/Exponential.lean
theorem exp_bound {x : ℂ} (hx : ‖x‖ ≤ 1) {n : ℕ} (hn : 0 < n) :
    ‖exp x - ∑ m ∈ range n, x ^ m / m.factorial‖ ≤
      ‖x‖ ^ n * ((n.succ : ℝ) * (n.factorial * n : ℝ)⁻¹)

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))).lim ≤
    ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)

Tactic:
refine lim_le (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)

Result:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤
    ↑(const abs (‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹))) j

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)

Tactic:
rw [← lim_const (abv := norm) (∑ m ∈ range n, _), exp, sub_eq_add_neg,
  ← lim_neg, lim_add, ← lim_norm]

Result:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))).lim ≤
    ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤
    ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)

Tactic:
rw [sum_range_sub_sum_range hj]

Result:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ‖∑ k ∈ filter (fun k => n ≤ k) (range j), x ^ k / ↑k.factorial‖ ≤ ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ 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]

Result:
no goals

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ filter (fun m => n ≤ m) (range j), x ^ m / ↑m.factorial‖ =
    ‖∑ m ∈ filter (fun m => n ≤ m) (range j), x ^ n * (x ^ (m - n) / ↑m.factorial)‖

Tactic:
refine congr_arg norm (sum_congr rfl fun m hm => ?_)

Result:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ filter (fun m => n ≤ m) (range j)
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ filter (fun m => n ≤ m) (range j)
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)

Tactic:
rw [mem_filter, mem_range] at hm

Result:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)

Proof state:
case h
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ filter (fun m => n ≤ m) (range j), 1 / ↑m.factorial ≤ ↑n.succ * (↑n.factorial * ↑n)⁻¹

Tactic:
exact sum_div_factorial_le _ _ hn

Result:
no goals

Proof state:
case h.h.hab
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
i✝ : ℕ
a✝ : i✝ ∈ filter (fun m => n ≤ m) (range j)
⊢ ‖x ^ (i✝ - n)‖ ≤ 1

Tactic:
rw [Complex.norm_pow]

Result:
case h.h.hab
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
i✝ : ℕ
a✝ : i✝ ∈ filter (fun m => n ≤ m) (range j)
⊢ ‖x‖ ^ (i✝ - n) ≤ 1

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ x_1 ∈ filter (fun m => n ≤ m) (range j), ‖x‖ ^ n * (‖x ^ (x_1 - n)‖ / ↑x_1.factorial) ≤
    ∑ m ∈ filter (fun m => n ≤ m) (range j), ‖x‖ ^ n * (1 / ↑m.factorial)

Tactic:
gcongr

Result:
case h.h.hab
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
i✝ : ℕ
a✝ : i✝ ∈ filter (fun m => n ≤ m) (range j)
⊢ ‖x ^ (i✝ - n)‖ ≤ 1

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ‖∑ k ∈ filter (fun k => n ≤ k) (range j), x ^ k / ↑k.factorial‖ ≤ ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)

Tactic:
calc
  ‖∑ m ∈ range j with n ≤ m, (x ^ m / m.factorial : ℂ)‖
    = ‖∑ m ∈ range j with n ≤ m, (x ^ n * (x ^ (m - n) / m.factorial) : ℂ)‖ := by
    refine congr_arg norm (sum_congr rfl fun m hm => ?_)
    rw [mem_filter, mem_range] at hm
    rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.2]
  _ ≤ ∑ m ∈ range j with n ≤ m, ‖x ^ n * (x ^ (m - n) / m.factorial)‖ :=
    IsAbsoluteValue.abv_sum norm ..
  _ ≤ ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (1 / m.factorial) := by
    simp_rw [Complex.norm_mul, Complex.norm_pow, Complex.norm_div, norm_natCast]
    gcongr
    rw [Complex.norm_pow]
    exact pow_le_one₀ (norm_nonneg _) hx
  _ = ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, (1 / m.factorial : ℝ) := by
    simp [abs_mul, abv_pow abs, abs_div, ← mul_sum]
  _ ≤ ‖x‖ ^ n * (n.succ * (n.factorial * n : ℝ)⁻¹) := by
    gcongr
    exact sum_div_factorial_le _ _ hn

Result:
no goals

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ filter (fun m => n ≤ m) (range j), ‖x‖ ^ n * (1 / ↑m.factorial) =
    ‖x‖ ^ n * ∑ m ∈ filter (fun m => n ≤ m) (range j), 1 / ↑m.factorial

Tactic:
simp [abs_mul, abv_pow abs, abs_div, ← mul_sum]

Result:
no goals

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ‖x‖ ^ n * ∑ m ∈ filter (fun m => n ≤ m) (range j), 1 / ↑m.factorial ≤ ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)

Tactic:
gcongr

Result:
case h
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ filter (fun m => n ≤ m) (range j), 1 / ↑m.factorial ≤ ↑n.succ * (↑n.factorial * ↑n)⁻¹

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ filter (fun m => n ≤ m) (range j), ‖x ^ n * (x ^ (m - n) / ↑m.factorial)‖ ≤
    ∑ m ∈ filter (fun m => n ≤ m) (range j), ‖x‖ ^ n * (1 / ↑m.factorial)

Tactic:
simp_rw [Complex.norm_mul, Complex.norm_pow, Complex.norm_div, norm_natCast]

Result:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ x_1 ∈ filter (fun m => n ≤ m) (range j), ‖x‖ ^ n * (‖x ^ (x_1 - n)‖ / ↑x_1.factorial) ≤
    ∑ m ∈ filter (fun m => n ≤ m) (range j), ‖x‖ ^ n * (1 / ↑m.factorial)

Proof state:
case h.h.hab
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
i✝ : ℕ
a✝ : i✝ ∈ filter (fun m => n ≤ m) (range j)
⊢ ‖x‖ ^ (i✝ - n) ≤ 1

Tactic:
exact pow_le_one₀ (norm_nonneg _) hx

Result:
no goals

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqNorm (exp' x - const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤
    ↑(const abs (‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹))) j

Tactic:
show
  ‖(∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial‖ ≤
    ‖x‖ ^ n * ((n.succ : ℝ) * (n.factorial * n : ℝ)⁻¹)

Result:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤
    ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)

Proof state:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤
    ↑(const abs (‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹))) j

Tactic:
simp_rw [← sub_eq_add_neg]

Result:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqNorm (exp' x - const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤
    ↑(const abs (‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹))) j