-- Mathlib/Data/Complex/Exponential.lean
lemma norm_exp_sub_sum_le_exp_norm_sub_sum (x : ℂ) (n : ℕ) :
    ‖exp x - ∑ m ∈ range n, x ^ m / m.factorial‖
      ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial

Proof state:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ i ∈ filter (fun k => n ≤ k) (range j), ‖x ^ i / ↑i.factorial‖ =
    ∑ k ∈ filter (fun k => n ≤ k) (range j), ‖x‖ ^ k / ↑k.factorial

Tactic:
congr with i

Result:
case e_f.h
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
⊢ ‖x ^ i / ↑i.factorial‖ = ‖x‖ ^ i / ↑i.factorial

Proof state:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ 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:
gcongr

Result:
case h
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j, ‖x‖ ^ m / ↑m.factorial ≤ Real.exp ‖x‖

Proof state:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ k ∈ filter (fun k => n ≤ k) (range j), x ^ k / ↑k.factorial‖ ≤
    ∑ k ∈ filter (fun k => n ≤ k) (range j), ‖x‖ ^ k / ↑k.factorial

Tactic:
refine (IsAbsoluteValue.abv_sum norm ..).trans_eq ?_

Result:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ i ∈ filter (fun k => n ≤ k) (range j), ‖x ^ i / ↑i.factorial‖ =
    ∑ k ∈ filter (fun k => n ≤ k) (range j), ‖x‖ ^ k / ↑k.factorial

Proof state:
x : ℂ
n : ℕ
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ 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]

Result:
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

Proof state:
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

Tactic:
simp_rw [← sub_eq_add_neg]

Result:
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

Proof state:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ 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

Tactic:
rw [sum_range_sub_sum_range hj, sum_range_sub_sum_range hj]

Result:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ k ∈ filter (fun k => n ≤ k) (range j), x ^ k / ↑k.factorial‖ ≤
    ∑ k ∈ filter (fun k => n ≤ k) (range j), ‖x‖ ^ k / ↑k.factorial

Proof state:
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

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

Result:
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

Proof state:
case e_f.h
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
⊢ ‖x ^ i / ↑i.factorial‖ = ‖x‖ ^ i / ↑i.factorial

Tactic:
simp [Complex.norm_pow]

Result:
no goals

Proof state:
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

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]
_ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial := by
  gcongr
  exact Real.sum_le_exp_of_nonneg (norm_nonneg _) _

Result:
no goals

Proof state:
case h
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j, ‖x‖ ^ m / ↑m.factorial ≤ Real.exp ‖x‖

Tactic:
exact Real.sum_le_exp_of_nonneg (norm_nonneg _) _

Result:
no goals