awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / (↑(n + 1) : ℝ) * a₂ - a₁| ≤ b₁ - |x| / (↑(n + 1) : ℝ) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / (↑(n + 1).factorial : ℝ) * b₂
⊢ |x| * |x| ^ n * ((↑n.factorial : ℝ)⁻¹ * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹) * b₂ =
    |x| ^ n * (↑n.factorial : ℝ)⁻¹ * (|x| * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)⁻¹ * b₂)

Tactic:
ac_rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / (↑(n + 1) : ℝ) * a₂ - a₁| ≤ b₁ - |x| / (↑(n + 1) : ℝ) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / (↑(n + 1).factorial : ℝ) * b₂
⊢ 0 ≤ |x| ^ n / (↑n.factorial : ℝ)

Tactic:
simp [div_nonneg, abs_nonneg]

Premises used: div_nonneg, abs_nonneg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
rm : ℝ
er : (↑m : ℝ) = rm
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / rm * ((rm + 1) / rm)
⊢ |1 - a| ≤ b - |x| / (↑m : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))

Tactic:
subst er
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / (↑m : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))
⊢ |1 + x / (↑m : ℝ) * 0 - a| ≤ b - |x| / (↑m : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))

Tactic:
simpa using e
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
x a b : ℝ
m : ℕ
e₁ : n + 1 = m
h : |x| ≤ 1
e : |1 - a| ≤ b - |x| / (↑m : ℝ) * (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 / (↑m : ℝ))
⊢ |rexp x - expNear n x a| ≤ |x| ^ n / (↑n.factorial : ℝ) * b

Tactic:
exact exp_approx_succ _ e₁ _ _ (by simpa using e) (exp_approx_end _ _ _ e₁ h)

Premises used: Real.exp_approx_end, Real.exp_approx_succ
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
rm : ℝ
er : (↑m : ℝ) = rm
h : |rexp 1 - expNear m 1 ((a₁ - 1) * rm)| ≤ HPow.hPow (α := ℝ) |1| m / (↑m.factorial : ℝ) * (b₁ * rm)
⊢ |rexp 1 - expNear m 1 ((a₁ - 1) * (↑m : ℝ))| ≤ HPow.hPow (α := ℝ) |1| m / (↑m.factorial : ℝ) * (b₁ * (↑m : ℝ))

Tactic:
subst er
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * (↑m : ℝ))| ≤ HPow.hPow (α := ℝ) |1| m / (↑m.factorial : ℝ) * (b₁ * (↑m : ℝ))
⊢ |rexp 1 - expNear n 1 a₁| ≤ HPow.hPow (α := ℝ) |1| n / (↑n.factorial : ℝ) * b₁

Tactic:
exp_approx_succ _ en _ _ ?_ h

Premises used: Real.exp_approx_succ
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * (↑m : ℝ))| ≤ HPow.hPow (α := ℝ) |1| m / (↑m.factorial : ℝ) * (b₁ * (↑m : ℝ))
refine :
  |1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * ((a₁ - 1) * (↑m : ℝ)) - a₁| ≤
    b₁ - HDiv.hDiv (α := ℝ) |1| (↑m : ℝ) * (b₁ * (↑m : ℝ))
⊢ |rexp 1 - expNear n 1 a₁| ≤ HPow.hPow (α := ℝ) |1| n / (↑n.factorial : ℝ) * b₁

Tactic:
refine exp_approx_succ _ en _ _ ?_ h

