awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
⊢ b - n < j - n
have e_a : b < j
Tactic: rw [tsub_lt_tsub_iff_right hb.2]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
⊢ b - n + n = b
have e_a : b = b
Tactic: rw [tsub_add_cancel_of_le hb.2]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖x‖ ^ n * ∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ) ≤ ‖x‖ ^ n * Real.exp ‖x‖
have hbc : ∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ) ≤ Real.exp ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ) ≤ Real.exp ‖x‖
have hbc : 0 ≤ ‖x‖
Tactic: refine Real.sum_le_exp_of_nonneg ?_ _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    (↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) : ℕ → ℝ) j
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 * (‖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 _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 : ℂ)))
⊢ norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    (↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) : ℕ → ℝ) j
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 * (‖x‖ ^ (m - n) / (↑(m - n).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 * (‖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 _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 : ℝ)))
⊢ norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    (↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) : ℕ → ℝ) j
have 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 : ℝ)
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 _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 : ℝ)
⊢ norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    (↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) : ℕ → ℝ) j
have 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 : ℝ)
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 _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 : ℝ)
⊢ norm (E := ℂ) (∑ k ∈ range j with n ≤ k, x ^ k / (↑k.factorial : ℂ)) ≤
    (↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) : ℕ → ℝ) j
have m₄ : ‖x‖ ^ n * ∑ m ∈ range (j - n), ‖x‖ ^ m / (↑m.factorial : ℝ) ≤ ‖x‖ ^ n * Real.exp ‖x‖
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 _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
⊢ |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| ≤
    |x| ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))
have hxc : ‖(↑x : ℂ)‖ ≤ 1
Tactic: have hxc : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖(↑x : ℂ)‖ ≤ 1
⊢ |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| ≤
    |x| ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))
have h : |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| =
  ‖cexp (↑x : ℂ) - ∑ m ∈ range n, (↑x : ℂ) ^ m / (↑m.factorial : ℂ)‖
Tactic: convert! exp_bound hxc hn using 2
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 : ℂ)‖
⊢ |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| ≤
    |x| ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))
have h₁ : |x| ^ n = ‖(↑x : ℂ)‖ ^ n
Tactic: convert! exp_bound hxc hn using 2
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖(↑x : ℂ)‖ ≤ 1
⊢ |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| =
    ‖cexp (↑x : ℂ) - ∑ m ∈ range n, (↑x : ℂ) ^ m / (↑m.factorial : ℂ)‖
have h : |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| = ‖rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)‖
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖(↑x : ℂ)‖ ≤ 1
⊢ |x| ^ n = ‖(↑x : ℂ)‖ ^ n
have h : |x| ^ n = ‖x‖ ^ n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
⊢ rexp x ≤
    ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ) +
      x ^ n * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ)
have h3 : |x| = x
Tactic: have h3 : |x| = x := by simpa
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
n : ℕ
hn : 0 < n
h3 : |x| = x
⊢ rexp x ≤
    ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ) +
      x ^ n * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ)
have h4 : |x| ≤ 1
Tactic: have h4 : |x| ≤ 1 := by rwa [h3]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
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 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ)
have h' : |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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
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 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ)
have h'₁ : |rexp x - ∑ m ∈ range n, x ^ m / (↑m.factorial : ℝ)| ≤
  x ^ n * ((↑n.succ : ℝ) / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ))
Tactic: rw [h3] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
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 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ)
have h'' : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
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 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / HMul.hMul (α := ℝ) (↑n.factorial : ℝ) (↑n : ℝ)
have t : 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''
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
x : ℝ
hx : |x| ≤ 1
⊢ |rexp x - 1| ≤ 2 * |x|
have this : ‖(↑x : ℂ)‖ ≤ 1
Tactic: have : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : |x| ≤ 1
⊢ |rexp x - 1 - x| ≤ HPow.hPow (β := ℕ) x 2
have rw : |rexp x - 1 - x| ≤ HPow.hPow (β := ℕ) |x| 2
Tactic: rw [← sq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
x : ℝ
hx : |x| ≤ 1
⊢ |rexp x - 1 - x| ≤ HPow.hPow (β := ℕ) |x| 2
have this : ‖(↑x : ℂ)‖ ≤ 1
Tactic: have : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
n : ℕ
x r : ℝ
⊢ expNear (n + 1) x r = expNear n x (1 + x / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * r)
have simp : x ^ n * x * ((↑n.factorial : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹) * r =
  x ^ n * (↑n.factorial : ℝ)⁻¹ * (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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ |rexp x - expNear m x 0| ≤ |x| ^ m / (↑m.factorial : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))
have simp : |rexp x - ∑ m ∈ range m, x ^ m / (↑m.factorial : ℝ)| ≤
  |x| ^ m / (↑m.factorial : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))
Tactic: simp only [expNear, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
n m : ℕ
x : ℝ
e₁ : n + 1 = m
h : |x| ≤ 1
⊢ |rexp x - ∑ m ∈ range m, x ^ m / (↑m.factorial : ℝ)| ≤
    |x| ^ m / (↑m.factorial : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))
have h₁ : |x| ^ m / (↑m.factorial : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ)) =
  |x| ^ m * ((↑m.succ : ℝ) / HMul.hMul (α := ℝ) (↑m.factorial : ℝ) (↑m : ℝ))
