awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ |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:
norm_num1
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ 2.7182818283 < 2244083 / 825552 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 + 2244083 / 825552 < 2.7182818286

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ LT.lt (α := ℝ) 2 2.7182818283

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ LT.lt (α := ℝ) 2.7182818286 3

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ rexp 1 < HAdd.hAdd (α := ℝ) (↑2 : ℝ) 1

Tactic:
exact_mod_cast exp_one_lt_three

Premises used: Real.exp_one_lt_three
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ HSub.hSub (α := ℝ) (↑3 : ℝ) 1 < rexp 1

Tactic:
exact_mod_cast exp_one_gt_two

Premises used: Real.exp_one_gt_two
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ rexp 1 + 1 / 2 < HAdd.hAdd (α := ℝ) (↑3 : ℝ) 1

Tactic:
grind [exp_one_lt_three]

Premises used: Real.exp_one_lt_three
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
refine : (↑3 : ℝ) ≤ rexp 1 + 1 / 2
⊢ round (rexp 1) = 3

Tactic:
refine round_eq _ |>.trans <| Int.floor_eq_iff.mpr ⟨?_, by grind [exp_one_lt_three]⟩

Premises used: Iff.mpr, round_eq, Int.floor_eq_iff, And.intro, Eq.trans
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
grw : (↑3 : ℝ) ≤ 2.7182818283 + 1 / 2
⊢ (↑3 : ℝ) ≤ rexp 1 + 1 / 2

Tactic:
grw [← exp_one_gt_d9]

Premises used: Real.exp_one_gt_d9
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ (↑3 : ℝ) ≤ 2.7182818283 + 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
rw : rexp 1 < 0.36787944116⁻¹
rw₁ : LT.lt (α := ℝ) 0 0.36787944116
⊢ 0.36787944116 < rexp (-1)

Tactic:
rw [exp_neg, lt_inv_comm₀ _ (exp_pos _)]

Premises used: lt_inv_comm₀, Real.exp_neg, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ rexp 1 < 0.36787944116⁻¹

Tactic:
lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) ?_

Premises used: lt_of_le_of_lt, abs_sub_le_iff, sub_le_iff_le_add, And.left, Iff.mp, Real.exp_one_near_10
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
refine : 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 + 2244083 / 825552 < 0.36787944116⁻¹
⊢ rexp 1 < 0.36787944116⁻¹

Tactic:
refine lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) ?_

Premises used: lt_of_le_of_lt, abs_sub_le_iff, sub_le_iff_le_add, And.left, Iff.mp, Real.exp_one_near_10
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 + 2244083 / 825552 < 0.36787944116⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ LT.lt (α := ℝ) 0 0.36787944116

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ LT.lt (α := ℝ) 0 0.3678794412

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
rw : 0.3678794412⁻¹ < rexp 1
⊢ rexp (-1) < 0.3678794412

Tactic:
rw [exp_neg, inv_lt_comm₀ (exp_pos _) (by norm_num)]

Premises used: inv_lt_comm₀, Real.exp_neg, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ 0.3678794412⁻¹ < 2244083 / 825552 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ 0.3678794412⁻¹ < rexp 1

Tactic:
exact lt_of_lt_of_le (by norm_num) (sub_le_comm.1 (abs_sub_le_iff.1 exp_one_near_10).2)

Premises used: abs_sub_le_iff, sub_le_comm, And.right, Iff.mp, Real.exp_one_near_10, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ 0.3678794412 < 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
this :
  |log 2 - 287209 / 414355| ≤
    1 / 17179869184 + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 2 34)
norm_num1 : ∀ (this : |log 2 - 287209 / 414355| ≤ 1 / 10000000000), |log 2 - 287209 / 414355| ≤ 1 / 10000000000
⊢ |log 2 - 287209 / 414355| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10

Tactic:
norm_num1 at *
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
this : |log 2 - 287209 / 414355| ≤ 1 / 10000000000
⊢ |log 2 - 287209 / 414355| ≤ 1 / 10000000000

