awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j with n ≤ m, HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ) ≤
    (↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹

Tactic:
exact sum_div_factorial_le _ _ hn

Premises used: Complex.sum_div_factorial_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
m :
  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 : ℂ)))
m₁ :
  LE.le (α := ℝ) (∑ m ∈ range j with n ≤ m, ‖x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))‖)
    (∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ))
m₂ :
  ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ) =
    ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ)
m₃ :
  ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ) ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)
⊢ norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑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 [← mul_sum]
    _ ≤ ‖x‖ ^ n * (n.succ * (n.factorial * n : ℝ)⁻¹) := by
      gcongr
      exact sum_div_factorial_le _ _ hn

Premises used: Norm.norm, HMul.hMul, Nat.cast, Finset.range, IsAbsoluteValue.abv_sum, Inv.inv, Nat.factorial, Nat.succ
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
rw :
  (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤ ‖x‖ ^ n / (↑n.factorial : ℝ) * 2
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)‖ ≤ ‖x‖ ^ n / (↑n.factorial : ℝ) * 2

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

Premises used: sub_eq_add_neg, CauSeq.lim_add, CauSeq.lim_const, Finset.range, Complex.exp, Complex.lim_norm, CauSeq.lim_neg, Finset.sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤ ‖x‖ ^ n / (↑n.factorial : ℝ) * 2

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

Premises used: CauSeq.le_of_exists, CauSeq.lim_le, Exists.intro
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
refine :
  ∀ (j : ℕ) (hj : j ≥ n),
    (↑(cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))) : ℕ → ℝ) j ≤
      (↑(const abs (‖x‖ ^ n / (↑n.factorial : ℝ) * 2)) : ℕ → ℝ) j
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤ ‖x‖ ^ n / (↑n.factorial : ℝ) * 2

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

Premises used: CauSeq.le_of_exists, CauSeq.lim_le, Exists.intro
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj : j ≥ n
k : ℕ := j - n
⊢ j = n + k

Tactic:
have hj : j = n + k := (add_tsub_cancel_of_le hj).symm
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
rw : norm (E := ℂ) (∑ k ∈ range k, x ^ (n + k) / (↑(n + k).factorial : ℂ)) ≤ ‖x‖ ^ n / (↑n.factorial : ℝ) * 2
⊢ ‖HSub.hSub (α := ℂ) (∑ m ∈ range j, x ^ m / (↑m.factorial : ℂ)) (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ))‖ ≤
    ‖x‖ ^ n / (↑n.factorial : ℝ) * 2

Tactic:
rw [hj, sum_range_add_sub_sum_range]

Premises used: Finset.sum_range_add_sub_sum_range
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ norm (E := ℂ) (∑ i ∈ range k, x ^ (n + i) / (↑(n + i).factorial : ℂ)) ≤
    ∑ i ∈ range k, ‖x ^ (n + i) / (↑(n + i).factorial : ℂ)‖

Tactic:
IsAbsoluteValue.abv_sum _ _ _

Premises used: IsAbsoluteValue.abv_sum
-- Module: Mathlib.Analysis.Complex.Exponential
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 ^ (n + i) / (↑(n + i).factorial : ℂ)‖)
    (∑ i ∈ range k, ‖x‖ ^ (n + i) / (↑(n + i).factorial : ℝ))

Tactic:
simp [norm_natCast, Complex.norm_pow]

Premises used: Complex.norm_pow, Complex.norm_natCast
-- Module: Mathlib.Analysis.Complex.Exponential
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‖ ^ (n + i) / (↑(n + i).factorial : ℝ))
    (∑ i ∈ range k, ‖x‖ ^ (n + i) / ((↑n.factorial : ℝ) * HPow.hPow (α := ℝ) (↑n.succ : ℝ) i))

Tactic:
?_
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ Eq (α := ℝ) (∑ i ∈ range k, ‖x‖ ^ (n + i) / ((↑n.factorial : ℝ) * HPow.hPow (α := ℝ) (↑n.succ : ℝ) i))
    (∑ i ∈ range k, ‖x‖ ^ n / (↑n.factorial : ℝ) * (‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i))

