awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
⊢ rexp x < 1 / (1 - x)
have exp : ∑ m ∈ range 3, x ^ m / (↑m.factorial : ℝ) +
    HPow.hPow (β := ℕ) x 3 * HAdd.hAdd (α := ℝ) (↑3 : ℝ) 1 / HMul.hMul (α := ℝ) (↑(Nat.factorial 3) : ℝ) (↑3 : ℝ) ≤
  1 + x + HPow.hPow (β := ℕ) x 2
Tactic: calc
    exp x ≤ _ := exp_bound' h1.le h2.le zero_lt_three
    _ ≤ 1 + x + x ^ 2 := by
      -- Porting note: was `norm_num [Finset.sum] <;> nlinarith`
      -- This proof should be restored after the norm_num plugin for big operators is ported.
      -- (It may also need the positivity extensions in https://github.com/leanprover-community/mathlib4/pull/3907.)
      rw [show 3 = 1 + 1 + 1 from rfl]
      repeat rw [Finset.sum_range_succ]
      norm_num [Nat.factorial]
      nlinarith
    _ < 1 / (1 - x) := by rw [lt_div_iff₀] <;> nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
exp :
  ∑ m ∈ range 3, x ^ m / (↑m.factorial : ℝ) +
      HPow.hPow (β := ℕ) x 3 * HAdd.hAdd (α := ℝ) (↑3 : ℝ) 1 / HMul.hMul (α := ℝ) (↑(Nat.factorial 3) : ℝ) (↑3 : ℝ) ≤
    1 + x + HPow.hPow (β := ℕ) x 2
⊢ rexp x < 1 / (1 - x)
have exp₁ : 1 + x + HPow.hPow (β := ℕ) x 2 < 1 / (1 - x)
Tactic: calc
    exp x ≤ _ := exp_bound' h1.le h2.le zero_lt_three
    _ ≤ 1 + x + x ^ 2 := by
      -- Porting note: was `norm_num [Finset.sum] <;> nlinarith`
      -- This proof should be restored after the norm_num plugin for big operators is ported.
      -- (It may also need the positivity extensions in https://github.com/leanprover-community/mathlib4/pull/3907.)
      rw [show 3 = 1 + 1 + 1 from rfl]
      repeat rw [Finset.sum_range_succ]
      norm_num [Nat.factorial]
      nlinarith
    _ < 1 / (1 - x) := by rw [lt_div_iff₀] <;> nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x < 1
⊢ rexp x ≤ 1 / (1 - x)
have inl : ∀ (h1 : LE.le (α := ℝ) 0 0) (h2 : LT.lt (α := ℝ) 0 1), rexp 0 ≤ 1 / HSub.hSub (α := ℝ) 1 0
Tactic: rcases eq_or_lt_of_le h1 with (rfl | h1)
Cleared hypotheses: x, h1, h2
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x < 1
inl : ∀ (h1 : LE.le (α := ℝ) 0 0) (h2 : LT.lt (α := ℝ) 0 1), rexp 0 ≤ 1 / HSub.hSub (α := ℝ) 1 0
⊢ rexp x ≤ 1 / (1 - x)
have inr : ∀ (h1 : 0 < x), rexp x ≤ 1 / (1 - x)
Tactic: rcases eq_or_lt_of_le h1 with (rfl | h1)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ x + 1 < rexp x
have inl : ∀ (hx : 0 < x), x + 1 < rexp x
Tactic: obtain hx | hx := hx.symm.lt_or_gt
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx : x ≠ 0
inl : ∀ (hx : 0 < x), x + 1 < rexp x
⊢ x + 1 < rexp x
have inr : ∀ (hx : x < 0), x + 1 < rexp x
Tactic: obtain hx | hx := hx.symm.lt_or_gt
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
⊢ x + 1 < rexp x
have inr : ∀ (h' : 1 ≤ -x), x + 1 < rexp x
Tactic: obtain h' | h' := le_or_gt 1 (-x)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
inr : ∀ (h' : 1 ≤ -x), x + 1 < rexp x
⊢ x + 1 < rexp x
have inr₁ : ∀ (h' : -x < 1), x + 1 < rexp x
Tactic: obtain h' | h' := le_or_gt 1 (-x)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
h' : 1 ≤ -x
⊢ x + 1 < rexp x
have linarith : rexp x ≤ x + 1 → 1 - -x + (rexp x - (x + 1)) + (0 - rexp x) = 0
Tactic: linarith [x.exp_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
h' : -x < 1
⊢ 0 < x + 1
have linarith : x + 1 ≤ 0 → -x - 1 + (x + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
h' : -x < 1
⊢ x + 1 < rexp x
have hx' : 0 < x + 1
Tactic: have hx' : 0 < x + 1 := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
⊢ x + 1 ≤ rexp x
have inl : HAdd.hAdd (α := ℝ) 0 1 ≤ rexp 0
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
inl : HAdd.hAdd (α := ℝ) 0 1 ≤ rexp 0
⊢ x + 1 ≤ rexp x
have inr : ∀ (hx : x ≠ 0), x + 1 ≤ rexp x
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
⊢ (1 - t / (↑n : ℝ)) ^ n ≤ rexp (-t)
have inl : ∀ (ht' : t ≤ (↑0 : ℝ)), HPow.hPow (β := ℕ) (1 - t / (↑0 : ℝ)) 0 ≤ rexp (-t)
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n, ht'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
inl : ∀ (ht' : t ≤ (↑0 : ℝ)), HPow.hPow (β := ℕ) (1 - t / (↑0 : ℝ)) 0 ≤ rexp (-t)
⊢ (1 - t / (↑n : ℝ)) ^ n ≤ rexp (-t)
have inr : ∀ (hn : n ≠ 0), (1 - t / (↑n : ℝ)) ^ n ≤ rexp (-t)
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
t : ℝ
ht' : t ≤ (↑0 : ℝ)
⊢ HPow.hPow (β := ℕ) (1 - t / (↑0 : ℝ)) 0 ≤ rexp (-t)
have inl : t ≤ 0
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
t : ℝ
ht' : t ≤ (↑0 : ℝ)
⊢ t ≤ 0
have inl : ∀ (ht' : t ≤ 0), t ≤ 0
Tactic: rwa [Nat.cast_zero] at ht'
Cleared hypotheses: ht'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
hn : n ≠ 0
⊢ (1 - t / (↑n : ℝ)) ^ n ≤ rexp (-(t / (↑n : ℝ))) ^ n
have ha : 0 ≤ 1 - t / (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
hn : n ≠ 0
ha : 0 ≤ 1 - t / (↑n : ℝ)
⊢ (1 - t / (↑n : ℝ)) ^ n ≤ rexp (-(t / (↑n : ℝ))) ^ n
have hab : 1 - t / (↑n : ℝ) ≤ rexp (-(t / (↑n : ℝ)))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
hn : n ≠ 0
⊢ rexp (-(t / (↑n : ℝ))) ^ n = rexp (-t)
have h : Ne (α := ℝ) (↑n : ℝ) 0
Tactic: rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
hn : n ≠ 0
⊢ (1 - t / (↑n : ℝ)) ^ n ≤ rexp (-t)
have t₁ : (1 - t / (↑n : ℝ)) ^ n ≤ rexp (-(t / (↑n : ℝ))) ^ n
Tactic: calc
    (1 - t / n) ^ n ≤ rexp (-(t / n)) ^ n := by
      gcongr
      · exact sub_nonneg.2 <| div_le_one_of_le₀ ht' n.cast_nonneg
      · exact one_sub_le_exp_neg _
    _ = rexp (-t) := by rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]; positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
hn : n ≠ 0
t₁ : (1 - t / (↑n : ℝ)) ^ n ≤ rexp (-(t / (↑n : ℝ))) ^ n
⊢ (1 - t / (↑n : ℝ)) ^ n ≤ rexp (-t)
have t₂ : rexp (-(t / (↑n : ℝ))) ^ n = rexp (-t)
Tactic: calc
    (1 - t / n) ^ n ≤ rexp (-(t / n)) ^ n := by
      gcongr
      · exact sub_nonneg.2 <| div_le_one_of_le₀ ht' n.cast_nonneg
      · exact one_sub_le_exp_neg _
    _ = rexp (-t) := by rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]; positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x c : ℝ
hc : 0 < c
⊢ x ≤ c⁻¹ * rexp (c * x)
have rw : c * x ≤ rexp (c * x)
Tactic: rw [le_inv_mul_iff₀ hc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
⊢ ‖cexp (↑x : ℂ)‖ = Real.exp x
have rw : ‖(↑(Real.exp x) : ℂ)‖ = Real.exp x
Tactic: rw [← ofReal_exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - 2244083 / 825552| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10
have h : |rexp 1 - expNear 0 1 (2244083 / 825552)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 0 / (↑(Nat.factorial 0) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10)
Tactic: apply exp_approx_start
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑1 : ℝ) 1
have norm_cast : Eq (α := ℝ) 1 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - expNear 0 1 (2244083 / 825552)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 0 / (↑(Nat.factorial 0) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10)
have h : |rexp 1 - expNear 1 1 ((2244083 / 825552 - 1) * 1)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 1 / (↑(Nat.factorial 1) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑2 : ℝ) 2
have norm_cast : Eq (α := ℝ) 2 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - expNear 1 1 ((2244083 / 825552 - 1) * 1)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 1 / (↑(Nat.factorial 1) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1)
have h : |rexp 1 - expNear 2 1 (((2244083 / 825552 - 1) * 1 - 1) * 2)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 2 / (↑(Nat.factorial 2) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑3 : ℝ) 3
have norm_cast : Eq (α := ℝ) 3 3
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - expNear 2 1 (((2244083 / 825552 - 1) * 1 - 1) * 2)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 2 / (↑(Nat.factorial 2) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2)
have h : |rexp 1 - expNear 3 1 ((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 3 / (↑(Nat.factorial 3) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑4 : ℝ) 4
have norm_cast : Eq (α := ℝ) 4 4
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - expNear 3 1 ((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 3 / (↑(Nat.factorial 3) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3)
have h : |rexp 1 - expNear 4 1 (((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 4 / (↑(Nat.factorial 4) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑5 : ℝ) 5
have norm_cast : Eq (α := ℝ) 5 5
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - expNear 4 1 (((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 4 / (↑(Nat.factorial 4) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4)
have h : |rexp 1 - expNear 5 1 ((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 5 / (↑(Nat.factorial 5) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑6 : ℝ) 6
have norm_cast : Eq (α := ℝ) 6 6
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - expNear 5 1 ((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 5 / (↑(Nat.factorial 5) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5)
have h : |rexp 1 - expNear 6 1 (((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 6 / (↑(Nat.factorial 6) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑7 : ℝ) 7
have norm_cast : Eq (α := ℝ) 7 7
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - expNear 6 1 (((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 6 / (↑(Nat.factorial 6) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6)
have h : |rexp 1 - expNear 7 1 ((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 7 / (↑(Nat.factorial 7) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑8 : ℝ) 8
have norm_cast : Eq (α := ℝ) 8 8
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - expNear 7 1 ((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 7 / (↑(Nat.factorial 7) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7)
have h : |rexp 1 -
      expNear 8 1 (((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 8 / (↑(Nat.factorial 8) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑9 : ℝ) 9
have norm_cast : Eq (α := ℝ) 9 9
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 -
        expNear 8 1
          (((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 8 / (↑(Nat.factorial 8) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8)
have h : |rexp 1 -
      expNear 9 1
        ((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) * 9)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 9 / (↑(Nat.factorial 9) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑10 : ℝ) 10
have norm_cast : Eq (α := ℝ) 10 10
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 -
        expNear 9 1
          ((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) *
            9)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 9 / (↑(Nat.factorial 9) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9)
have h : |rexp 1 -
      expNear 10 1
        (((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) * 9 -
            1) *
          10)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 10 / (↑(Nat.factorial 10) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑11 : ℝ) 11
have norm_cast : Eq (α := ℝ) 11 11
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 -
        expNear 10 1
          (((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) * 9 -
              1) *
            10)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 10 / (↑(Nat.factorial 10) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10)
have h : |rexp 1 -
      expNear 11 1
        ((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) * 9 -
                1) *
              10 -
            1) *
          11)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 11 / (↑(Nat.factorial 11) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑12 : ℝ) 12
have norm_cast : Eq (α := ℝ) 12 12
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 -
        expNear 11 1
          ((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) *
                    9 -
                  1) *
                10 -
              1) *
            11)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 11 / (↑(Nat.factorial 11) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11)
have h : |rexp 1 -
      expNear 12 1
        (((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) * 9 -
                    1) *
                  10 -
                1) *
              11 -
            1) *
          12)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 12 / (↑(Nat.factorial 12) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑13 : ℝ) 13
have norm_cast : Eq (α := ℝ) 13 13
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 -
        expNear 12 1
          (((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) *
                        9 -
                      1) *
                    10 -
                  1) *
                11 -
              1) *
            12)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 12 / (↑(Nat.factorial 12) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12)
have h : |rexp 1 -
      expNear 13 1
        ((((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) *
                          9 -
                        1) *
                      10 -
                    1) *
                  11 -
                1) *
              12 -
            1) *
          13)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 13 / (↑(Nat.factorial 13) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - expNear 0 1 (2244083 / 825552)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 0 / (↑(Nat.factorial 0) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10)
have h : |rexp 1 -
      expNear 13 1
        ((((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) *
                          9 -
                        1) *
                      10 -
                    1) *
                  11 -
                1) *
              12 -
            1) *
          13)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 13 / (↑(Nat.factorial 13) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13)
Tactic: iterate 13 refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ Eq (α := ℝ) (↑14 : ℝ) 14
have norm_cast : Eq (α := ℝ) 14 14
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 -
        expNear 13 1
          ((((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) *
                            9 -
                          1) *
                        10 -
                      1) *
                    11 -
                  1) *
                12 -
              1) *
            13)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 13 / (↑(Nat.factorial 13) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13)
have h : |1 -
      (((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) * 9 -
                      1) *
                    10 -
                  1) *
                11 -
              1) *
            12 -
          1) *
        13| ≤
  1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 -
    HDiv.hDiv (α := ℝ) |1| 14 * (HAdd.hAdd (α := ℝ) 14 1 / 14)
Tactic: refine exp_approx_end' _ (by norm_num1; rfl) _ (by norm_cast) (by simp) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - 363916618873 / 133877442384| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20
have h : |rexp 1 - expNear 0 1 (363916618873 / 133877442384)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 0 / (↑(Nat.factorial 0) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20)
Tactic: apply exp_approx_start
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - expNear 0 1 (363916618873 / 133877442384)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 0 / (↑(Nat.factorial 0) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20)
have h : |rexp 1 - expNear 1 1 ((363916618873 / 133877442384 - 1) * 1)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 1 / (↑(Nat.factorial 1) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - expNear 1 1 ((363916618873 / 133877442384 - 1) * 1)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 1 / (↑(Nat.factorial 1) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1)
have h : |rexp 1 - expNear 2 1 (((363916618873 / 133877442384 - 1) * 1 - 1) * 2)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 2 / (↑(Nat.factorial 2) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - expNear 2 1 (((363916618873 / 133877442384 - 1) * 1 - 1) * 2)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 2 / (↑(Nat.factorial 2) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2)
have h : |rexp 1 - expNear 3 1 ((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 3 / (↑(Nat.factorial 3) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 - expNear 3 1 ((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 3 / (↑(Nat.factorial 3) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3)
have h : |rexp 1 - expNear 4 1 (((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 4 / (↑(Nat.factorial 4) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_