awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 1 1
⊢ Eq (α := ℝ) (↑1 : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
h :
  |rexp 1 - expNear 1 1 ((2244083 / 825552 - 1) * 1)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 1 / (↑(Nat.factorial 1) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 * 1)
⊢ |rexp 1 - expNear 0 1 (2244083 / 825552)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 0 / (↑(Nat.factorial 0) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10)

Tactic:
refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℕ) 2 2

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 2 2
⊢ Eq (α := ℝ) (↑2 : ℝ) 2

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℕ) 3 3

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 3 3
⊢ Eq (α := ℝ) (↑3 : ℝ) 3

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℕ) 4 4

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 4 4
⊢ Eq (α := ℝ) (↑4 : ℝ) 4

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℕ) 5 5

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 5 5
⊢ Eq (α := ℝ) (↑5 : ℝ) 5

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℕ) 6 6

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 6 6
⊢ Eq (α := ℝ) (↑6 : ℝ) 6

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℕ) 7 7

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 7 7
⊢ Eq (α := ℝ) (↑7 : ℝ) 7

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℕ) 8 8

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 8 8
⊢ Eq (α := ℝ) (↑8 : ℝ) 8

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℕ) 9 9

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 9 9
⊢ Eq (α := ℝ) (↑9 : ℝ) 9

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℕ) 10 10

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 10 10
⊢ Eq (α := ℝ) (↑10 : ℝ) 10

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℕ) 11 11

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 11 11
⊢ Eq (α := ℝ) (↑11 : ℝ) 11

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℕ) 12 12

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 12 12
⊢ Eq (α := ℝ) (↑12 : ℝ) 12

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℕ) 13 13

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 13 13
⊢ Eq (α := ℝ) (↑13 : ℝ) 13

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |rexp 1 - expNear 0 1 (2244083 / 825552)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 0 / (↑(Nat.factorial 0) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10)

Tactic:
iterate 13 refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℕ) 14 14

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) 14 14
⊢ Eq (α := ℝ) (↑14 : ℝ) 14

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ LE.le (α := ℝ) |1| 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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_approx_end' _ (by norm_num1; rfl) _ (by norm_cast) (by simp) ?_

Premises used: Real.exp_approx_end'
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ |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:
norm_num1
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
h :
  |rexp 1 - expNear 0 1 (363916618873 / 133877442384)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 0 / (↑(Nat.factorial 0) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20)
⊢ |rexp 1 - 363916618873 / 133877442384| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20

Tactic:
apply exp_approx_start

Premises used: Real.exp_approx_start
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
h :
  |rexp 1 - expNear 1 1 ((363916618873 / 133877442384 - 1) * 1)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 1 / (↑(Nat.factorial 1) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1)
⊢ |rexp 1 - expNear 0 1 (363916618873 / 133877442384)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 0 / (↑(Nat.factorial 0) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20)

Tactic:
refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
h :
  |rexp 1 - expNear 5 1 ((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 5 / (↑(Nat.factorial 5) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5)
⊢ |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) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
h :
  |rexp 1 - expNear 6 1 (((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 6 / (↑(Nat.factorial 6) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6)
⊢ |rexp 1 - expNear 5 1 ((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 5 / (↑(Nat.factorial 5) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5)

Tactic:
refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
h :
  |rexp 1 -
        expNear 7 1
          ((((((((363916618873 / 133877442384 - 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 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7)
⊢ |rexp 1 - expNear 6 1 (((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 6 / (↑(Nat.factorial 6) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6)

Tactic:
refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
h :
  |rexp 1 -
        expNear 8 1
          (((((((((363916618873 / 133877442384 - 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 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8)
⊢ |rexp 1 -
        expNear 7 1
          ((((((((363916618873 / 133877442384 - 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 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7)

Tactic:
refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
h :
  |rexp 1 -
        expNear 9 1
          ((((((((((363916618873 / 133877442384 - 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 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9)
⊢ |rexp 1 -
        expNear 8 1
          (((((((((363916618873 / 133877442384 - 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 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8)

Tactic:
refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
h :
  |rexp 1 -
        expNear 10 1
          (((((((((((363916618873 / 133877442384 - 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 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10)
⊢ |rexp 1 -
        expNear 9 1
          ((((((((((363916618873 / 133877442384 - 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 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9)

Tactic:
refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_

Premises used: Real.exp_1_approx_succ_eq
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
h :
  |rexp 1 -
        expNear 11 1
          ((((((((((((363916618873 / 133877442384 - 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 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11)
⊢ |rexp 1 -
        expNear 10 1
          (((((((((((363916618873 / 133877442384 - 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 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10)

Tactic:
refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_

Premises used: Real.exp_1_approx_succ_eq