-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |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)
have 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)
Tactic: refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_