n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : abs' (1 + x / ↑m * a₂ - a₁) ≤ b₁ - abs' x / ↑m * b₂
h : abs' (exp x - expNear m x a₂) ≤ abs' x ^ m / ↑(Nat.factorial m) * b₂
⊢ abs' x ^ m / ↑(Nat.factorial m) * b₂ + abs' (expNear m x a₂ - expNear n x a₁) ≤ abs' x ^ n / ↑(Nat.factorial n) * b₁
n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : abs' (1 + x / ↑m * a₂ - a₁) ≤ b₁ - abs' x / ↑m * b₂
h : abs' (exp x - expNear m x a₂) ≤ abs' x ^ m / ↑(Nat.factorial m) * b₂
⊢ abs' (exp x - expNear n x a₁) ≤ abs' x ^ n / ↑(Nat.factorial n) * b₁
refine' (abs_sub_le _ _ _).trans ((add_le_add_right h _).trans _)
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : abs' (1 + x / ↑(n + 1) * a₂ - a₁) ≤ b₁ - abs' x / ↑(n + 1) * b₂
h : abs' (exp x - expNear (n + 1) x a₂) ≤ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂
⊢ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂ + abs' (expNear (n + 1) x a₂ - expNear n x a₁) ≤
    abs' x ^ n / ↑(Nat.factorial n) * b₁
n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : abs' (1 + x / ↑m * a₂ - a₁) ≤ b₁ - abs' x / ↑m * b₂
h : abs' (exp x - expNear m x a₂) ≤ abs' x ^ m / ↑(Nat.factorial m) * b₂
⊢ abs' x ^ m / ↑(Nat.factorial m) * b₂ + abs' (expNear m x a₂ - expNear n x a₁) ≤ abs' x ^ n / ↑(Nat.factorial n) * b₁
subst e₁
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : abs' (1 + x / ↑(n + 1) * a₂ - a₁) ≤ b₁ - abs' x / ↑(n + 1) * b₂
h : abs' (exp x - expNear (n + 1) x a₂) ≤ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂
⊢ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂ +
      abs' (x ^ n / ↑(Nat.factorial n)) * abs' (1 + x / (↑n + 1) * a₂ - a₁) ≤
    abs' x ^ n / ↑(Nat.factorial n) * b₁
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : abs' (1 + x / ↑(n + 1) * a₂ - a₁) ≤ b₁ - abs' x / ↑(n + 1) * b₂
h : abs' (exp x - expNear (n + 1) x a₂) ≤ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂
⊢ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂ + abs' (expNear (n + 1) x a₂ - expNear n x a₁) ≤
    abs' x ^ n / ↑(Nat.factorial n) * b₁
rw [expNear_succ, expNear_sub, abs_mul]
case h.e'_3
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : abs' (1 + x / ↑(n + 1) * a₂ - a₁) ≤ b₁ - abs' x / ↑(n + 1) * b₂
h : abs' (exp x - expNear (n + 1) x a₂) ≤ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂
⊢ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂ +
      abs' (x ^ n / ↑(Nat.factorial n)) * abs' (1 + x / (↑n + 1) * a₂ - a₁) =
    abs' x ^ n / ↑(Nat.factorial n) * (abs' x / ↑(n + 1) * b₂ + abs' (1 + x / ↑(n + 1) * a₂ - a₁))

n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : abs' (1 + x / ↑(n + 1) * a₂ - a₁) ≤ b₁ - abs' x / ↑(n + 1) * b₂
h : abs' (exp x - expNear (n + 1) x a₂) ≤ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂
⊢ 0 ≤ abs' x ^ n / ↑(Nat.factorial n)
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : abs' (1 + x / ↑(n + 1) * a₂ - a₁) ≤ b₁ - abs' x / ↑(n + 1) * b₂
h : abs' (exp x - expNear (n + 1) x a₂) ≤ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂
⊢ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂ +
      abs' (x ^ n / ↑(Nat.factorial n)) * abs' (1 + x / (↑n + 1) * a₂ - a₁) ≤
    abs' x ^ n / ↑(Nat.factorial n) * b₁
convert mul_le_mul_of_nonneg_left (a := abs' x ^ n / ↑(Nat.factorial n))
    (le_sub_iff_add_le'.1 e) ?_ using 1
case h.e'_3
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : abs' (1 + x / ↑(n + 1) * a₂ - a₁) ≤ b₁ - abs' x / ↑(n + 1) * b₂
h : abs' (exp x - expNear (n + 1) x a₂) ≤ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂
⊢ abs' x ^ n * abs' x * ((↑(Nat.factorial n))⁻¹ * (↑n + 1)⁻¹) * b₂ =
    abs' x ^ n * (↑(Nat.factorial n))⁻¹ * (abs' x * (↑n + 1)⁻¹ * b₂)
case h.e'_3
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : abs' (1 + x / ↑(n + 1) * a₂ - a₁) ≤ b₁ - abs' x / ↑(n + 1) * b₂
h : abs' (exp x - expNear (n + 1) x a₂) ≤ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂
⊢ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂ +
      abs' (x ^ n / ↑(Nat.factorial n)) * abs' (1 + x / (↑n + 1) * a₂ - a₁) =
    abs' x ^ n / ↑(Nat.factorial n) * (abs' x / ↑(n + 1) * b₂ + abs' (1 + x / ↑(n + 1) * a₂ - a₁))
simp [mul_add, pow_succ', div_eq_mul_inv, abs_mul, abs_inv, ← pow_abs, mul_inv]
no goals
case h.e'_3
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : abs' (1 + x / ↑(n + 1) * a₂ - a₁) ≤ b₁ - abs' x / ↑(n + 1) * b₂
h : abs' (exp x - expNear (n + 1) x a₂) ≤ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂
⊢ abs' x ^ n * abs' x * ((↑(Nat.factorial n))⁻¹ * (↑n + 1)⁻¹) * b₂ =
    abs' x ^ n * (↑(Nat.factorial n))⁻¹ * (abs' x * (↑n + 1)⁻¹ * b₂)
ac_rfl
no goals
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : abs' (1 + x / ↑(n + 1) * a₂ - a₁) ≤ b₁ - abs' x / ↑(n + 1) * b₂
h : abs' (exp x - expNear (n + 1) x a₂) ≤ abs' x ^ (n + 1) / ↑(Nat.factorial (n + 1)) * b₂
⊢ 0 ≤ abs' x ^ n / ↑(Nat.factorial n)
simp [div_nonneg, abs_nonneg]