-- Mathlib/Data/Complex/ExponentialBounds.lean
theorem exp_one_near_10 : |exp 1 - 2244083 / 825552| ≤ 1 / 10 ^ 10

Proof state:
⊢ 12 + 1 = ?m.1416

Tactic:
norm_num1

Result:
⊢ 13 = ?m.1416

Proof state:
⊢ 13 + 1 = ?m.2142

Tactic:
norm_num1

Result:
⊢ 14 = ?m.2142

Proof state:
case h

⊢ |rexp 1 -
        expNear 12 1
          (((((((((((((2244083 / 825552 - 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 ^ 10 * 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) ?_

Result:
case h

⊢ |rexp 1 -
        expNear 13 1
          ((((((((((((((2244083 / 825552 - 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 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13)

Proof state:
case h

⊢ |rexp 1 -
        expNear 13 1
          ((((((((((((((2244083 / 825552 - 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 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13)

Tactic:
norm_num1

Result:
case h

⊢ |rexp 1 - expNear 13 1 (5 / 7)| ≤ |1| ^ 13 / ↑(Nat.factorial 13) * (243243 / 390625)

Proof state:
case h

⊢ |rexp 1 - expNear 0 1 (2244083 / 825552)| ≤ |1| ^ 0 / ↑(Nat.factorial 0) * (1 / 10 ^ 10)

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

Result:
case h

⊢ |rexp 1 -
        expNear 13 1
          ((((((((((((((2244083 / 825552 - 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 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13)

Proof state:
⊢ |rexp 1 - 2244083 / 825552| ≤ 1 / 10 ^ 10

Tactic:
apply exp_approx_start

Result:
case h

⊢ |rexp 1 - expNear 0 1 (2244083 / 825552)| ≤ |1| ^ 0 / ↑(Nat.factorial 0) * (1 / 10 ^ 10)

Proof state:
case h

⊢ |1 - 5 / 7| ≤ 243243 / 390625 - |1| / 14 * ((14 + 1) / 14)

Tactic:
rw [_root_.abs_one, abs_of_pos] <;> norm_num1

Result:
no goals

Proof state:
case h

⊢ |rexp 1 - expNear 13 1 (5 / 7)| ≤ |1| ^ 13 / ↑(Nat.factorial 13) * (243243 / 390625)

Tactic:
refine exp_approx_end' _ (by norm_num1; rfl) _ (by norm_cast) (by simp) ?_

Result:
case h

⊢ |1 - 5 / 7| ≤ 243243 / 390625 - |1| / 14 * ((14 + 1) / 14)

Proof state:
⊢ |1| ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
⊢ 13 = ?m.1416

Tactic:
rfl

Result:
no goals

Proof state:
⊢ ↑13 = ?m.1418

Tactic:
norm_cast

Result:
no goals

Proof state:
⊢ ↑14 = ?m.2145

Tactic:
norm_cast

Result:
no goals

Proof state:
⊢ 14 = ?m.2142

Tactic:
rfl

Result:
no goals