awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 + HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) * ((a₁ - 1) * (↑m : ℝ)) - a₁| ≤
    b₁ - HDiv.hDiv (α := ℝ) |1| (↑m : ℝ) * (b₁ * (↑m : ℝ))
have simp : |1 + (↑m : ℝ)⁻¹ * ((a₁ - 1) * (↑m : ℝ)) - a₁| ≤ b₁ - (↑m : ℝ)⁻¹ * (b₁ * (↑m : ℝ))
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 : ℝ))
⊢ Ne (α := ℝ) (↑m : ℝ) 0
have norm_cast : ¬m = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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 + (↑m : ℝ)⁻¹ * ((a₁ - 1) * (↑m : ℝ)) - a₁| ≤ b₁ - (↑m : ℝ)⁻¹ * (b₁ * (↑m : ℝ))
have field_simp : |1 + (a₁ - 1) - a₁| ≤ b₁ * HSub.hSub (α := ℝ) 1 1
Tactic: field_simp [show (m : ℝ) ≠ 0 by norm_cast; lia]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (hypothesis)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
⊢ rexp x < 1 / (1 - x)
have H : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
⊢ ∑ 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
have 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
Tactic: rw [Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
⊢ ∑ 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
have 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
Tactic: rw [Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
⊢ ∑ 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
have 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
Tactic: rw [Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
⊢ ∑ 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
have 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
Tactic: repeat rw [Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
⊢ ∑ 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
have norm_num : 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2
Tactic: norm_num [Nat.factorial]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2
have nlinarith₆ : 1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 → 18 / 18 = 1
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2
have nlinarith₈ : 1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 →
  GT.gt (α := ℝ) 18 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2
have nlinarith₁₀ : 1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 →
  GT.gt (α := ℝ) 5 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 ≤ 1 + x + HPow.hPow (β := ℕ) x 2
have nlinarith₁₁ : 1 + x + HPow.hPow (β := ℕ) x 2 < 1 + x + HPow.hPow (β := ℕ) x 2 / 2 + HPow.hPow (β := ℕ) x 3 * 4 / 18 →
  GT.gt (α := ℝ) 9 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 < 1 / (1 - x)
have rw : (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x) < 1
Tactic: rw [lt_div_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
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
⊢ 1 + x + HPow.hPow (β := ℕ) x 2 < 1 / (1 - x)
have rw₁ : 0 < 1 - x
Tactic: rw [lt_div_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
⊢ (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x) < 1
have 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
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Exponential (goal)
Goal:
x : ℝ
h1 : 0 < x
h2 : x < 1
H : 0 < 1 - (1 + x + HPow.hPow (β := ℕ) x 2) * (1 - x)
⊢ 0 < 1 - x
have nlinarith : 1 - x ≤ 0 → x - 1 + (1 - x - 0) = 0
Tactic: nlinarith