mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |rexp 1 - expNear 4 1 (((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4)| ≤
    |1| ^ 4 / ↑(Nat.factorial 4) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4)

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

Goal state after:
⊢ |rexp 1 - expNear 5 1 ((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5)| ≤
    |1| ^ 5 / ↑(Nat.factorial 5) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |rexp 1 - expNear 5 1 ((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5)| ≤
    |1| ^ 5 / ↑(Nat.factorial 5) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5)

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

Goal state after:
⊢ |rexp 1 - expNear 6 1 (((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6)| ≤
    |1| ^ 6 / ↑(Nat.factorial 6) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |rexp 1 - expNear 6 1 (((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6)| ≤
    |1| ^ 6 / ↑(Nat.factorial 6) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6)

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

Goal state after:
⊢ |rexp 1 -
        expNear 7 1
          ((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7)| ≤
    |1| ^ 7 / ↑(Nat.factorial 7) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |rexp 1 -
        expNear 7 1
          ((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7)| ≤
    |1| ^ 7 / ↑(Nat.factorial 7) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7)

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

Goal state after:
⊢ |rexp 1 -
        expNear 8 1
          (((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) *
            8)| ≤
    |1| ^ 8 / ↑(Nat.factorial 8) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |rexp 1 -
        expNear 8 1
          (((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) *
            8)| ≤
    |1| ^ 8 / ↑(Nat.factorial 8) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8)

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

Goal state after:
⊢ |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)| ≤
    |1| ^ 9 / ↑(Nat.factorial 9) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |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)| ≤
    |1| ^ 9 / ↑(Nat.factorial 9) * (1 / 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) ?_

Goal state after:
⊢ |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)| ≤
    |1| ^ 10 / ↑(Nat.factorial 10) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |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)| ≤
    |1| ^ 10 / ↑(Nat.factorial 10) * (1 / 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) ?_

Goal state after:
⊢ |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)| ≤
    |1| ^ 11 / ↑(Nat.factorial 11) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |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)| ≤
    |1| ^ 11 / ↑(Nat.factorial 11) * (1 / 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) ?_

Goal state after:
⊢ |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)| ≤
    |1| ^ 12 / ↑(Nat.factorial 12) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |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)| ≤
    |1| ^ 12 / ↑(Nat.factorial 12) * (1 / 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) ?_

Goal state after:
⊢ |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)| ≤
    |1| ^ 13 / ↑(Nat.factorial 13) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |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)| ≤
    |1| ^ 13 / ↑(Nat.factorial 13) * (1 / 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) ?_

Goal state after:
⊢ |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)| ≤
    |1| ^ 14 / ↑(Nat.factorial 14) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |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)| ≤
    |1| ^ 14 / ↑(Nat.factorial 14) * (1 / 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) ?_

Goal state after:
⊢ |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)| ≤
    |1| ^ 15 / ↑(Nat.factorial 15) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15)
Module: Mathlib.Analysis.Complex.CanonicalDecomposition

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
⊢ ((∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
        ∏ᶠ (i : ℂ), meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) •
      meromorphicTrailingCoeffAt
        (((∏ᶠ (u : ℂ), canonicalFactor R u ^ (-(divisor f B₀R) u)) * ∏ᶠ (v : ℂ), (fun x ↦ x - v) ^ (divisor f S₀R) v) •
          h)
        w =
    ((∏ i ∈ t₂, meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) *
        ∏ i ∈ t₁, meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) •
      meromorphicTrailingCoeffAt
        (((∏ i ∈ t₂, canonicalFactor R i ^ (-(divisor f B₀R) i)) * ∏ i ∈ t₁, (fun x ↦ x - i) ^ (divisor f S₀R) i) • h) w

Tactic:
rw [finprod_eq_prod_of_mulSupport_subset (s := t₂) _ _,
        finprod_eq_prod_of_mulSupport_subset (s := t₁) _ _,
        finprod_eq_prod_of_mulSupport_subset (s := t₂) _ _,
        finprod_eq_prod_of_mulSupport_subset (s := t₁) _ _]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
⊢ (mulSupport fun v ↦ (fun x ↦ x - v) ^ (divisor f S₀R) v) ⊆ ↑t₁

E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
⊢ (mulSupport fun u ↦ canonicalFactor R u ^ (-(divisor f B₀R) u)) ⊆ ↑t₂

E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
⊢ (mulSupport fun i ↦ meromorphicTrailingCoeffAt (fun x ↦ x - i) w ^ (-divisor f S₀R) i) ⊆ ↑t₁

E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
w : ℂ
f h : ℂ → E
D : ECanonicalDecomp f h R
hw : w ∈ closedBall 0 R
hR : 0 < R
B₀R : Set ℂ := ball 0 R
S₀R : Set ℂ := sphere 0 R
t₁ : Finset ℂ
ht₁ : ↑t₁ = (divisor f S₀R).support
t₂ : Finset ℂ
ht₂ : ↑t₂ = (divisor f B₀R).support
this : MeromorphicAt h w
⊢ (mulSupport fun i ↦ meromorphicTrailingCoeffAt (canonicalFactor R i) w ^ (divisor f B₀R) i) ⊆ ↑t₂
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |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)| ≤
    |1| ^ 15 / ↑(Nat.factorial 15) * (1 / 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) ?_

Goal state after:
⊢ |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)| ≤
    |1| ^ 16 / ↑(Nat.factorial 16) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |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)| ≤
    |1| ^ 16 / ↑(Nat.factorial 16) *
      (1 / 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) ?_

Goal state after:
⊢ |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)| ≤
    |1| ^ 17 / ↑(Nat.factorial 17) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |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)| ≤
    |1| ^ 17 / ↑(Nat.factorial 17) *
      (1 / 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) ?_

Goal state after:
⊢ |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)| ≤
    |1| ^ 18 / ↑(Nat.factorial 18) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18)
Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |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)| ≤
    |1| ^ 18 / ↑(Nat.factorial 18) *
      (1 / 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) ?_

Goal state after:
⊢ |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)| ≤
    |1| ^ 19 / ↑(Nat.factorial 19) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18 * 19)