Tactic:
?_
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ∑ i ∈ range k, ‖x‖ ^ n / (↑n.factorial : ℝ) * (‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i) ≤
    ‖x‖ ^ n / (↑n.factorial : ℝ) * 2

Tactic:
?_
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
calc_1 :
  LE.le (α := ℝ) (∑ i ∈ range k, ‖x‖ ^ (n + i) / (↑(n + i).factorial : ℝ))
    (∑ i ∈ range k, ‖x‖ ^ (n + i) / ((↑n.factorial : ℝ) * HPow.hPow (α := ℝ) (↑n.succ : ℝ) i))
calc_2 :
  Eq (α := ℝ) (∑ i ∈ range k, ‖x‖ ^ (n + i) / ((↑n.factorial : ℝ) * HPow.hPow (α := ℝ) (↑n.succ : ℝ) i))
    (∑ i ∈ range k, ‖x‖ ^ n / (↑n.factorial : ℝ) * (‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i))
calc_3 :
  ∑ i ∈ range k, ‖x‖ ^ n / (↑n.factorial : ℝ) * (‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i) ≤
    ‖x‖ ^ n / (↑n.factorial : ℝ) * 2
⊢ norm (E := ℂ) (∑ k ∈ range k, x ^ (n + k) / (↑(n + k).factorial : ℂ)) ≤ ‖x‖ ^ n / (↑n.factorial : ℝ) * 2

Tactic:
calc
    ‖∑ i ∈ range k, x ^ (n + i) / ((n + i).factorial : ℂ)‖ ≤
        ∑ i ∈ range k, ‖x ^ (n + i) / ((n + i).factorial : ℂ)‖ :=
      IsAbsoluteValue.abv_sum _ _ _
    _ ≤ ∑ i ∈ range k, ‖x‖ ^ (n + i) / (n + i).factorial := by
      simp [norm_natCast, Complex.norm_pow]
    _ ≤ ∑ i ∈ range k, ‖x‖ ^ (n + i) / ((n.factorial : ℝ) * (n.succ : ℝ) ^ i) := ?_
    _ = ∑ i ∈ range k, ‖x‖ ^ n / n.factorial * (‖x‖ ^ i / (n.succ : ℝ) ^ i) := ?_
    _ ≤ ‖x‖ ^ n / ↑n.factorial * 2 := ?_

Premises used: Finset.range, IsAbsoluteValue.abv_sum, Nat.factorial
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
calc_1 : ∀ i ∈ range k, (↑n.factorial : ℝ) * HPow.hPow (α := ℝ) (↑n.succ : ℝ) i ≤ (↑(n + i).factorial : ℝ)
⊢ LE.le (α := ℝ) (∑ i ∈ range k, ‖x‖ ^ (n + i) / (↑(n + i).factorial : ℝ))
    (∑ i ∈ range k, ‖x‖ ^ (n + i) / ((↑n.factorial : ℝ) * HPow.hPow (α := ℝ) (↑n.succ : ℝ) i))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
i : ℕ
h : i ∈ range k
⊢ (↑n.factorial : ℝ) * HPow.hPow (α := ℝ) (↑n.succ : ℝ) i ≤ (↑(n + i).factorial : ℝ)

Tactic:
mod_cast Nat.factorial_mul_pow_le_factorial

Premises used: Nat.cast_mul._simp_1, HMul.hMul, congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.factorial_mul_pow_le_factorial, Nat.cast, HPow.hPow, HAdd.hAdd, Nat.factorial, congrFun', Eq.symm, Nat.succ, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
i : ℕ
h : i ∈ range k
⊢ (↑n.factorial : ℝ) * HPow.hPow (α := ℝ) (↑n.succ : ℝ) i ≤ (↑(n + i).factorial : ℝ)