Tactic:
assumption
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
suffices :
  |log 2 - 287209 / 414355| ≤
    1 / 17179869184 + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 2 34)
⊢ |log 2 - 287209 / 414355| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10

Tactic:
suffices |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34) by
    norm_num1 at *
    assumption
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
rw : LT.lt (α := ℝ) 0 2⁻¹
⊢ Eq (α := ℝ) |2⁻¹| 2⁻¹

Tactic:
rw [abs_of_pos]

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ LT.lt (α := ℝ) 0 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℝ) |2⁻¹| 2⁻¹

Tactic:
have t : |(2⁻¹ : ℝ)| = 2⁻¹ := by rw [abs_of_pos]; norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : Eq (α := ℝ) |2⁻¹| 2⁻¹
rw : LT.lt (α := ℝ) 2⁻¹ 1
⊢ LT.lt (α := ℝ) |2⁻¹| 1

Tactic:
rw [t]
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : Eq (α := ℝ) |2⁻¹| 2⁻¹
⊢ LT.lt (α := ℝ) 2⁻¹ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : Eq (α := ℝ) |2⁻¹| 2⁻¹
⊢ |∑ i ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (HSub.hSub (α := ℝ) 1 2⁻¹)| ≤
    HPow.hPow (α := ℝ) |2⁻¹| (HAdd.hAdd (α := ℕ) 34 1) / HSub.hSub (α := ℝ) 1 |2⁻¹|

Tactic:
have z := Real.abs_log_sub_add_sum_range_le (show |(2⁻¹ : ℝ)| < 1 by rw [t]; norm_num) 34
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : Eq (α := ℝ) |2⁻¹| 2⁻¹
z :
  |∑ i ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (HSub.hSub (α := ℝ) 1 2⁻¹)| ≤
    HPow.hPow (α := ℝ) |2⁻¹| (HAdd.hAdd (α := ℕ) 34 1) / HSub.hSub (α := ℝ) 1 |2⁻¹|
⊢ |∑ i ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (HSub.hSub (α := ℝ) 1 2⁻¹)| ≤
    HPow.hPow (α := ℝ) 2⁻¹ (HAdd.hAdd (α := ℕ) 34 1) / HSub.hSub (α := ℝ) 1 2⁻¹

Tactic:
rw [t] at z
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : Eq (α := ℝ) |2⁻¹| 2⁻¹
z :
  |∑ i ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (HSub.hSub (α := ℝ) 1 2⁻¹)| ≤
    HPow.hPow (α := ℝ) 2⁻¹ (HAdd.hAdd (α := ℕ) 34 1) / HSub.hSub (α := ℝ) 1 2⁻¹
⊢ |∑ x ∈ range 34, (1 / 2) ^ (x + 1) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + log (1 / 2)| ≤ 1 / 17179869184

Tactic:
norm_num1 at z
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : Eq (α := ℝ) |2⁻¹| 2⁻¹
z : |∑ x ∈ range 34, (1 / 2) ^ (x + 1) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + log (1 / 2)| ≤ 1 / 17179869184
⊢ |log 2 - ∑ x ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (x + 1) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1| ≤ 1 / 17179869184

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

Premises used: sub_eq_add_neg, one_div, abs_sub_comm, Real.log_inv, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : Eq (α := ℝ) |2⁻¹| 2⁻¹
z : |log 2 - ∑ x ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (x + 1) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1| ≤ 1 / 17179869184
apply :
  |∑ x ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (x + 1) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 - 287209 / 414355| ≤
    1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 2 34
⊢ |log 2 - 287209 / 414355| ≤
    1 / 17179869184 + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 2 34)

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

Premises used: abs_sub_le, add_le_add, le_trans
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : Eq (α := ℝ) |2⁻¹| 2⁻¹
z : |log 2 - ∑ x ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (x + 1) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1| ≤ 1 / 17179869184
⊢ |∑ x ∈ range 34, HPow.hPow (α := ℝ) 2⁻¹ (x + 1) / HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 - 287209 / 414355| ≤
    1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 2 34