Premises used: Real.exp_approx_succ
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * (↑m : ℝ))| ≤ HPow.hPow (α := ℝ) |1| m / (↑m.factorial : ℝ) * (b₁ * (↑m : ℝ))
simp : |1 + (↑m : ℝ)⁻¹ * ((a₁ - 1) * (↑m : ℝ)) - a₁| ≤ b₁ - (↑m : ℝ)⁻¹ * (b₁ * (↑m : ℝ))
⊢ |1 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * ((a₁ - 1) * (↑m : ℝ)) - a₁| ≤
    b₁ - HDiv.hDiv (α := ℝ) |1| (↑m : ℝ) * (b₁ * (↑m : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * (↑m : ℝ))| ≤ HPow.hPow (α := ℝ) |1| m / (↑m.factorial : ℝ) * (b₁ * (↑m : ℝ))
norm_cast : ¬m = 0
⊢ Ne (α := ℝ) (↑m : ℝ) 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * (↑m : ℝ))| ≤ HPow.hPow (α := ℝ) |1| m / (↑m.factorial : ℝ) * (b₁ * (↑m : ℝ))
⊢ ¬m = 0

Tactic:
lia
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * (↑m : ℝ))| ≤ HPow.hPow (α := ℝ) |1| m / (↑m.factorial : ℝ) * (b₁ * (↑m : ℝ))
field_simp : |1 + (a₁ - 1) - a₁| ≤ b₁ * HSub.hSub (α := ℝ) 1 1
⊢ |1 + (↑m : ℝ)⁻¹ * ((a₁ - 1) * (↑m : ℝ)) - a₁| ≤ b₁ - (↑m : ℝ)⁻¹ * (b₁ * (↑m : ℝ))

Tactic:
field_simp [show (m : ℝ) ≠ 0 by norm_cast; lia]
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * (↑m : ℝ))| ≤ HPow.hPow (α := ℝ) |1| m / (↑m.factorial : ℝ) * (b₁ * (↑m : ℝ))
⊢ |1 + (a₁ - 1) - a₁| ≤ b₁ * HSub.hSub (α := ℝ) 1 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x a b : ℝ
h : |rexp x - expNear 0 x a| ≤ HPow.hPow (β := ℕ) |x| 0 / (↑(Nat.factorial 0) : ℝ) * b
⊢ |rexp x - a| ≤ b

Tactic:
simpa using h
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
⊢ 0 < HPow.hPow (β := ℕ) x 3

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
⊢ HPow.hPow (β := ℕ) x 3 = 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
⊢ 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)

Tactic:
have H : 0 < 1 - (1 + x + x ^ 2) * (1 - x) := calc
    0 < x ^ 3 := by positivity
    _ = 1 - (1 + x + x ^ 2) * (1 - x) := by ring
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
⊢ rexp x ≤
    ∑ m ∈ range 3, x ^ m / (↑m.factorial : ℝ) +
      HPow.hPow (β := ℕ) x 3 * HAdd.hAdd (α := ℝ) (↑3 : ℝ) 1 / HMul.hMul (α := ℝ) (↑(Nat.factorial 3) : ℝ) (↑3 : ℝ)

Tactic:
exp_bound' h1.le h2.le zero_lt_three

Premises used: zero_lt_three, LT.lt.le, Real.exp_bound'
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
rw :
  ∑ x_1 ∈ range (HAdd.hAdd (α := ℕ) 1 1), x ^ x_1 / (↑x_1.factorial : ℝ) +
        x ^ HAdd.hAdd (α := ℕ) 1 1 / (↑(HAdd.hAdd (α := ℕ) 1 1).factorial : ℝ) +
      x ^ (HAdd.hAdd (α := ℕ) 1 1 + 1) * HAdd.hAdd (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) 1 /
        HMul.hMul (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1).factorial : ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) ≤
    1 + x + HPow.hPow (β := ℕ) x 2
⊢ ∑ m ∈ range (HAdd.hAdd (α := ℕ) 1 1 + 1), x ^ m / (↑m.factorial : ℝ) +
      x ^ (HAdd.hAdd (α := ℕ) 1 1 + 1) * HAdd.hAdd (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) 1 /
        HMul.hMul (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1).factorial : ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) ≤
    1 + x + HPow.hPow (β := ℕ) x 2

