-- Mathlib/Data/Complex/Exponential.lean
theorem exp_bound_div_one_sub_of_interval' {x : ℝ} (h1 : 0 < x) (h2 : x < 1) :
    Real.exp x < 1 / (1 - x)

Proof state:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ 1 + x + x ^ 2 / 2 + x ^ 3 * 4 / 18 ≤ 1 + x + x ^ 2

Tactic:
nlinarith

Result:
no goals

Proof state:
x : ℝ
h1 : 0 < x
h2 : x < 1
⊢ x ^ 3 = 1 - (1 + x + x ^ 2) * (1 - x)

Tactic:
ring

Result:
no goals

Proof state:
x : ℝ
h1 : 0 < x
h2 : x < 1
⊢ 0 < x ^ 3

Tactic:
positivity

Result:
no goals

Proof state:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ ∑ x_1 ∈ range 0, x ^ x_1 / ↑x_1.factorial + x ^ 0 / ↑(Nat.factorial 0) + x ^ 1 / ↑(Nat.factorial 1) +
        x ^ 2 / ↑(Nat.factorial 2) +
      x ^ 3 * (↑3 + 1) / (↑(Nat.factorial 3) * ↑3) ≤
    1 + x + x ^ 2

Tactic:
norm_num [Nat.factorial]

Result:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ 1 + x + x ^ 2 / 2 + x ^ 3 * 4 / 18 ≤ 1 + x + x ^ 2

Proof state:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ ∑ x_1 ∈ range 2, x ^ x_1 / ↑x_1.factorial + x ^ 2 / ↑(Nat.factorial 2) +
      x ^ 3 * (↑3 + 1) / (↑(Nat.factorial 3) * ↑3) ≤
    1 + x + x ^ 2

Tactic:
repeat rw [Finset.sum_range_succ]

Result:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ ∑ x_1 ∈ range 0, x ^ x_1 / ↑x_1.factorial + x ^ 0 / ↑(Nat.factorial 0) + x ^ 1 / ↑(Nat.factorial 1) +
        x ^ 2 / ↑(Nat.factorial 2) +
      x ^ 3 * (↑3 + 1) / (↑(Nat.factorial 3) * ↑3) ≤
    1 + x + x ^ 2

Proof state:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ ∑ x_1 ∈ range 1, x ^ x_1 / ↑x_1.factorial + x ^ 1 / ↑(Nat.factorial 1) + x ^ 2 / ↑(Nat.factorial 2) +
      x ^ 3 * (↑3 + 1) / (↑(Nat.factorial 3) * ↑3) ≤
    1 + x + x ^ 2

Tactic:
rw [Finset.sum_range_succ]

Result:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ ∑ x_1 ∈ range 0, x ^ x_1 / ↑x_1.factorial + x ^ 0 / ↑(Nat.factorial 0) + x ^ 1 / ↑(Nat.factorial 1) +
        x ^ 2 / ↑(Nat.factorial 2) +
      x ^ 3 * (↑3 + 1) / (↑(Nat.factorial 3) * ↑3) ≤
    1 + x + x ^ 2

Proof state:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (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
    erw [Finset.sum_range_succ]
    repeat rw [Finset.sum_range_succ]
    norm_num [Nat.factorial]
    nlinarith
  _ < 1 / (1 - x) := by rw [lt_div_iff₀] <;> nlinarith

Result:
no goals

Proof state:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ ∑ m ∈ range 3, x ^ m / ↑m.factorial + x ^ 3 * (↑3 + 1) / (↑(Nat.factorial 3) * ↑3) ≤ 1 + x + x ^ 2

Tactic:
erw [Finset.sum_range_succ]

Result:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ ∑ x_1 ∈ range 2, x ^ x_1 / ↑x_1.factorial + x ^ 2 / ↑(Nat.factorial 2) +
      x ^ 3 * (↑3 + 1) / (↑(Nat.factorial 3) * ↑3) ≤
    1 + x + x ^ 2

Proof state:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ 1 + x + x ^ 2 < 1 / (1 - x)

Tactic:
rw [lt_div_iff₀] <;> nlinarith

Result:
no goals

Proof state:
x : ℝ
h1 : 0 < x
h2 : x < 1
⊢ rexp x < 1 / (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

Result:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + x ^ 2) * (1 - x)
⊢ rexp x < 1 / (1 - x)