-- Lean 4 proof step from Mathlib.Analysis.Complex.ExponentialBounds (goal)
Goal:
⊢ |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)
have h : |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| ≤
  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 -
    HDiv.hDiv (α := ℝ) |1| 22 * (HAdd.hAdd (α := ℝ) 22 1 / 22)
Tactic: refine exp_approx_end' _ (by norm_num1; rfl) _ (by norm_cast) (by simp) ?_