awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℂ)) ≤
    (↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) : ℕ → ℝ) j
⊢ ‖HSub.hSub (α := ℂ) (∑ 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]

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

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

Premises used: Norm.norm, congr_arg, Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
refine :
  ∀ (m : ℕ) (hm : m ∈ {m ∈ range j | n ≤ m}), x ^ m / (↑m.factorial : ℂ) = x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))
⊢ 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:
refine congr_arg norm (sum_congr rfl fun m hm => ?_)

Premises used: Norm.norm, congr_arg, Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ {m ∈ range j | n ≤ m}
⊢ m < j ∧ n ≤ m

Tactic:
rw [mem_filter, mem_range] at hm

Premises used: Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
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 : ℂ)
rw₂ rw₃ : x ^ m / (↑m.factorial : ℂ) = x ^ m / (↑m.factorial : ℂ)
⊢ 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]

Premises used: mul_div_assoc, pow_add, And.right, add_tsub_cancel_of_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ norm (E := ℂ) (∑ m ∈ range j with n ≤ m, x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))) ≤
    ∑ m ∈ range j with n ≤ m, ‖x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))‖

Tactic:
IsAbsoluteValue.abv_sum norm ..

Premises used: Norm.norm, IsAbsoluteValue.abv_sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
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 * (‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)))
⊢ LE.le (α := ℝ) (∑ m ∈ range j with n ≤ m, ‖x ^ n * (x ^ (m - n) / (↑m.factorial : ℂ))‖)
    (∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)))

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

Premises used: Complex.norm_pow, Complex.norm_natCast, Complex.norm_div, Complex.norm_mul
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
h : ∀ (i : ℕ) (hi : i ∈ {m ∈ range j | n ≤ m}), ‖x ^ (i - n)‖ ≤ ‖x‖ ^ (i - n)
h₁ : ∀ (i : ℕ) (hi : i ∈ {m ∈ range j | n ≤ m}), i - n ≤ i
⊢ 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 * (‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)))

Tactic:
gcongr with i hi
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
hi : i ∈ {m ∈ range j | n ≤ m}
h h₁ : ‖x‖ ^ (i - n) ≤ ‖x‖ ^ (i - n)
⊢ ‖x ^ (i - n)‖ ≤ ‖x‖ ^ (i - n)

Tactic:
rw [Complex.norm_pow]

Premises used: Complex.norm_pow
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
i : ℕ
hi : i ∈ {m ∈ range j | n ≤ m}
⊢ i - n ≤ i

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
rw rw₁ :
  ‖x‖ ^ n * ∑ i ∈ range j with n ≤ i, ‖x‖ ^ (i - n) / (↑(i - n).factorial : ℝ) =
    ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)
⊢ ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)) =
    ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)

Tactic:
rw [← mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
e_a :
  Eq (α := ℝ) (∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ))
    (∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ))
⊢ ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ) =
    ‖x‖ ^ n * ∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ)

Tactic:
congr 1
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ Eq (α := ℝ) (∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ))
    (∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ))

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