Tactic:
rw [Finset.sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
rw :
  ∑ x_1 ∈ range 1, x ^ x_1 / (↑x_1.factorial : ℝ) + HPow.hPow (β := ℕ) x 1 / (↑(Nat.factorial 1) : ℝ) +
        x ^ HAdd.hAdd (α := ℕ) 1 1 / (↑(HAdd.hAdd (α := ℕ) 1 1).factorial : ℝ) +
      x ^ (HAdd.hAdd (α := ℕ) 1 1 + 1) * HAdd.hAdd (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) 1 /
        HMul.hMul (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1).factorial : ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) ≤
    1 + x + HPow.hPow (β := ℕ) x 2
⊢ ∑ x_1 ∈ range (HAdd.hAdd (α := ℕ) 1 1), x ^ x_1 / (↑x_1.factorial : ℝ) +
        x ^ HAdd.hAdd (α := ℕ) 1 1 / (↑(HAdd.hAdd (α := ℕ) 1 1).factorial : ℝ) +
      x ^ (HAdd.hAdd (α := ℕ) 1 1 + 1) * HAdd.hAdd (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) 1 /
        HMul.hMul (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1).factorial : ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) ≤
    1 + x + HPow.hPow (β := ℕ) x 2

Tactic:
rw [Finset.sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
rw :
  ∑ x_1 ∈ range 0, x ^ x_1 / (↑x_1.factorial : ℝ) + HPow.hPow (β := ℕ) x 0 / (↑(Nat.factorial 0) : ℝ) +
          HPow.hPow (β := ℕ) x 1 / (↑(Nat.factorial 1) : ℝ) +
        x ^ HAdd.hAdd (α := ℕ) 1 1 / (↑(HAdd.hAdd (α := ℕ) 1 1).factorial : ℝ) +
      x ^ (HAdd.hAdd (α := ℕ) 1 1 + 1) * HAdd.hAdd (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) 1 /
        HMul.hMul (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1).factorial : ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) ≤
    1 + x + HPow.hPow (β := ℕ) x 2
⊢ ∑ x_1 ∈ range 1, x ^ x_1 / (↑x_1.factorial : ℝ) + HPow.hPow (β := ℕ) x 1 / (↑(Nat.factorial 1) : ℝ) +
        x ^ HAdd.hAdd (α := ℕ) 1 1 / (↑(HAdd.hAdd (α := ℕ) 1 1).factorial : ℝ) +
      x ^ (HAdd.hAdd (α := ℕ) 1 1 + 1) * HAdd.hAdd (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) 1 /
        HMul.hMul (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1).factorial : ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) ≤
    1 + x + HPow.hPow (β := ℕ) x 2

Tactic:
rw [Finset.sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
repeat :
  ∑ x_1 ∈ range 0, x ^ x_1 / (↑x_1.factorial : ℝ) + HPow.hPow (β := ℕ) x 0 / (↑(Nat.factorial 0) : ℝ) +
          HPow.hPow (β := ℕ) x 1 / (↑(Nat.factorial 1) : ℝ) +
        x ^ HAdd.hAdd (α := ℕ) 1 1 / (↑(HAdd.hAdd (α := ℕ) 1 1).factorial : ℝ) +
      x ^ (HAdd.hAdd (α := ℕ) 1 1 + 1) * HAdd.hAdd (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) 1 /
        HMul.hMul (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1).factorial : ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) ≤
    1 + x + HPow.hPow (β := ℕ) x 2
⊢ ∑ m ∈ range (HAdd.hAdd (α := ℕ) 1 1 + 1), x ^ m / (↑m.factorial : ℝ) +
      x ^ (HAdd.hAdd (α := ℕ) 1 1 + 1) * HAdd.hAdd (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) 1 /
        HMul.hMul (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1).factorial : ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) ≤
    1 + x + HPow.hPow (β := ℕ) x 2