Tactic:
exact mod_cast Nat.factorial_mul_pow_le_factorial

Premises used: Nat.factorial_mul_pow_le_factorial
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ Eq (α := ℝ) (∑ i ∈ range k, ‖x‖ ^ (n + i) / ((↑n.factorial : ℝ) * HPow.hPow (α := ℝ) (↑n.succ : ℝ) i))
    (∑ i ∈ range k, ‖x‖ ^ n / (↑n.factorial : ℝ) * (‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i))

Tactic:
simp only [pow_add, div_eq_inv_mul, mul_inv, mul_left_comm, mul_assoc]

Premises used: mul_inv, mul_assoc, pow_add, mul_left_comm, div_eq_inv_mul
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
calc_3 :
  ‖x‖ ^ n / (↑n.factorial : ℝ) * ∑ i ∈ range k, ‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i ≤
    ‖x‖ ^ n / (↑n.factorial : ℝ) * 2
⊢ ∑ i ∈ range k, ‖x‖ ^ n / (↑n.factorial : ℝ) * (‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i) ≤
    ‖x‖ ^ n / (↑n.factorial : ℝ) * 2

Tactic:
rw [← mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
calc_3 : LE.le (α := ℝ) (∑ i ∈ range k, ‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i) 2
⊢ ‖x‖ ^ n / (↑n.factorial : ℝ) * ∑ i ∈ range k, ‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i ≤
    ‖x‖ ^ n / (↑n.factorial : ℝ) * 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
calc_3 : LE.le (α := ℝ) (∑ x_1 ∈ range k, (‖x‖ / (↑n.succ : ℝ)) ^ x_1) 2
⊢ LE.le (α := ℝ) (∑ i ∈ range k, ‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i) 2

Tactic:
simp_rw [← div_pow]

Premises used: div_pow
-- Module: Mathlib.Analysis.Complex.Exponential
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
calc_3₂ : ‖x‖ / (↑n.succ : ℝ) ≠ 1
⊢ LE.le (α := ℝ) (∑ x_1 ∈ range k, (‖x‖ / (↑n.succ : ℝ)) ^ x_1) 2

Tactic:
rw [geom_sum_eq, div_le_iff_of_neg]

Premises used: div_le_iff_of_neg, geom_sum_eq
-- Module: Mathlib.Analysis.Complex.Exponential
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
trans₁ : -1 ≤ (‖x‖ / (↑n.succ : ℝ)) ^ k - 1
⊢ 2 * (‖x‖ / (↑n.succ : ℝ) - 1) ≤ (‖x‖ / (↑n.succ : ℝ)) ^ k - 1

Tactic:
trans (-1 : ℝ)

Premises used: OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Complex.Exponential
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
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
⊢ 2 * (‖x‖ / (↑n.succ : ℝ) - 1) ≤ -1

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
simp : 0 ≤ ‖x‖ ^ k / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ k
⊢ -1 ≤ (‖x‖ / (↑n.succ : ℝ)) ^ k - 1

Tactic:
simp only [neg_le_sub_iff_le_add, div_pow, Nat.cast_succ, le_add_iff_nonneg_left]

Premises used: Nat.cast_succ, div_pow, neg_le_sub_iff_le_add, le_add_iff_nonneg_left
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj_1 : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ 0 ≤ ‖x‖ ^ k / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ k

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Exponential
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
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
linarith₄ : 0 ≤ ‖x‖ / (↑n.succ : ℝ) - 1 → GT.gt (α := ℝ) 2 0
⊢ ‖x‖ / (↑n.succ : ℝ) - 1 < 0

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.Exponential
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
linarith₃ :
  ‖x‖ / (↑n.succ : ℝ) = 1 →
    -1 + (2 * (‖x‖ / (↑n.succ : ℝ)) - HMul.hMul (α := ℝ) 1 1) +
        2 * -(1 * (‖x‖ / (↑n.succ : ℝ)) - HMul.hMul (α := ℝ) 1 1) =
      0
linarith₄ : ‖x‖ / (↑n.succ : ℝ) = 1 → GT.gt (α := ℝ) 2 0
⊢ ‖x‖ / (↑n.succ : ℝ) ≠ 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp x - 1‖ = ‖cexp x - ∑ m ∈ range 1, x ^ m / (↑m.factorial : ℂ)‖

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ LT.lt (α := ℕ) 0 1

Tactic:
decide
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ HPow.hPow (β := ℕ) ‖x‖ 1 * ((↑(Nat.succ 1) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 1) : ℝ) (↑1 : ℝ))⁻¹) = 2 * ‖x‖

