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

Proof state:
case e_a.refine_1
x : ℂ
n j : ℕ
hj : j ≥ n
a : ℕ
ha : a ∈ range (j - n)
⊢ (fun m hm => m + n) a ha ∈ filter (fun m => n ≤ m) (range j)

Tactic:
simp only [mem_filter, mem_range, le_add_iff_nonneg_left, zero_le, and_true]

Result:
case e_a.refine_1
x : ℂ
n j : ℕ
hj : j ≥ n
a : ℕ
ha : a ∈ range (j - n)
⊢ a + n < j

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

Result:
x : ℂ
n : ℕ
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))).lim ≤ ‖x‖ ^ n * Real.exp ‖x‖

Proof state:
x : ℂ
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 * (‖x‖ ^ (m - n) / ↑(m - n).factorial)

Tactic:
gcongr with i hi

Result:
case h.h.hac
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
hi : i ∈ filter (fun m => n ≤ m) (range j)
⊢ ‖x ^ (i - n)‖ ≤ ‖x‖ ^ (i - n)

case h.h.hdb.h.h
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
hi : i ∈ filter (fun m => n ≤ m) (range j)
⊢ i - n ≤ i

Proof state:
case h.h.hac
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
hi : i ∈ filter (fun m => n ≤ m) (range j)
⊢ ‖x ^ (i - n)‖ ≤ ‖x‖ ^ (i - n)

Tactic:
rw [Complex.norm_pow]

Result:
no goals

Proof state:
case e_a.refine_2
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ range (j - n)) (a₂ : ℕ) (ha₂ : a₂ ∈ range (j - n)),
    (fun m hm => m + n) a₁ ha₁ = (fun m hm => m + n) a₂ ha₂ → a₁ = a₂

Tactic:
intro a ha b hb hab

Result:
case e_a.refine_2
x : ℂ
n j : ℕ
hj : j ≥ n
a : ℕ
ha : a ∈ range (j - n)
b : ℕ
hb : b ∈ range (j - n)
hab : (fun m hm => m + n) a ha = (fun m hm => m + n) b hb
⊢ a = b

Proof state:
case e_a.refine_3
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b ∈ filter (fun m => n ≤ m) (range j)
⊢ ∃ a < j - n, a + n = b

Tactic:
simp only [mem_filter, mem_range] at hb

Result:
case e_a.refine_3
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
⊢ ∃ a < j - n, a + n = b

Proof state:
case e_a.refine_1
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∀ (a : ℕ) (ha : a ∈ range (j - n)), (fun m hm => m + n) a ha ∈ filter (fun m => n ≤ m) (range j)

Tactic:
intro a ha

Result:
case e_a.refine_1
x : ℂ
n j : ℕ
hj : j ≥ n
a : ℕ
ha : a ∈ range (j - n)
⊢ (fun m hm => m + n) a ha ∈ filter (fun m => n ≤ m) (range j)

Proof state:
case e_a.refine_4
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∀ (a : ℕ) (ha : a ∈ range (j - n)),
    ‖x‖ ^ a / ↑a.factorial = ‖x‖ ^ ((fun m hm => m + n) a ha - n) / ↑((fun m hm => m + n) a ha - n).factorial

Tactic:
simp

Result:
no goals

Proof state:
case e_a.refine_3.refine_1
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
⊢ b - n < j - n

Tactic:
rw [tsub_lt_tsub_iff_right hb.2]

Result:
case e_a.refine_3.refine_1
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
⊢ b < j

Proof state:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ ↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) j

Tactic:
rw [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‖ ≤ ↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) j

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

Tactic:
refine Real.sum_le_exp_of_nonneg ?_ _

Result:
case h
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ 0 ≤ ‖x‖

Proof state:
case h
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ 0 ≤ ‖x‖

Tactic:
exact norm_nonneg _

Result:
no goals

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

Tactic:
congr 1

Result:
case e_a
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ filter (fun m => n ≤ m) (range j), ‖x‖ ^ (m - n) / ↑(m - n).factorial =
    ∑ m ∈ range (j - 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 (‖x‖ ^ n * Real.exp ‖x‖)) 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 (‖x‖ ^ n * Real.exp ‖x‖)) j

Proof state:
case e_a.refine_3
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
⊢ ∃ a < j - n, a + n = b

Tactic:
refine ⟨b - n, ?_, ?_⟩

Result:
case e_a.refine_3.refine_1
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
⊢ b - n < j - n

case e_a.refine_3.refine_2
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
⊢ b - n + n = b

Proof state:
x : ℂ
n : ℕ
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))).lim ≤ ‖x‖ ^ n * Real.exp ‖x‖

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 (‖x‖ ^ n * Real.exp ‖x‖)) j

Proof state:
case e_a.refine_3.refine_1
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
⊢ b < j

Tactic:
exact hb.1

Result:
no goals

Proof state:
case e_a.refine_3
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b ∈ filter (fun m => n ≤ m) (range j)
⊢ ∃ a, ∃ (ha : a ∈ range (j - n)), (fun m hm => m + n) a ha = b

Tactic:
simp only [mem_range, exists_prop]

Result:
case e_a.refine_3
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b ∈ filter (fun m => n ≤ m) (range j)
⊢ ∃ a < j - n, a + n = b

Proof state:
x : ℂ
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 * (‖x‖ ^ (m - n) / ↑(m - n).factorial)

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

Result:
x : ℂ
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 * (‖x‖ ^ (m - n) / ↑(m - n).factorial)

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

Tactic:
refine (sum_bij (fun m hm ↦ m + n) ?_ ?_ ?_ ?_).symm

Result:
case e_a.refine_1
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∀ (a : ℕ) (ha : a ∈ range (j - n)), (fun m hm => m + n) a ha ∈ filter (fun m => n ≤ m) (range j)

case e_a.refine_2
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ range (j - n)) (a₂ : ℕ) (ha₂ : a₂ ∈ range (j - n)),
    (fun m hm => m + n) a₁ ha₁ = (fun m hm => m + n) a₂ ha₂ → a₁ = a₂

case e_a.refine_3
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∀ b ∈ filter (fun m => n ≤ m) (range j), ∃ a, ∃ (ha : a ∈ range (j - n)), (fun m hm => m + n) a ha = b

case e_a.refine_4
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∀ (a : ℕ) (ha : a ∈ range (j - n)),
    ‖x‖ ^ a / ↑a.factorial = ‖x‖ ^ ((fun m hm => m + n) a ha - n) / ↑((fun m hm => m + n) a ha - n).factorial

Proof state:
case h.h.hdb.h.h
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
hi : i ∈ filter (fun m => n ≤ m) (range j)
⊢ i - n ≤ i

Tactic:
simp

Result:
no goals

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

Tactic:
gcongr

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

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

Tactic:
rw [← mul_sum]

Result:
no goals

Proof state:
x : ℂ
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 : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)