Module: Mathlib.Analysis.Complex.ExponentialBounds

Goal state before:
pp: ⊢ |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)| ≤
    |1| ^ 21 / ↑(Nat.factorial 21) *
      (1 / 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_approx_end' _ (by norm_num1; rfl) _ (by norm_cast) (by simp) ?_

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