awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |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)
have 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)
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 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)
have 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)
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 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)
have 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)
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 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)
have 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)
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 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)
have 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)
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 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)
have 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)
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 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)
have 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)
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 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)
have h : |rexp 1 -
      expNear 12 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 -
            1) *
          12)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 12 / (↑(Nat.factorial 12) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 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:
⊢ |rexp 1 -
        expNear 12 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 -
              1) *
            12)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 12 / (↑(Nat.factorial 12) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12)
have h : |rexp 1 -
      expNear 13 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 -
                1) *
              12 -
            1) *
          13)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 13 / (↑(Nat.factorial 13) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 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 13 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 -
                  1) *
                12 -
              1) *
            13)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 13 / (↑(Nat.factorial 13) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13)
have h : |rexp 1 -
      expNear 14 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 -
                    1) *
                  12 -
                1) *
              13 -
            1) *
          14)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 14 / (↑(Nat.factorial 14) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14)
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 (α := ℝ) (↑15 : ℝ) 15
have norm_cast : Eq (α := ℝ) 15 15
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 -
        expNear 14 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 -
                      1) *
                    12 -
                  1) *
                13 -
              1) *
            14)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 14 / (↑(Nat.factorial 14) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14)
have h : |rexp 1 -
      expNear 15 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 -
                        1) *
                      12 -
                    1) *
                  13 -
                1) *
              14 -
            1) *
          15)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 15 / (↑(Nat.factorial 15) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15)
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 (α := ℝ) (↑16 : ℝ) 16
have norm_cast : Eq (α := ℝ) 16 16
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 -
        expNear 15 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 -
                          1) *
                        12 -
                      1) *
                    13 -
                  1) *
                14 -
              1) *
            15)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 15 / (↑(Nat.factorial 15) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15)
have h : |rexp 1 -
      expNear 16 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 -
                            1) *
                          12 -
                        1) *
                      13 -
                    1) *
                  14 -
                1) *
              15 -
            1) *
          16)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 16 / (↑(Nat.factorial 16) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16)
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 (α := ℝ) (↑17 : ℝ) 17
have norm_cast : Eq (α := ℝ) 17 17
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 -
        expNear 16 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 -
                              1) *
                            12 -
                          1) *
                        13 -
                      1) *
                    14 -
                  1) *
                15 -
              1) *
            16)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 16 / (↑(Nat.factorial 16) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16)
have h : |rexp 1 -
      expNear 17 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 -
                                1) *
                              12 -
                            1) *
                          13 -
                        1) *
                      14 -
                    1) *
                  15 -
                1) *
              16 -
            1) *
          17)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 17 / (↑(Nat.factorial 17) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17)
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 (α := ℝ) (↑18 : ℝ) 18
have norm_cast : Eq (α := ℝ) 18 18
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 -
        expNear 17 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 -
                                  1) *
                                12 -
                              1) *
                            13 -
                          1) *
                        14 -
                      1) *
                    15 -
                  1) *
                16 -
              1) *
            17)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 17 / (↑(Nat.factorial 17) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 *
        17)
have h : |rexp 1 -
      expNear 18 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 -
                                    1) *
                                  12 -
                                1) *
                              13 -
                            1) *
                          14 -
                        1) *
                      15 -
                    1) *
                  16 -
                1) *
              17 -
            1) *
          18)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 18 / (↑(Nat.factorial 18) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 *
      18)
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 (α := ℝ) (↑19 : ℝ) 19
have norm_cast : Eq (α := ℝ) 19 19
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 -
        expNear 18 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 -
                                      1) *
                                    12 -
                                  1) *
                                13 -
                              1) *
                            14 -
                          1) *
                        15 -
                      1) *
                    16 -
                  1) *
                17 -
              1) *
            18)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 18 / (↑(Nat.factorial 18) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 *
          17 *
        18)
have h : |rexp 1 -
      expNear 19 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 -
                                        1) *
                                      12 -
                                    1) *
                                  13 -
                                1) *
                              14 -
                            1) *
                          15 -
                        1) *
                      16 -
                    1) *
                  17 -
                1) *
              18 -
            1) *
          19)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 19 / (↑(Nat.factorial 19) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 *
        18 *
      19)
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 (α := ℝ) (↑20 : ℝ) 20
have norm_cast : Eq (α := ℝ) 20 20
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |rexp 1 -
        expNear 19 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 -
                                          1) *
                                        12 -
                                      1) *
                                    13 -
                                  1) *
                                14 -
                              1) *
                            15 -
                          1) *
                        16 -
                      1) *
                    17 -
                  1) *
                18 -
              1) *
            19)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 19 / (↑(Nat.factorial 19) : ℝ) *
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 *
            17 *
          18 *
        19)
have h : |rexp 1 -
      expNear 20 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 -
                                            1) *
                                          12 -
                                        1) *
                                      13 -
                                    1) *
                                  14 -
                                1) *
                              15 -
                            1) *
                          16 -
                        1) *
                      17 -
                    1) *
                  18 -
                1) *
              19 -
            1) *
          20)| ≤
  HPow.hPow (α := ℝ) (β := ℕ) |1| 20 / (↑(Nat.factorial 20) : ℝ) *
    (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 *
          18 *
        19 *
      20)
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 (α := ℝ) (↑21 : ℝ) 21
have norm_cast : Eq (α := ℝ) 21 21
Tactic: norm_cast