Tactic:
norm_num [sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ 0.6931471803 < 287209 / 414355 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10

Tactic:
norm_num1
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 + 287209 / 414355 < 0.6931471808

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
this :
  |log 3 - 109861228867 / 100000000000| ≤
    HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹ + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹)
norm_num1 :
  ∀ (this : |log 3 - 109861228867 / 100000000000| ≤ 1 / 10000000000),
    |log 3 - 109861228867 / 100000000000| ≤ 1 / 10000000000
⊢ |log 3 - 109861228867 / 100000000000| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10

Tactic:
norm_num1 at *
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
this : |log 3 - 109861228867 / 100000000000| ≤ 1 / 10000000000
⊢ |log 3 - 109861228867 / 100000000000| ≤ 1 / 10000000000

Tactic:
assumption
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
suffices :
  |log 3 - 109861228867 / 100000000000| ≤
    HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹ + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹)
⊢ |log 3 - 109861228867 / 100000000000| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10

Tactic:
suffices |log 3 - 109861228867 / 100000000000| ≤
      (2 / 3) ^ 71 / 3⁻¹ + (1 / 10 ^ 10 - (2 / 3) ^ 71 / 3⁻¹) by
    norm_num1 at *
    assumption
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ |2 / 3| = 2 / 3

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ |2 / 3| = 2 / 3

Tactic:
have t : |2 / 3| = (2 : ℝ) / 3 := by norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : |2 / 3| = 2 / 3
⊢ |2 / 3| < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : |2 / 3| = 2 / 3
⊢ |∑ i ∈ range 70, (2 / 3) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - 2 / 3)| ≤
    |2 / 3| ^ HAdd.hAdd (α := ℕ) 70 1 / (1 - |2 / 3|)

Tactic:
have z := abs_log_sub_add_sum_range_le (x := 2 / 3) (by norm_num) 70
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : |2 / 3| = 2 / 3
z :
  |∑ i ∈ range 70, (2 / 3) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - 2 / 3)| ≤
    (2 / 3) ^ HAdd.hAdd (α := ℕ) 70 1 / (1 - 2 / 3)
⊢ 1 - 2 / 3 = 1 / 3

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : |2 / 3| = 2 / 3
z :
  |∑ i ∈ range 70, (2 / 3) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - 2 / 3)| ≤
    |2 / 3| ^ HAdd.hAdd (α := ℕ) 70 1 / (1 - |2 / 3|)
⊢ |log 3 - ∑ i ∈ range 70, (2 / 3) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| ≤ (2 / 3) ^ HAdd.hAdd (α := ℕ) 70 1 / 3⁻¹

Tactic:
rw [t, show (1 - (2 : ℝ) / 3) = (1 / 3 : ℝ) by norm_num, one_div (3 : ℝ), log_inv,
    ← sub_eq_add_neg, _root_.abs_sub_comm] at z

Premises used: sub_eq_add_neg, one_div, abs_sub_comm, Real.log_inv, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : |2 / 3| = 2 / 3
z :
  |log 3 - ∑ i ∈ range 70, (2 / 3) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| ≤ (2 / 3) ^ HAdd.hAdd (α := ℕ) 70 1 / 3⁻¹
apply :
  |∑ i ∈ range 70, (2 / 3) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 - 109861228867 / 100000000000| ≤
    1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹
⊢ |log 3 - 109861228867 / 100000000000| ≤
    HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹ + (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹)

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

Premises used: abs_sub_le, add_le_add, le_trans
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : |2 / 3| = 2 / 3
z :
  |log 3 - ∑ i ∈ range 70, (2 / 3) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| ≤ (2 / 3) ^ HAdd.hAdd (α := ℕ) 70 1 / 3⁻¹
⊢ |∑ i ∈ range 70, (2 / 3) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 - 109861228867 / 100000000000| ≤
    1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (2 / 3) 71 / 3⁻¹

