awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 1
h₂ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 0
h₃ : HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) ≠ 0
h₄ : HSub.hSub (α := α) (↑n.succ : α) 1 = (↑n : α)
rw :
  (↑n.factorial : α)⁻¹ *
      ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
        ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) =
    ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)
rw₁ :
  (↑n.factorial : α)⁻¹ *
        ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
          ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) *
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
rw₂ :
  HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
      ((↑n.factorial : α)⁻¹ *
        ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
          ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α)))) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
rw₃ :
  HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
      ((↑n.factorial : α)⁻¹ * (HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
        ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
rw₄ :
  HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
      ((HSub.hSub (α := α) (↑n.succ : α) 1 * (↑n.factorial : α))⁻¹ *
        ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
⊢ HMul.hMul (α := α) (↑n.factorial : α)⁻¹ (∑ m ∈ range (j - n), HPow.hPow (α := α) (↑n.succ : α)⁻¹ m) =
    ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)
have rw₅ : HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
    ((HMul.hMul (α := α) (↑n : α) (↑n.factorial : α))⁻¹ *
      ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) =
  (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
Tactic: rw [geom_sum_inv h₁ h₂, eq_div_iff_mul_eq h₃, mul_comm _ (n.factorial * n : α),
          ← mul_assoc (n.factorial⁻¹ : α), ← mul_inv_rev, h₄, ← mul_assoc (n.factorial * n : α),
          mul_comm (n : α) n.factorial, mul_inv_cancel₀ h₃, one_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 1
h₂ : Ne.{u_1 + 1} (α := α) (↑n.succ : α) 0
h₃ : HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) ≠ 0
h₄ : HSub.hSub (α := α) (↑n.succ : α) 1 = (↑n : α)
rw :
  (↑n.factorial : α)⁻¹ *
      ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
        ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) =
    ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)
rw₁ :
  (↑n.factorial : α)⁻¹ *
        ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
          ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) *
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
rw₂ :
  HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
      ((↑n.factorial : α)⁻¹ *
        ((HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
          ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α)))) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
rw₃ :
  HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
      ((↑n.factorial : α)⁻¹ * (HSub.hSub (α := α) (↑n.succ : α) 1)⁻¹ *
        ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
rw₄ :
  HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
      ((HSub.hSub (α := α) (↑n.succ : α) 1 * (↑n.factorial : α))⁻¹ *
        ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
rw₅ :
  HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) *
      ((HMul.hMul (α := α) (↑n : α) (↑n.factorial : α))⁻¹ *
        ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α))) =
    (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
⊢ HMul.hMul (α := α) (↑n.factorial : α)⁻¹ (∑ m ∈ range (j - n), HPow.hPow (α := α) (↑n.succ : α)⁻¹ m) =
    ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)
have rw₆ : HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) * (HMul.hMul (α := α) (↑n : α) (↑n.factorial : α))⁻¹ *
    ((↑n.succ : α) - HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) * (↑n.succ : α)) =
  (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
Tactic: rw [geom_sum_inv h₁ h₂, eq_div_iff_mul_eq h₃, mul_comm _ (n.factorial * n : α),
          ← mul_assoc (n.factorial⁻¹ : α), ← mul_inv_rev, h₄, ← mul_assoc (n.factorial * n : α),
          mul_comm (n : α) n.factorial, mul_inv_cancel₀ h₃, one_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ ((↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)) /
      HMul.hMul (α := α) (↑n.factorial : α) (↑n : α) ≤
    (↑n.succ : α) / HMul.hMul (α := α) (↑n.factorial : α) (↑n : α)
have hab : (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) ≤ (↑n.succ : α)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ (↑n.succ : α) - (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n) ≤ (↑n.succ : α)
have hab : 0 ≤ (↑n.succ : α) * HPow.hPow (α := α) (↑n.succ : α)⁻¹ (j - n)
Tactic: apply sub_le_self
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)‖ ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)
have rw : (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤
  ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)
Tactic: rw [← lim_const (abv := norm) (∑ m ∈ range n, _), exp, sub_eq_add_neg,
    ← lim_neg, lim_add, ← lim_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
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 : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)
have refine : ∀ (j : ℕ) (hj : j ≥ n),
  (↑(cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))) : ℕ → ℝ) j ≤
    (↑(const abs (‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹))) : ℕ → ℝ) j
Tactic: refine lim_le (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ‖HSub.hSub (α := ℂ) (∑ m ∈ range j, x ^ m / (↑m.factorial : ℂ)) (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ))‖ ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)
have rw : norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
  ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)
