-- Mathlib/Data/Complex/ExponentialBounds.lean
theorem log_two_near_10 : |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10

Proof state:
⊢ |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10

Tactic:
suffices |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34) by
  norm_num1 at *
  assumption

Result:
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)

Proof state:
this : |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
⊢ |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10

Tactic:
norm_num1 at *

Result:
this : |log 2 - 287209 / 414355| ≤ 1 / 10000000000
⊢ |log 2 - 287209 / 414355| ≤ 1 / 10000000000

Proof state:
t : |2⁻¹| = 2⁻¹
z : |log 2 - ∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)

Tactic:
apply le_trans (_root_.abs_sub_le _ _ _) (add_le_add z _)

Result:
t : |2⁻¹| = 2⁻¹
z : |log 2 - ∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1) - 287209 / 414355| ≤ 1 / 10 ^ 10 - 1 / 2 ^ 34

Proof state:
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)

Tactic:
have t : |(2⁻¹ : ℝ)| = 2⁻¹ := by rw [abs_of_pos]; norm_num

Result:
t : |2⁻¹| = 2⁻¹
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)

Proof state:
⊢ |2⁻¹| = 2⁻¹

Tactic:
rw [abs_of_pos]

Result:
⊢ 0 < 2⁻¹

Proof state:
t : |2⁻¹| = 2⁻¹
⊢ |2⁻¹| < 1

Tactic:
rw [t]

Result:
t : |2⁻¹| = 2⁻¹
⊢ 2⁻¹ < 1

Proof state:
t : |2⁻¹| = 2⁻¹
z : |∑ x ∈ range 34, (1 / 2) ^ (x + 1) / (↑x + 1) + log (1 / 2)| ≤ 1 / 17179869184
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)

Tactic:
rw [one_div (2 : ℝ), log_inv, ← sub_eq_add_neg, _root_.abs_sub_comm] at z

Result:
t : |2⁻¹| = 2⁻¹
z : |log 2 - ∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)

Proof state:
t : |2⁻¹| = 2⁻¹
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)

Tactic:
have z := Real.abs_log_sub_add_sum_range_le (show |(2⁻¹ : ℝ)| < 1 by rw [t]; norm_num) 34

Result:
t : |2⁻¹| = 2⁻¹
z : |∑ i ∈ range 34, 2⁻¹ ^ (i + 1) / (↑i + 1) + log (1 - 2⁻¹)| ≤ |2⁻¹| ^ (34 + 1) / (1 - |2⁻¹|)
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)

Proof state:
t : |2⁻¹| = 2⁻¹
⊢ 2⁻¹ < 1

Tactic:
norm_num

Result:
no goals

Proof state:
t : |2⁻¹| = 2⁻¹
z : |log 2 - ∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |∑ x ∈ range 0, 2⁻¹ ^ (x + 1) / (↑x + 1) + 2⁻¹ ^ (0 + 1) / (↑0 + 1) + 2⁻¹ ^ (1 + 1) / (↑1 + 1) +
                                                                        2⁻¹ ^ (2 + 1) / (↑2 + 1) +
                                                                      2⁻¹ ^ (3 + 1) / (↑3 + 1) +
                                                                    2⁻¹ ^ (4 + 1) / (↑4 + 1) +
                                                                  2⁻¹ ^ (5 + 1) / (↑5 + 1) +
                                                                2⁻¹ ^ (6 + 1) / (↑6 + 1) +
                                                              2⁻¹ ^ (7 + 1) / (↑7 + 1) +
                                                            2⁻¹ ^ (8 + 1) / (↑8 + 1) +
                                                          2⁻¹ ^ (9 + 1) / (↑9 + 1) +
                                                        2⁻¹ ^ (10 + 1) / (↑10 + 1) +
                                                      2⁻¹ ^ (11 + 1) / (↑11 + 1) +
                                                    2⁻¹ ^ (12 + 1) / (↑12 + 1) +
                                                  2⁻¹ ^ (13 + 1) / (↑13 + 1) +
                                                2⁻¹ ^ (14 + 1) / (↑14 + 1) +
                                              2⁻¹ ^ (15 + 1) / (↑15 + 1) +
                                            2⁻¹ ^ (16 + 1) / (↑16 + 1) +
                                          2⁻¹ ^ (17 + 1) / (↑17 + 1) +
                                        2⁻¹ ^ (18 + 1) / (↑18 + 1) +
                                      2⁻¹ ^ (19 + 1) / (↑19 + 1) +
                                    2⁻¹ ^ (20 + 1) / (↑20 + 1) +
                                  2⁻¹ ^ (21 + 1) / (↑21 + 1) +
                                2⁻¹ ^ (22 + 1) / (↑22 + 1) +
                              2⁻¹ ^ (23 + 1) / (↑23 + 1) +
                            2⁻¹ ^ (24 + 1) / (↑24 + 1) +
                          2⁻¹ ^ (25 + 1) / (↑25 + 1) +
                        2⁻¹ ^ (26 + 1) / (↑26 + 1) +
                      2⁻¹ ^ (27 + 1) / (↑27 + 1) +
                    2⁻¹ ^ (28 + 1) / (↑28 + 1) +
                  2⁻¹ ^ (29 + 1) / (↑29 + 1) +
                2⁻¹ ^ (30 + 1) / (↑30 + 1) +
              2⁻¹ ^ (31 + 1) / (↑31 + 1) +
            2⁻¹ ^ (32 + 1) / (↑32 + 1) +
          2⁻¹ ^ (33 + 1) / (↑33 + 1) -
        287209 / 414355| ≤
    1 / 10 ^ 10 - 1 / 2 ^ 34

Tactic:
norm_num

Result:
t : |2⁻¹| = 2⁻¹
z : |log 2 - ∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |30417026706710207 / 51397301678363663775930777600| ≤ 7011591 / 167772160000000000

Proof state:
this : |log 2 - 287209 / 414355| ≤ 1 / 10000000000
⊢ |log 2 - 287209 / 414355| ≤ 1 / 10000000000

Tactic:
assumption

Result:
no goals

Proof state:
t : |2⁻¹| = 2⁻¹
z : |∑ i ∈ range 34, 2⁻¹ ^ (i + 1) / (↑i + 1) + log (1 - 2⁻¹)| ≤ |2⁻¹| ^ (34 + 1) / (1 - |2⁻¹|)
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)

Tactic:
rw [t] at z

Result:
t : |2⁻¹| = 2⁻¹
z : |∑ i ∈ range 34, 2⁻¹ ^ (i + 1) / (↑i + 1) + log (1 - 2⁻¹)| ≤ 2⁻¹ ^ (34 + 1) / (1 - 2⁻¹)
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)

Proof state:
⊢ 0 < 2⁻¹

Tactic:
norm_num

Result:
no goals

Proof state:
t : |2⁻¹| = 2⁻¹
z : |∑ i ∈ range 34, 2⁻¹ ^ (i + 1) / (↑i + 1) + log (1 - 2⁻¹)| ≤ 2⁻¹ ^ (34 + 1) / (1 - 2⁻¹)
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)

Tactic:
norm_num1 at z

Result:
t : |2⁻¹| = 2⁻¹
z : |∑ x ∈ range 34, (1 / 2) ^ (x + 1) / (↑x + 1) + log (1 / 2)| ≤ 1 / 17179869184
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)

Proof state:
t : |2⁻¹| = 2⁻¹
z : |log 2 - ∑ x ∈ range 34, 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |30417026706710207 / 51397301678363663775930777600| ≤ 7011591 / 167772160000000000

Tactic:
rw [abs_of_pos] <;> norm_num

Result:
no goals