Premises used: Finset.sum_bij, HAdd.hAdd, Eq.symm
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
e_a : ∀ (a : ℕ) (ha : a ∈ range (j - n)), (fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha ∈ {m ∈ range j | n ≤ m}
e_a₁ :
  ∀ (a₁ : ℕ) (ha₁ : a₁ ∈ range (j - n)) (a₂ : ℕ) (ha₂ : a₂ ∈ range (j - n)),
    Eq (α := ℕ) ((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a₁ ha₁)
        ((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a₂ ha₂) →
      a₁ = a₂
e_a₂ :
  ∀ b ∈ {m ∈ range j | n ≤ m},
    ∃ (a : ℕ) (ha : a ∈ range (j - n)), (fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha = b
e_a₃ :
  ∀ (a : ℕ) (ha : a ∈ range (j - n)),
    ‖x‖ ^ a / (↑a.factorial : ℝ) =
      ‖x‖ ^ ((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha - n) /
        (↑((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha - n).factorial : ℝ)
⊢ Eq (α := ℝ) (∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ))
    (∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ))

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

Premises used: Finset.sum_bij, HAdd.hAdd, Eq.symm
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∀ (a : ℕ) (ha : a ∈ range (j - n)), (fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha ∈ {m ∈ range j | n ≤ m}

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
a : ℕ
ha : a ∈ range (j - n)
b : ℕ
hb : b ∈ range (j - n)
hab :
  Eq (α := ℕ) ((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha)
    ((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) b hb)
⊢ a = b

Tactic:
simpa using hab
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b ∈ {m ∈ range j | n ≤ m}
e_a : ∃ a < j - n, a + n = b
⊢ ∃ (a : ℕ) (ha : a ∈ range (j - n)), (fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha = b

Tactic:
simp only [mem_range, exists_prop]

Premises used: Finset.mem_range, exists_prop
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b ∈ {m ∈ range j | n ≤ m}
⊢ b < j ∧ n ≤ b

Tactic:
simp only [mem_filter, mem_range] at hb

Premises used: Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
⊢ ∃ a < j - n, a + n = b

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

Premises used: HSub.hSub, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
e_a : b - n < j - n
e_a₁ : b - n + n = b
⊢ ∃ a < j - n, a + n = b

Tactic:
refine ⟨b - n, ?_, ?_⟩
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
e_a : b < j
⊢ b - n < j - n

Tactic:
rw [tsub_lt_tsub_iff_right hb.2]

Premises used: And.right, tsub_lt_tsub_iff_right
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
⊢ b < j

Tactic:
hb.1

Premises used: And.left
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
⊢ b < j

Tactic:
exact hb.1

Premises used: And.left
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
e_a e_a₁ : b = b
⊢ b - n + n = b

Tactic:
rw [tsub_add_cancel_of_le hb.2]

Premises used: tsub_add_cancel_of_le, And.right
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∀ (a : ℕ) (ha : a ∈ range (j - n)),
    ‖x‖ ^ a / (↑a.factorial : ℝ) =
      ‖x‖ ^ ((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha - n) /
        (↑((fun (m : ℕ) (hm : m ∈ range (j - n)) ↦ m + n) a ha - n).factorial : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
hbc : ∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ) ≤ Real.exp ‖x‖
⊢ ‖x‖ ^ n * ∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ) ≤ ‖x‖ ^ n * Real.exp ‖x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ) ≤ Real.exp ‖x‖

Tactic:
Real.sum_le_exp_of_nonneg ?_ _

Premises used: Real.sum_le_exp_of_nonneg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
hbc : 0 ≤ ‖x‖
⊢ ∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ) ≤ Real.exp ‖x‖

Tactic:
refine Real.sum_le_exp_of_nonneg ?_ _

Premises used: Real.sum_le_exp_of_nonneg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ 0 ≤ ‖x‖

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ 0 ≤ ‖x‖

Tactic:
exact norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℂ
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 * (‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)))
m₂ :
  ∑ m ∈ range j with n ≤ m, ‖x‖ ^ n * (‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)) =
    ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ)
m₃ :
  ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, ‖x‖ ^ (m - n) / (↑(m - n).factorial : ℝ) =
    ‖x‖ ^ n * ∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ)
m₄ : ‖x‖ ^ n * ∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ) ≤ ‖x‖ ^ n * Real.exp ‖x‖
⊢ norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    (↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) : ℕ → ℝ) j

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 * (‖x‖ ^ (m - n) / (m - n).factorial) := by
      simp_rw [Complex.norm_mul, Complex.norm_pow, Complex.norm_div, norm_natCast]
      gcongr with i hi
      · rw [Complex.norm_pow]
      · simp
    _ = ‖x‖ ^ n * ∑ m ∈ range j with n ≤ m, (‖x‖ ^ (m - n) / (m - n).factorial) := by
      rw [← mul_sum]
    _ = ‖x‖ ^ n * ∑ m ∈ range (j - n), (‖x‖ ^ m / m.factorial) := by
      congr 1
      refine (sum_bij (fun m hm ↦ m + n) ?_ ?_ ?_ ?_).symm
      · grind
      · intro a ha b hb hab
        simpa using hab
      · intro b hb
        simp only [mem_range, exists_prop]
        simp only [mem_filter, mem_range] at hb
        refine ⟨b - n, ?_, ?_⟩
        · rw [tsub_lt_tsub_iff_right hb.2]
          exact hb.1
        · rw [tsub_add_cancel_of_le hb.2]
      · simp
    _ ≤ ‖x‖ ^ n * Real.exp ‖x‖ := by
      gcongr
      refine Real.sum_le_exp_of_nonneg ?_ _
      exact norm_nonneg _