Tactic:
norm_num [sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ 1.0986122885 < 109861228867 / 100000000000 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10

Tactic:
norm_num1
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 + 109861228867 / 100000000000 < 1.0986122888

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
this :
  |log 5 - 160943791243 / 100000000000| ≤
    HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹ +
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹)
norm_num1 :
  ∀ (this : |log 5 - 160943791243 / 100000000000| ≤ 1 / 10000000000),
    |log 5 - 160943791243 / 100000000000| ≤ 1 / 10000000000
⊢ |log 5 - 160943791243 / 100000000000| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10

Tactic:
norm_num1 at *
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
this : |log 5 - 160943791243 / 100000000000| ≤ 1 / 10000000000
⊢ |log 5 - 160943791243 / 100000000000| ≤ 1 / 10000000000

Tactic:
assumption
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
suffices :
  |log 5 - 160943791243 / 100000000000| ≤
    HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹ +
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹)
⊢ |log 5 - 160943791243 / 100000000000| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10

Tactic:
suffices |log 5 - 160943791243 / 100000000000| ≤
      (4 / 5) ^ 131 / 5⁻¹ + (1 / 10 ^ 10 - (4 / 5) ^ 131 / 5⁻¹) by
    norm_num1 at *
    assumption
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ |4 / 5| = 4 / 5

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ |4 / 5| = 4 / 5

Tactic:
have t : |4 / 5| = (4 : ℝ) / 5 := by norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : |4 / 5| = 4 / 5
⊢ |4 / 5| < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : |4 / 5| = 4 / 5
⊢ |∑ i ∈ range 130, (4 / 5) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - 4 / 5)| ≤
    |4 / 5| ^ HAdd.hAdd (α := ℕ) 130 1 / (1 - |4 / 5|)

Tactic:
have z := abs_log_sub_add_sum_range_le (x := 4 / 5) (by norm_num) 130
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : |4 / 5| = 4 / 5
z :
  |∑ i ∈ range 130, (4 / 5) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - 4 / 5)| ≤
    (4 / 5) ^ HAdd.hAdd (α := ℕ) 130 1 / (1 - 4 / 5)
⊢ 1 - 4 / 5 = 1 / 5

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : |4 / 5| = 4 / 5
z :
  |∑ i ∈ range 130, (4 / 5) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + log (1 - 4 / 5)| ≤
    |4 / 5| ^ HAdd.hAdd (α := ℕ) 130 1 / (1 - |4 / 5|)
⊢ |log 5 - ∑ i ∈ range 130, (4 / 5) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| ≤
    (4 / 5) ^ HAdd.hAdd (α := ℕ) 130 1 / 5⁻¹

Tactic:
rw [t, show (1 - (4 : ℝ) / 5) = (1 / 5 : ℝ) by norm_num, one_div (5 : ℝ), log_inv,
    ← sub_eq_add_neg, _root_.abs_sub_comm] at z

Premises used: sub_eq_add_neg, one_div, abs_sub_comm, Real.log_inv, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : |4 / 5| = 4 / 5
z :
  |log 5 - ∑ i ∈ range 130, (4 / 5) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| ≤
    (4 / 5) ^ HAdd.hAdd (α := ℕ) 130 1 / 5⁻¹
apply :
  |∑ i ∈ range 130, (4 / 5) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 - 160943791243 / 100000000000| ≤
    1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹
⊢ |log 5 - 160943791243 / 100000000000| ≤
    HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹ +
      (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹)

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

Premises used: abs_sub_le, add_le_add, le_trans
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
t : |4 / 5| = 4 / 5
z :
  |log 5 - ∑ i ∈ range 130, (4 / 5) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1| ≤
    (4 / 5) ^ HAdd.hAdd (α := ℕ) 130 1 / 5⁻¹
⊢ |∑ i ∈ range 130, (4 / 5) ^ (i + 1) / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 - 160943791243 / 100000000000| ≤
    1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 - HPow.hPow (β := ℕ) (4 / 5) 131 / 5⁻¹