Tactic: rw [sum_range_sub_sum_range hj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < 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 : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < 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 : ℂ
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 : ℂ))
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 : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < 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 : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < 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 : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < 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 * HDiv.hDiv (α := ℝ) 1 (↑m.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 * HDiv.hDiv (α := ℝ) 1 (↑m.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 : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < 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 * HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ))
have h : ∀ i ∈ {m ∈ range j | n ≤ m}, ‖x ^ (i - n)‖ ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
i : ℕ
h : i ∈ {m ∈ range j | n ≤ m}
⊢ ‖x ^ (i - n)‖ ≤ 1
have h : ‖x‖ ^ (i - n) ≤ 1
Tactic: rw [Complex.norm_pow]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ) ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)
have hbc : ∑ m ∈ range j with n ≤ m, HDiv.hDiv (α := ℝ) 1 (↑m.factorial : ℝ) ≤
  (↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)
have 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 : ℂ)))
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 : ℂ)))
⊢ norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)
have 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 : ℝ))
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 : ℝ))
⊢ norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)
have 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 : ℝ)
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 : ℝ)
⊢ norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    ‖x‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)
have m₃ : ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, HDiv.hDiv (α := ℝ) 1 (↑m.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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
⊢ ‖cexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)‖ ≤ ‖x‖ ^ n / (↑n.factorial : ℝ) * 2
have rw : (cauSeqNorm (exp' x + -const norm (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ)))).lim ≤ ‖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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
have 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
Tactic: refine lim_le (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
x : ℂ
n : ℕ
hx : ‖x‖ / (↑n.succ : ℝ) ≤ 1 / 2
j : ℕ
hj : j ≥ n
k : ℕ := j - n
⊢ ‖HSub.hSub (α := ℂ) (∑ m ∈ range j, x ^ m / (↑m.factorial : ℂ)) (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ))‖ ≤
    ‖x‖ ^ n / (↑n.factorial : ℝ) * 2
have hj₁ : j = n + k
Tactic: have hj : j = n + k := (add_tsub_cancel_of_le hj).symm
-- 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
⊢ ‖HSub.hSub (α := ℂ) (∑ m ∈ range j, x ^ m / (↑m.factorial : ℂ)) (∑ m ∈ range n, x ^ m / (↑m.factorial : ℂ))‖ ≤
    ‖x‖ ^ n / (↑n.factorial : ℝ) * 2
have rw : norm (E := ℂ) (∑ k ∈ range k, x ^ (n + k) / (↑(n + k).factorial : ℂ)) ≤ ‖x‖ ^ n / (↑n.factorial : ℝ) * 2
Tactic: rw [hj, sum_range_add_sub_sum_range]
-- 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
⊢ norm (E := ℂ) (∑ k ∈ range k, x ^ (n + k) / (↑(n + k).factorial : ℂ)) ≤ ‖x‖ ^ n / (↑n.factorial : ℝ) * 2
have 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))
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 := ?_
-- 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_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))
⊢ norm (E := ℂ) (∑ k ∈ range k, x ^ (n + k) / (↑(n + k).factorial : ℂ)) ≤ ‖x‖ ^ n / (↑n.factorial : ℝ) * 2
have 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))
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 := ?_
-- 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_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))
⊢ norm (E := ℂ) (∑ k ∈ range k, x ^ (n + k) / (↑(n + k).factorial : ℂ)) ≤ ‖x‖ ^ n / (↑n.factorial : ℝ) * 2
have calc_3 : ∑ i ∈ range k, ‖x‖ ^ n / (↑n.factorial : ℝ) * (‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i) ≤
  ‖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 := ?_
-- 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‖ ^ (n + i) / (↑(n + i).factorial : ℝ))
    (∑ i ∈ range k, ‖x‖ ^ (n + i) / ((↑n.factorial : ℝ) * HPow.hPow (α := ℝ) (↑n.succ : ℝ) i))
have calc_1 : ∀ i ∈ range k, (↑n.factorial : ℝ) * HPow.hPow (α := ℝ) (↑n.succ : ℝ) i ≤ (↑(n + i).factorial : ℝ)
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
⊢ ∑ i ∈ range k, ‖x‖ ^ n / (↑n.factorial : ℝ) * (‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i) ≤
    ‖x‖ ^ n / (↑n.factorial : ℝ) * 2
have calc_3 : ‖x‖ ^ n / (↑n.factorial : ℝ) * ∑ i ∈ range k, ‖x‖ ^ i / HPow.hPow (α := ℝ) (↑n.succ : ℝ) i ≤
  ‖x‖ ^ n / (↑n.factorial : ℝ) * 2
Tactic: rw [← mul_sum]