Premises used: Norm.norm, HSub.hSub, Real.exp, Finset.range, IsAbsoluteValue.abv_sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
⊢ ‖(↑x : ℂ)‖ ≤ 1

Tactic:
have hxc : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖(↑x : ℂ)‖ ≤ 1
⊢ ‖cexp (↑x : ℂ) - ∑ m ∈ range n, (↑x : ℂ) ^ m / (↑m.factorial : ℂ)‖ ≤
    ‖(↑x : ℂ)‖ ^ n * ((↑n.succ : ℝ) * (HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))⁻¹)

Tactic:
exp_bound hxc hn

Premises used: Complex.exp_bound
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖(↑x : ℂ)‖ ≤ 1
h :
  |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| =
    ‖cexp (↑x : ℂ) - ∑ m ∈ range n, (↑x : ℂ) ^ m / (↑m.factorial : ℂ)‖
h₁ : |x| ^ n = ‖(↑x : ℂ)‖ ^ n
⊢ |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| ≤
    |x| ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))

Tactic:
convert! exp_bound hxc hn using 2
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖(↑x : ℂ)‖ ≤ 1
h h₁ h₂ h₃ : |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| = ‖rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)‖
⊢ |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| =
    ‖cexp (↑x : ℂ) - ∑ m ∈ range n, (↑x : ℂ) ^ m / (↑m.factorial : ℂ)‖

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖(↑x : ℂ)‖ ≤ 1
h h₁ h₂ h₃ : |x| ^ n = ‖x‖ ^ n
⊢ |x| ^ n = ‖(↑x : ℂ)‖ ^ n

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
⊢ |x| = x

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
⊢ |x| = x

Tactic:
have h3 : |x| = x := by simpa
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
rwa rwa₁ rwa₂ rwa₃ : x ≤ 1
⊢ |x| ≤ 1

Tactic:
rwa [h3]
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
⊢ |x| ≤ 1

Tactic:
have h4 : |x| ≤ 1 := by rwa [h3]
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
⊢ |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| ≤
    |x| ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))

Tactic:
have h' := Real.exp_bound h4 hn
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
h' :
  |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| ≤
    |x| ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))
⊢ |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| ≤
    x ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))

Tactic:
rw [h3] at h'
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
h' :
  |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| ≤
    x ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))
⊢ rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ) ≤
    x ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))

Tactic:
have h'' := (abs_sub_le_iff.1 h').1
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
h' :
  |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| ≤
    x ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))
h'' :
  rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ) ≤
    x ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))
⊢ rexp x ≤
    ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ) + x ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))

Tactic:
have t := sub_le_iff_le_add'.1 h''
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
h4 : |x| ≤ 1
h' :
  |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| ≤
    x ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))
h'' :
  rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ) ≤
    x ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))
t :
  rexp x ≤
    ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ) + x ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))
⊢ rexp x ≤
    ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ) +
      x ^ n * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ)

Tactic:
simpa [mul_div_assoc] using t

Premises used: mul_div_assoc
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : |x| ≤ 1
⊢ ‖(↑x : ℂ)‖ ≤ 1

Tactic:
have : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : |x| ≤ 1
this : ‖(↑x : ℂ)‖ ≤ 1
⊢ |rexp x - 1| ≤ 2 * |x|

Tactic:
exact_mod_cast Complex.norm_exp_sub_one_le (x := x) this

Premises used: Complex.norm_exp_sub_one_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : |x| ≤ 1
rw : |rexp x - 1 - x| ≤ HPow.hPow (β := ℕ) |x| 2
⊢ |rexp x - 1 - x| ≤ HPow.hPow (β := ℕ) x 2

Tactic:
rw [← sq_abs]

Premises used: sq_abs
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : |x| ≤ 1
this : ‖(↑x : ℂ)‖ ≤ 1
⊢ |rexp x - 1 - x| ≤ HPow.hPow (β := ℕ) |x| 2

Tactic:
exact_mod_cast Complex.norm_exp_sub_one_sub_id_le this

Premises used: Complex.norm_exp_sub_one_sub_id_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x r : ℝ
⊢ expNear 0 x r = r