Tactic:
repeat rw [Finset.sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
norm_num : 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2
⊢ ∑ x_1 ∈ range 0, x ^ x_1 / (↑x_1.factorial : ℝ) + HPow.hPow (β := ℕ) x 0 / (↑(Nat.factorial 0) : ℝ) +
          HPow.hPow (β := ℕ) x 1 / (↑(Nat.factorial 1) : ℝ) +
        x ^ HAdd.hAdd (α := ℕ) 1 1 / (↑(HAdd.hAdd (α := ℕ) 1 1).factorial : ℝ) +
      x ^ (HAdd.hAdd (α := ℕ) 1 1 + 1) * HAdd.hAdd (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) 1 /
        HMul.hMul (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1).factorial : ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1 + 1) : ℝ) ≤
    1 + x + HPow.hPow (β := ℕ) x 2

Tactic:
norm_num [Nat.factorial]

Premises used: Nat.factorial
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
nlinarith :
  1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 →
    18 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 18
nlinarith₁ :
  1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 →
    9 * HPow.hPow (α := ℝ) (β := ℕ) 1 2 = 9
nlinarith₂ :
  1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 →
    HDiv.hDiv (α := ℝ) 2 2 = 1
nlinarith₃ :
  1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 →
    HMul.hMul (α := ℝ) 9 2 = 18
nlinarith₄ :
  1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 →
    1 * HPow.hPow (α := ℝ) (β := ℕ) 1 3 = 1
nlinarith₅ :
  1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 →
    HMul.hMul (α := ℝ) 1 1 = 1
nlinarith₆ :
  1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 → 18 / 18 = 1
nlinarith₇ :
  1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 →
    HMul.hMul (α := ℝ) 1 18 = 18
nlinarith₈ :
  1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 →
    GT.gt (α := ℝ) 18 0
nlinarith₉ :
  1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 →
    5 * (0 - (1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x))) +
          (HMul.hMul (α := ℝ) 18 1 + 18 * x + 18 * HPow.hPow (β := ℕ) (1 * x) 2 -
            (HMul.hMul (α := ℝ) 18 1 + 18 * x + 9 * HPow.hPow (β := ℕ) (1 * x) 2 +
              1 * HPow.hPow (β := ℕ) (1 * x) 3 * HMul.hMul (α := ℝ) 1 4)) +
        9 * (0 - (0 - HPow.hPow (β := ℕ) x 2) * (x - 1)) =
      0
nlinarith₁₀ :
  1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 →
    GT.gt (α := ℝ) 5 0
nlinarith₁₁ :
  1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 →
    GT.gt (α := ℝ) 9 0
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
rw : (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x) < 1
rw₁ : 0 < 1 - x
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 < 1 / (1 - x)

Tactic:
rw [lt_div_iff₀]

Premises used: lt_div_iff₀
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
nlinarith :
  1 ≤ (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x) →
    0 - (1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)) + (1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)) = 0
⊢ (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x) < 1

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
nlinarith : 1 - x ≤ 0 → x - 1 + (1 - x - 0) = 0
⊢ 0 < 1 - x

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
exp :
  ∑ m ∈ range 3, x ^ m / (↑m.factorial : ℝ) +
      HPow.hPow (β := ℕ) x 3 * HAdd.hAdd (α := ℝ) (↑3 : ℝ) 1 / HMul.hMul (α := ℝ) (↑(Nat.factorial 3) : ℝ) (↑3 : ℝ) ≤
    1 + x + HPow.hPow (β := ℕ) x 2
exp₁ : 1 + x + HPow.hPow (β := ℕ) x 2 < 1 / (1 - x)
⊢ rexp x < 1 / (1 - x)