Tactic:
simp [mul_two, mul_add, mul_comm, Nat.factorial]

Premises used: Nat.factorial, mul_comm, mul_add, mul_two
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp x - 1 - x‖ = ‖cexp x - ∑ m ∈ range 2, x ^ m / (↑m.factorial : ℂ)‖

Tactic:
simp [sub_eq_add_neg, sum_range_succ_comm, add_assoc, Nat.factorial]

Premises used: add_assoc, sub_eq_add_neg, Finset.sum_range_succ_comm, Nat.factorial
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ LT.lt (α := ℕ) 0 2

Tactic:
decide
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
hbc : (↑(Nat.succ 2) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 2) : ℝ) (↑2 : ℝ))⁻¹ ≤ 1
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * ((↑(Nat.succ 2) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 2) : ℝ) (↑2 : ℝ))⁻¹) ≤
    HPow.hPow (β := ℕ) ‖x‖ 2 * 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ (↑(Nat.succ 2) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 2) : ℝ) (↑2 : ℝ))⁻¹ ≤ 1

Tactic:
norm_num [Nat.factorial]

Premises used: Nat.factorial
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
rw rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 * 1 = HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖Real.exp x - 1 - x‖ = ‖(↑(Real.exp x) : ℂ) - 1 - (↑x : ℂ)‖

Tactic:
exact_mod_cast Complex.norm_real _

Premises used: Complex.norm_real
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖(↑(Real.exp x) : ℂ) - 1 - (↑x : ℂ)‖ = ‖cexp (↑x : ℂ) - 1 - (↑x : ℂ)‖

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖(↑x : ℂ)‖ ≤ 1

Tactic:
exact_mod_cast hx
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : ‖x‖ ≤ 1
⊢ HPow.hPow (β := ℕ) ‖(↑x : ℂ)‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
rw :
  (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤
    Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / (↑m.factorial : ℝ)
⊢ ‖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]

Premises used: sub_eq_add_neg, CauSeq.lim_add, CauSeq.lim_const, Finset.range, Complex.exp, Complex.lim_norm, CauSeq.lim_neg, Finset.sum
-- Module: Mathlib.Analysis.Complex.Exponential
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 : ℝ)

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

Premises used: CauSeq.le_of_exists, CauSeq.lim_le, Exists.intro
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
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
⊢ (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 => ?_⟩)

Premises used: CauSeq.le_of_exists, CauSeq.lim_le, Exists.intro
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
rw :
  norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    ∑ k ∈ range j with n ≤ k, ‖x‖ ^ k / (↑k.factorial : ℝ)
⊢ ‖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:
rw [sum_range_sub_sum_range hj, sum_range_sub_sum_range hj]

Premises used: Finset.sum_range_sub_sum_range
-- Module: Mathlib.Analysis.Complex.Exponential
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 : ℝ)

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

Premises used: Norm.norm, LE.le.trans_eq, IsAbsoluteValue.abv_sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
refine :
  Eq (α := ℝ) (∑ i ∈ range j with n ≤ i, ‖x ^ i / (↑i.factorial : ℂ)‖)
    (∑ k ∈ range j with n ≤ k, ‖x‖ ^ k / (↑k.factorial : ℝ))
⊢ norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    ∑ k ∈ range j with n ≤ k, ‖x‖ ^ k / (↑k.factorial : ℝ)

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