Tactic:
simp [expNear]

Premises used: Real.expNear
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
x r : ℝ
simp :
  x ^ n * x * ((↑n.factorial : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹) * r =
    x ^ n * (↑n.factorial : ℝ)⁻¹ * (x * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * r)
⊢ expNear (n + 1) x r = expNear n x (1 + x / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * r)

Tactic:
simp [expNear, range_add_one, mul_add, add_left_comm, add_assoc, pow_succ, div_eq_mul_inv,
    Nat.factorial]

Premises used: Real.expNear, add_left_comm, pow_succ, add_assoc, Finset.range_add_one, div_eq_mul_inv, Nat.factorial, mul_add
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
x r : ℝ
⊢ x ^ n * x * ((↑n.factorial : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹) * r =
    x ^ n * (↑n.factorial : ℝ)⁻¹ * (x * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * r)

Tactic:
ac_rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
x r₁ r₂ : ℝ
⊢ expNear n x r₁ - expNear n x r₂ = x ^ n / (↑n.factorial : ℝ) * (r₁ - r₂)

Tactic:
simp [expNear, mul_sub]

Premises used: Real.expNear, mul_sub
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
simp :
  |rexp x - ∑ m ∈ range m, x ^ m / (↑m.factorial : ℝ)| ≤
    |x| ^ m / (↑m.factorial : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))
⊢ |rexp x - expNear m x 0| ≤ |x| ^ m / (↑m.factorial : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))

Tactic:
simp only [expNear, mul_zero, add_zero]

Premises used: Real.expNear, MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ |rexp x - ∑ m ∈ range m, x ^ m / (↑m.factorial : ℝ)| ≤
    |x| ^ m * ((↑m.succ : ℝ) / HMul.hMul (α := ℝ) (↑m.factorial : ℝ) (↑m : ℝ))

Tactic:
exp_bound (n := m) h ?_

Premises used: Real.exp_bound
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
h₁ :
  |x| ^ m / (↑m.factorial : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)) =
    |x| ^ m * ((↑m.succ : ℝ) / HMul.hMul (α := ℝ) (↑m.factorial : ℝ) (↑m : ℝ))
convert! : 0 < m
⊢ |rexp x - ∑ m ∈ range m, x ^ m / (↑m.factorial : ℝ)| ≤
    |x| ^ m / (↑m.factorial : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))

Tactic:
convert! exp_bound (n := m) h ?_ using 1

Premises used: Real.exp_bound
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ |x| ^ m / (↑m.factorial : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)) =
    |x| ^ m * ((↑m.succ : ℝ) / HMul.hMul (α := ℝ) (↑m.factorial : ℝ) (↑m : ℝ))

Tactic:
simp [field]
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ 0 < m

Tactic:
lia
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : |1 + x / (↑m : ℝ) * a₂ - a₁| ≤ b₁ - |x| / (↑m : ℝ) * b₂
h : |rexp x - expNear m x a₂| ≤ |x| ^ m / (↑m.factorial : ℝ) * b₂
grw : |x| ^ m / (↑m.factorial : ℝ) * b₂ + |expNear m x a₂ - expNear n x a₁| ≤ |x| ^ n / (↑n.factorial : ℝ) * b₁
⊢ |rexp x - expNear n x a₁| ≤ |x| ^ n / (↑n.factorial : ℝ) * b₁

Tactic:
grw [abs_sub_le, h]

Premises used: abs_sub_le
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : |1 + x / (↑m : ℝ) * a₂ - a₁| ≤ b₁ - |x| / (↑m : ℝ) * b₂
h : |rexp x - expNear m x a₂| ≤ |x| ^ m / (↑m.factorial : ℝ) * b₂
subst :
  ∀ (e : |1 + x / (↑(n + 1) : ℝ) * a₂ - a₁| ≤ b₁ - |x| / (↑(n + 1) : ℝ) * b₂)
    (h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / (↑(n + 1).factorial : ℝ) * b₂),
    |x| ^ (n + 1) / (↑(n + 1).factorial : ℝ) * b₂ + |expNear (n + 1) x a₂ - expNear n x a₁| ≤
      |x| ^ n / (↑n.factorial : ℝ) * b₁