Tactic:
calc
    exp x ≤ _ := exp_bound' h1.le h2.le zero_lt_three
    _ ≤ 1 + x + x ^ 2 := by
      -- Porting note: was `norm_num [Finset.sum] <;> nlinarith`
      -- This proof should be restored after the norm_num plugin for big operators is ported.
      -- (It may also need the positivity extensions in https://github.com/leanprover-community/mathlib4/pull/3907.)
      rw [show 3 = 1 + 1 + 1 from rfl]
      repeat rw [Finset.sum_range_succ]
      norm_num [Nat.factorial]
      nlinarith
    _ < 1 / (1 - x) := by rw [lt_div_iff₀] <;> nlinarith

Premises used: zero_lt_three, HSub.hSub, LT.lt.le, Real.exp, Real.exp_bound', OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1 : 0 ≤ x
h2 : x < 1
inl : ∀ (h1 : LE.le (α := ℝ) 0 0) (h2 : LT.lt (α := ℝ) 0 1), rexp 0 ≤ 1 / HSub.hSub (α := ℝ) 1 0
inr : ∀ (h1 : 0 < x), rexp x ≤ 1 / (1 - x)
⊢ rexp x ≤ 1 / (1 - x)

Tactic:
rcases eq_or_lt_of_le h1 with (rfl | h1)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
h1 : LE.le (α := ℝ) 0 0
h2 : LT.lt (α := ℝ) 0 1
⊢ rexp 0 ≤ 1 / HSub.hSub (α := ℝ) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1_1 : 0 ≤ x
h2 : x < 1
h1 : 0 < x
⊢ rexp x ≤ 1 / (1 - x)

Tactic:
(exp_bound_div_one_sub_of_interval' h1 h2).le

Premises used: LT.lt.le, Real.exp_bound_div_one_sub_of_interval'
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
h1_1 : 0 ≤ x
h2 : x < 1
h1 : 0 < x
⊢ rexp x ≤ 1 / (1 - x)

Tactic:
exact (exp_bound_div_one_sub_of_interval' h1 h2).le

Premises used: LT.lt.le, Real.exp_bound_div_one_sub_of_interval'
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : x ≠ 0
inl : ∀ (hx : 0 < x), x + 1 < rexp x
inr : ∀ (hx : x < 0), x + 1 < rexp x
⊢ x + 1 < rexp x

Tactic:
obtain hx | hx := hx.symm.lt_or_gt

Premises used: Ne.symm, Ne.lt_or_gt
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : 0 < x
⊢ x + 1 < rexp x

Tactic:
add_one_lt_exp_of_pos hx

Premises used: _private.0.Real.add_one_lt_exp_of_pos
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : 0 < x
⊢ x + 1 < rexp x

Tactic:
exact add_one_lt_exp_of_pos hx

Premises used: _private.0.Real.add_one_lt_exp_of_pos
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
inr : ∀ (h' : 1 ≤ -x), x + 1 < rexp x
inr₁ : ∀ (h' : -x < 1), x + 1 < rexp x
⊢ x + 1 < rexp x

Tactic:
obtain h' | h' := le_or_gt 1 (-x)

Premises used: le_or_gt, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
h' : 1 ≤ -x
linarith : rexp x ≤ x + 1 → 1 - -x + (rexp x - (x + 1)) + (0 - rexp x) = 0
⊢ x + 1 < rexp x

Tactic:
linarith [x.exp_pos]

Premises used: Real.exp_pos
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
h' : -x < 1
linarith : x + 1 ≤ 0 → -x - 1 + (x + 1 - 0) = 0
⊢ 0 < x + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
h' : -x < 1
⊢ 0 < x + 1

Tactic:
have hx' : 0 < x + 1 := by linarith
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
h' : -x < 1
hx' : 0 < x + 1
⊢ x + 1 < rexp x

Tactic:
simpa [add_comm, exp_neg, inv_lt_inv₀ (exp_pos _) hx']
    using exp_bound_div_one_sub_of_interval' (neg_pos.2 hx) h'

Premises used: Iff.mpr, neg_pos, add_comm, Real.exp_bound_div_one_sub_of_interval', Real.exp_neg, inv_lt_inv₀, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
inl : HAdd.hAdd (α := ℝ) 0 1 ≤ rexp 0
inr : ∀ (hx : x ≠ 0), x + 1 ≤ rexp x
⊢ x + 1 ≤ rexp x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
⊢ HAdd.hAdd (α := ℝ) 0 1 ≤ rexp 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : x ≠ 0
⊢ x + 1 ≤ rexp x

Tactic:
(add_one_lt_exp hx).le

Premises used: LT.lt.le, Real.add_one_lt_exp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : x ≠ 0
⊢ x + 1 ≤ rexp x

Tactic:
exact (add_one_lt_exp hx).le

Premises used: LT.lt.le, Real.add_one_lt_exp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
hx : x ≠ 0
⊢ 1 - x < rexp (-x)

Tactic:
(sub_eq_neg_add _ _).trans_lt <| add_one_lt_exp <| neg_ne_zero.2 hx

Premises used: Iff.mpr, sub_eq_neg_add, Eq.trans_lt, neg_ne_zero, Real.add_one_lt_exp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
⊢ 1 - x ≤ rexp (-x)

Tactic:
(sub_eq_neg_add _ _).trans_le <| add_one_le_exp _

Premises used: sub_eq_neg_add, Eq.trans_le, Real.add_one_le_exp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
inl : ∀ (ht' : t ≤ (↑0 : ℝ)), HPow.hPow (β := ℕ) (1 - t / (↑0 : ℝ)) 0 ≤ rexp (-t)
inr : ∀ (hn : n ≠ 0), (1 - t / (↑n : ℝ)) ^ n ≤ rexp (-t)
⊢ (1 - t / (↑n : ℝ)) ^ n ≤ rexp (-t)

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
t : ℝ
ht' : t ≤ (↑0 : ℝ)
inl : t ≤ 0
⊢ HPow.hPow (β := ℕ) (1 - t / (↑0 : ℝ)) 0 ≤ rexp (-t)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
t : ℝ
ht' : t ≤ (↑0 : ℝ)
inl inl₁ inl₂ inl₃ : ∀ (ht' : t ≤ 0), t ≤ 0
⊢ t ≤ 0

Tactic:
rwa [Nat.cast_zero] at ht'

Premises used: Nat.cast_zero
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
hn : n ≠ 0
ha : 0 ≤ 1 - t / (↑n : ℝ)
hab : 1 - t / (↑n : ℝ) ≤ rexp (-(t / (↑n : ℝ)))
⊢ (1 - t / (↑n : ℝ)) ^ n ≤ rexp (-(t / (↑n : ℝ))) ^ n

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
hn : n ≠ 0
⊢ 0 ≤ 1 - t / (↑n : ℝ)

Tactic:
sub_nonneg.2 <| div_le_one_of_le₀ ht' n.cast_nonneg

Premises used: div_le_one_of_le₀, Iff.mpr, Nat.cast_nonneg, sub_nonneg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
hn : n ≠ 0
⊢ 0 ≤ 1 - t / (↑n : ℝ)

Tactic:
exact sub_nonneg.2 <| div_le_one_of_le₀ ht' n.cast_nonneg

Premises used: div_le_one_of_le₀, Iff.mpr, Nat.cast_nonneg, sub_nonneg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
hn : n ≠ 0
⊢ 1 - t / (↑n : ℝ) ≤ rexp (-(t / (↑n : ℝ)))

Tactic:
one_sub_le_exp_neg _

Premises used: Real.one_sub_le_exp_neg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
hn : n ≠ 0
⊢ 1 - t / (↑n : ℝ) ≤ rexp (-(t / (↑n : ℝ)))

Tactic:
exact one_sub_le_exp_neg _

Premises used: Real.one_sub_le_exp_neg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
hn : n ≠ 0
h : Ne (α := ℝ) (↑n : ℝ) 0
⊢ rexp (-(t / (↑n : ℝ))) ^ n = rexp (-t)

Tactic:
rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]

Premises used: div_mul_cancel₀, mul_comm, Real.exp_nat_mul, mul_neg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
hn : n ≠ 0
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
n : ℕ
t : ℝ
ht' : t ≤ (↑n : ℝ)
hn : n ≠ 0
t₁ : (1 - t / (↑n : ℝ)) ^ n ≤ rexp (-(t / (↑n : ℝ))) ^ n
t₂ : rexp (-(t / (↑n : ℝ))) ^ n = rexp (-t)
⊢ (1 - t / (↑n : ℝ)) ^ n ≤ rexp (-t)

Tactic:
calc
    (1 - t / n) ^ n ≤ rexp (-(t / n)) ^ n := by
      gcongr
      · exact sub_nonneg.2 <| div_le_one_of_le₀ ht' n.cast_nonneg
      · exact one_sub_le_exp_neg _
    _ = rexp (-t) := by rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]; positivity

Premises used: HSub.hSub, HDiv.hDiv, Real.exp, Nat.cast, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x c : ℝ
hc : 0 < c
rw : c * x ≤ rexp (c * x)
⊢ x ≤ c⁻¹ * rexp (c * x)

Tactic:
rw [le_inv_mul_iff₀ hc]

Premises used: le_inv_mul_iff₀
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x c : ℝ
hc : 0 < c
⊢ c * x ≤ c * x + 1

Tactic:
le_add_of_nonneg_right zero_le_one

Premises used: zero_le_one, le_add_of_nonneg_right
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x c : ℝ
hc : 0 < c
⊢ c * x + 1 ≤ rexp (c * x)

Tactic:
Real.add_one_le_exp (c * x)

Premises used: HMul.hMul, Real.add_one_le_exp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x c : ℝ
hc : 0 < c
⊢ c * x ≤ rexp (c * x)

Tactic:
calc c * x
  _ ≤ c * x + 1 := le_add_of_nonneg_right zero_le_one
  _ ≤ _ := Real.add_one_le_exp (c * x)

Premises used: HMul.hMul, zero_le_one, le_add_of_nonneg_right, Real.add_one_le_exp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
ι : Type u_1
s : Finset ι
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
⊢ ∏ i ∈ s, (1 + f i) ≤ rexp (∑ i ∈ s, f i)

Tactic:
(Finset.prod_le_prod (fun i _ ↦ add_nonneg zero_le_one (hf i))
    fun i _ ↦ (add_comm 1 (f i)).le.trans (add_one_le_exp _)).trans
    (exp_sum s f).symm.le

Premises used: Finset.prod_le_prod, Eq.le, add_nonneg, add_comm, zero_le_one, LE.le.trans, OfNat.ofNat, Eq.symm, Real.add_one_le_exp, Real.exp_sum
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
rw : ‖(↑(Real.exp x) : ℂ)‖ = Real.exp x
⊢ ‖cexp (↑x : ℂ)‖ = Real.exp x

Tactic:
rw [← ofReal_exp]

Premises used: Complex.ofReal_exp
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
⊢ ‖(↑(Real.exp x) : ℂ)‖ = Real.exp x

Tactic:
Complex.norm_of_nonneg (le_of_lt (Real.exp_pos _))

Premises used: le_of_lt, Complex.norm_of_nonneg, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.Exponential
Goal:
x : ℝ
⊢ ‖(↑(Real.exp x) : ℂ)‖ = Real.exp x

Tactic:
exact Complex.norm_of_nonneg (le_of_lt (Real.exp_pos _))

Premises used: le_of_lt, Complex.norm_of_nonneg, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
h :
  |rexp 1 - expNear 0 1 (2244083 / 825552)| ≤
    HPow.hPow (α := ℝ) (β := ℕ) |1| 0 / (↑(Nat.factorial 0) : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10)
⊢ |rexp 1 - 2244083 / 825552| ≤ 1 / HPow.hPow (α := ℝ) (β := ℕ) 10 10

Tactic:
apply exp_approx_start

Premises used: Real.exp_approx_start
-- Module: Mathlib.Analysis.Complex.ExponentialBounds
Goal:
⊢ Eq (α := ℕ) 1 1

Tactic:
rfl