Premises used: Norm.norm, LE.le.trans_eq, IsAbsoluteValue.abv_sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
e_f : ∀ (i : ℕ), ‖x ^ i / (↑i.factorial : ℂ)‖ = ‖x‖ ^ i / (↑i.factorial : ℝ)
⊢ Eq (α := ℝ) (∑ i ∈ range j with n ≤ i, ‖x ^ i / (↑i.factorial : ℂ)‖)
    (∑ k ∈ range j with n ≤ k, ‖x‖ ^ k / (↑k.factorial : ℝ))

Tactic:
congr with i
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
⊢ ‖x ^ i / (↑i.factorial : ℂ)‖ = ‖x‖ ^ i / (↑i.factorial : ℝ)

Tactic:
simp [Complex.norm_pow, Complex.norm_natCast]

Premises used: Complex.norm_pow, Complex.norm_natCast
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
h : ∑ m ∈ range j, ‖x‖ ^ m / (↑m.factorial : ℝ) ≤ Real.exp ‖x‖
⊢ 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:
gcongr
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range j, ‖x‖ ^ m / (↑m.factorial : ℝ) ≤ Real.exp ‖x‖

Tactic:
Real.sum_le_exp_of_nonneg (norm_nonneg _) _

Premises used: Real.sum_le_exp_of_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
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 _) _

Premises used: Real.sum_le_exp_of_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.Complex.Exponential
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 : ℝ))
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 : ℝ)
⊢ (↑(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, Complex.norm_natCast]
  _ ≤ Real.exp ‖x‖ - ∑ m ∈ range n, ‖x‖ ^ m / m.factorial := by
    gcongr
    exact Real.sum_le_exp_of_nonneg (norm_nonneg _) _

Premises used: Norm.norm, HDiv.hDiv, Real.exp, Nat.cast, Finset.range, HPow.hPow, Nat.factorial, Finset.sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
⊢ ‖cexp x - ∑ m ∈ range 0, x ^ m / (↑m.factorial : ℂ)‖ ≤ Real.exp ‖x‖ - ∑ m ∈ range 0, ‖x‖ ^ m / (↑m.factorial : ℝ)

Tactic:
norm_exp_sub_sum_le_exp_norm_sub_sum x 0

Premises used: Complex.norm_exp_sub_sum_le_exp_norm_sub_sum, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
h : ‖cexp x‖ = ‖cexp x - ∑ m ∈ range 0, x ^ m / (↑m.factorial : ℂ)‖
h₁ : Real.exp ‖x‖ = Real.exp ‖x‖ - ∑ m ∈ range 0, ‖x‖ ^ m / (↑m.factorial : ℝ)
⊢ ‖cexp x‖ ≤ Real.exp ‖x‖

Tactic:
convert! norm_exp_sub_sum_le_exp_norm_sub_sum x 0 using 1

Premises used: Complex.norm_exp_sub_sum_le_exp_norm_sub_sum, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
⊢ ‖cexp x‖ = ‖cexp x - ∑ m ∈ range 0, x ^ m / (↑m.factorial : ℂ)‖

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
⊢ Real.exp ‖x‖ = Real.exp ‖x‖ - ∑ m ∈ range 0, ‖x‖ ^ m / (↑m.factorial : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
rw : (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤ ‖x‖ ^ n * Real.exp ‖x‖
⊢ ‖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]

Premises used: sub_eq_add_neg, CauSeq.lim_add, CauSeq.lim_const, Finset.range, Complex.exp, Complex.lim_norm, CauSeq.lim_neg, Finset.sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
⊢ (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤ ‖x‖ ^ n * Real.exp ‖x‖

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

Premises used: CauSeq.le_of_exists, CauSeq.lim_le, Exists.intro
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n : ℕ
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
⊢ (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 => ?_⟩)

Premises used: CauSeq.le_of_exists, CauSeq.lim_le, Exists.intro