awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
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)
⊢ |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) ?_

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Tactic:
iterate 21 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 (α := ℕ) 22 22

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

Tactic:
norm_cast