Tactic: convert! exp_bound (n := m) h ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 : ℝ))
⊢ |rexp x - ∑ m ∈ range m, x ^ m / (↑m.factorial : ℝ)| ≤
    |x| ^ m / (↑m.factorial : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))
have convert! : 0 < m
Tactic: convert! exp_bound (n := m) h ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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₂
⊢ |rexp x - expNear n x a₁| ≤ |x| ^ n / (↑n.factorial : ℝ) * b₁
have grw : |x| ^ m / (↑m.factorial : ℝ) * b₂ + |expNear m x a₂ - expNear n x a₁| ≤ |x| ^ n / (↑n.factorial : ℝ) * b₁
Tactic: grw [abs_sub_le, h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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₂
⊢ |x| ^ m / (↑m.factorial : ℝ) * b₂ + |expNear m x a₂ - expNear n x a₁| ≤ |x| ^ n / (↑n.factorial : ℝ) * b₁
have 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₁
Tactic: subst e₁
Cleared hypotheses: m, e₁, e, h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 + 1) / (↑(n + 1).factorial : ℝ) * b₂ + |expNear (n + 1) x a₂ - expNear n x a₁| ≤
    |x| ^ n / (↑n.factorial : ℝ) * b₁
have 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₁
Tactic: rw [expNear_succ, expNear_sub, abs_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 + 1) / (↑(n + 1).factorial : ℝ) * b₂ +
      |x ^ n / (↑n.factorial : ℝ)| * |1 + x / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a₂ - a₁| ≤
    |x| ^ n / (↑n.factorial : ℝ) * b₁
have 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₁|)
Tactic: convert!
    mul_le_mul_of_nonneg_left (a := |x| ^ n / ↑(Nat.factorial n)) (le_sub_iff_add_le'.1 e) ?_
      using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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₁|)
⊢ |x| ^ (n + 1) / (↑(n + 1).factorial : ℝ) * b₂ +
      |x ^ n / (↑n.factorial : ℝ)| * |1 + x / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * a₂ - a₁| ≤
    |x| ^ n / (↑n.factorial : ℝ) * b₁
have mul_le_mul_of_nonneg_left : 0 ≤ |x| ^ n / (↑n.factorial : ℝ)
Tactic: convert!
    mul_le_mul_of_nonneg_left (a := |x| ^ n / ↑(Nat.factorial n)) (le_sub_iff_add_le'.1 e) ?_
      using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 + 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₁|)
have h₁ : |x| * |x| ^ n * ((↑n.factorial : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹) * b₂ =
  |x| ^ n * (↑n.factorial : ℝ)⁻¹ * (|x| * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * b₂)
Tactic: simp [mul_add, pow_succ', div_eq_mul_inv, abs_mul, abs_inv, Nat.factorial]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
rm : ℝ
er : (↑m : ℝ) = rm
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / rm * ((rm + 1) / rm)
⊢ |rexp x - expNear n x a| ≤ |x| ^ n / (↑n.factorial : ℝ) * b
have e₂ : |1 - a| ≤ b - |x| / (↑m : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))
Tactic: subst er
Cleared hypotheses: rm, er, e
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
rm : ℝ
er : (↑m : ℝ) = rm
h : |rexp 1 - expNear m 1 ((a₁ - 1) * rm)| ≤ HPow.hPow (α := ℝ) |1| m / (↑m.factorial : ℝ) * (b₁ * rm)
⊢ |rexp 1 - expNear n 1 a₁| ≤ HPow.hPow (α := ℝ) |1| n / (↑n.factorial : ℝ) * b₁
have h₁ : |rexp 1 - expNear m 1 ((a₁ - 1) * (↑m : ℝ))| ≤ HPow.hPow (α := ℝ) |1| m / (↑m.factorial : ℝ) * (b₁ * (↑m : ℝ))
Tactic: subst er
Cleared hypotheses: rm, er, h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * (↑m : ℝ))| ≤ HPow.hPow (α := ℝ) |1| m / (↑m.factorial : ℝ) * (b₁ * (↑m : ℝ))
⊢ |rexp 1 - expNear n 1 a₁| ≤ HPow.hPow (α := ℝ) |1| n / (↑n.factorial : ℝ) * b₁
have refine : |1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * ((a₁ - 1) * (↑m : ℝ)) - a₁| ≤
  b₁ - HDiv.hDiv (α := ℝ) |1| (↑m : ℝ) * (b₁ * (↑m : ℝ))
Tactic: refine exp_approx_succ _ en _ _ ?_ h