Tactic:
norm_num [sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ 1.6094379123 < 160943791243 / 100000000000 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10

Tactic:
norm_num1
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10 + 160943791243 / 100000000000 < 1.6094379126

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
x : ℝ
hs : ∀ x_1 ∈ norm ∘ f '' re ⁻¹' {x}, 0 ≤ x_1
⊢ 0 ≤ sSupNormIm f x

Tactic:
apply Real.sSup_nonneg

Premises used: Real.sSup_nonneg
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
x y : ℝ
z1 : ℂ
left : z1 ∈ re ⁻¹' {x}
hz2 : (norm ∘ f) z1 = y
⊢ 0 ≤ y

Tactic:
simp only [← hz2, comp, norm_nonneg]

Premises used: Function.comp, norm_nonneg
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
x : ℝ
linarith : ε + sSupNormIm f x ≤ 0 → 0 - ε + (ε + sSupNormIm f x - 0) + (0 - sSupNormIm f x) = 0
⊢ 0 < ε + sSupNormIm f x

Tactic:
linarith [sSupNormIm_nonneg f x]

Premises used: Complex.HadamardThreeLines.sSupNormIm_nonneg
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
simp :
  ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (z - 1)‖ * ‖((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
⊢ ‖invInterpStrip f z ε‖ = (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
simp only [invInterpStrip, norm_mul]

Premises used: Complex.HadamardThreeLines.invInterpStrip, norm_mul
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
rw :
  ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
⊢ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (z - 1)‖ * ‖((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
rw [← ofReal_add]

Premises used: Complex.ofReal_add
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
rw :
  ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
rw [← ofReal_add]

Premises used: Complex.ofReal_add
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
repeat :
  ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
⊢ ‖((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (z - 1)‖ * ‖((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
repeat rw [← ofReal_add]

Premises used: Complex.ofReal_add
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
rw :
  (ε + sSupNormIm f 0) ^ (z - 1).re * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
rw [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _]

Premises used: Complex.HadamardThreeLines.sSupNormIm_eps_pos, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
rw :
  (ε + sSupNormIm f 0) ^ (z - 1).re * (ε + sSupNormIm f 1) ^ (-z).re =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
⊢ (ε + sSupNormIm f 0) ^ (z - 1).re * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
rw [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _]

Premises used: Complex.HadamardThreeLines.sSupNormIm_eps_pos, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
repeat :
  (ε + sSupNormIm f 0) ^ (z - 1).re * (ε + sSupNormIm f 1) ^ (-z).re =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)
⊢ ‖(↑(ε + sSupNormIm f 0) : ℂ) ^ (z - 1)‖ * ‖(↑(ε + sSupNormIm f 1) : ℂ) ^ (-z)‖ =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
repeat rw [norm_cpow_eq_rpow_re_of_pos (sSupNormIm_eps_pos f hε _) _]

Premises used: Complex.HadamardThreeLines.sSupNormIm_eps_pos, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
ε : ℝ
hε : ε > 0
⊢ (ε + sSupNormIm f 0) ^ (z - 1).re * (ε + sSupNormIm f 1) ^ (-z).re =
    (ε + sSupNormIm f 0) ^ (z.re - 1) * (ε + sSupNormIm f 1) ^ (-z.re)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
h : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ invInterpStrip f z ε
⊢ DiffContOnCl ℂ (F := ℂ) (fun (z : ℂ) ↦ invInterpStrip f z ε) (verticalStrip 0 1)

Tactic:
apply Differentiable.diffContOnCl

Premises used: Differentiable.diffContOnCl
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
ε : ℝ
hε : ε > 0
h : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ ((↑ε : ℂ) + (↑(sSupNormIm f 0) : ℂ)) ^ (z - 1)
h₁ : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ ((↑ε : ℂ) + (↑(sSupNormIm f 1) : ℂ)) ^ (-z)
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ invInterpStrip f z ε

Tactic:
apply Differentiable.mul

Premises used: Differentiable.mul