⊢ |x| ^ m / (↑m.factorial : ℝ) * b₂ + |expNear m x a₂ - expNear n x a₁| ≤ |x| ^ n / (↑n.factorial : ℝ) * b₁

Tactic:
subst e₁
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / (↑(n + 1) : ℝ) * a₂ - a₁| ≤ b₁ - |x| / (↑(n + 1) : ℝ) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / (↑(n + 1).factorial : ℝ) * b₂
rw :
  |x| ^ (n + 1) / (↑(n + 1).factorial : ℝ) * b₂ +
      |x ^ n / (↑n.factorial : ℝ)| * |1 + x / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a₂ - a₁| ≤
    |x| ^ n / (↑n.factorial : ℝ) * b₁
⊢ |x| ^ (n + 1) / (↑(n + 1).factorial : ℝ) * b₂ + |expNear (n + 1) x a₂ - expNear n x a₁| ≤
    |x| ^ n / (↑n.factorial : ℝ) * b₁

Tactic:
rw [expNear_succ, expNear_sub, abs_mul]

Premises used: Real.expNear_succ, abs_mul, Real.expNear_sub
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / (↑(n + 1) : ℝ) * a₂ - a₁| ≤ b₁ - |x| / (↑(n + 1) : ℝ) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / (↑(n + 1).factorial : ℝ) * b₂
⊢ |x| ^ n / (↑n.factorial : ℝ) * (|x| / (↑(n + 1) : ℝ) * b₂ + |1 + x / (↑(n + 1) : ℝ) * a₂ - a₁|) ≤
    |x| ^ n / (↑n.factorial : ℝ) * b₁

Tactic:
mul_le_mul_of_nonneg_left (a := |x| ^ n / ↑(Nat.factorial n)) (le_sub_iff_add_le'.1 e) ?_

Premises used: le_sub_iff_add_le', Iff.mp, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / (↑(n + 1) : ℝ) * a₂ - a₁| ≤ b₁ - |x| / (↑(n + 1) : ℝ) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / (↑(n + 1).factorial : ℝ) * b₂
h₁ :
  |x| ^ (n + 1) / (↑(n + 1).factorial : ℝ) * b₂ +
      |x ^ n / (↑n.factorial : ℝ)| * |1 + x / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a₂ - a₁| =
    |x| ^ n / (↑n.factorial : ℝ) * (|x| / (↑(n + 1) : ℝ) * b₂ + |1 + x / (↑(n + 1) : ℝ) * a₂ - a₁|)
mul_le_mul_of_nonneg_left : 0 ≤ |x| ^ n / (↑n.factorial : ℝ)
⊢ |x| ^ (n + 1) / (↑(n + 1).factorial : ℝ) * b₂ +
      |x ^ n / (↑n.factorial : ℝ)| * |1 + x / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a₂ - a₁| ≤
    |x| ^ n / (↑n.factorial : ℝ) * b₁

Tactic:
convert!
    mul_le_mul_of_nonneg_left (a := |x| ^ n / ↑(Nat.factorial n)) (le_sub_iff_add_le'.1 e) ?_
      using 1

Premises used: le_sub_iff_add_le', Iff.mp, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / (↑(n + 1) : ℝ) * a₂ - a₁| ≤ b₁ - |x| / (↑(n + 1) : ℝ) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / (↑(n + 1).factorial : ℝ) * b₂
h₁ :
  |x| * |x| ^ n * ((↑n.factorial : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹) * b₂ =
    |x| ^ n * (↑n.factorial : ℝ)⁻¹ * (|x| * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * b₂)
⊢ |x| ^ (n + 1) / (↑(n + 1).factorial : ℝ) * b₂ +
      |x ^ n / (↑n.factorial : ℝ)| * |1 + x / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a₂ - a₁| =
    |x| ^ n / (↑n.factorial : ℝ) * (|x| / (↑(n + 1) : ℝ) * b₂ + |1 + x / (↑(n + 1) : ℝ) * a₂ - a₁|)

Tactic:
simp [mul_add, pow_succ', div_eq_mul_inv, abs_mul, abs_inv, Nat.factorial]

Premises used: abs_inv, abs_mul, div_eq_mul_inv, Nat.factorial, mul_add, pow_succ'