-- Mathlib/Data/Complex/Exponential.lean
theorem exp_approx_succ {n} {x a₁ b₁ : ℝ} (m : ℕ) (e₁ : n + 1 = m) (a₂ b₂ : ℝ)
    (e : |1 + x / m * a₂ - a₁| ≤ b₁ - |x| / m * b₂)
    (h : |exp x - expNear m x a₂| ≤ |x| ^ m / m.factorial * b₂) :
    |exp x - expNear n x a₁| ≤ |x| ^ n / n.factorial * b₁

Proof state:
n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂
h : |rexp x - expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂
⊢ |x| ^ m / ↑m.factorial * b₂ + |expNear m x a₂ - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁

Tactic:
subst e₁

Result:
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| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |expNear (n + 1) x a₂ - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁

Proof state:
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| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |expNear (n + 1) x a₂ - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁

Tactic:
rw [expNear_succ, expNear_sub, abs_mul]

Result:
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| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |x ^ n / ↑n.factorial| * |1 + x / (↑n + 1) * a₂ - a₁| ≤
    |x| ^ n / ↑n.factorial * b₁

Proof state:
case h.e'_3
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)⁻¹ * (↑n + 1)⁻¹) * b₂ = |x| ^ n * (↑n.factorial)⁻¹ * (|x| * (↑n + 1)⁻¹ * b₂)

Tactic:
ac_rfl

Result:
no goals

Proof state:
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| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |x ^ n / ↑n.factorial| * |1 + x / (↑n + 1) * a₂ - a₁| ≤
    |x| ^ n / ↑n.factorial * b₁

Tactic:
convert mul_le_mul_of_nonneg_left (a := |x| ^ n / ↑(Nat.factorial n))
    (le_sub_iff_add_le'.1 e) ?_ using 1

Result:
case h.e'_3
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| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |x ^ n / ↑n.factorial| * |1 + x / (↑n + 1) * a₂ - a₁| =
    |x| ^ n / ↑n.factorial * (|x| / ↑(n + 1) * b₂ + |1 + x / ↑(n + 1) * a₂ - a₁|)

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

Proof state:
case h.e'_3
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| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |x ^ n / ↑n.factorial| * |1 + x / (↑n + 1) * a₂ - a₁| =
    |x| ^ n / ↑n.factorial * (|x| / ↑(n + 1) * b₂ + |1 + x / ↑(n + 1) * a₂ - a₁|)

Tactic:
simp [mul_add, pow_succ', div_eq_mul_inv, abs_mul, abs_inv, ← pow_abs, mul_inv, Nat.factorial]

Result:
case h.e'_3
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)⁻¹ * (↑n + 1)⁻¹) * b₂ = |x| ^ n * (↑n.factorial)⁻¹ * (|x| * (↑n + 1)⁻¹ * b₂)

Proof state:
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]

Result:
no goals

Proof state:
n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂
h : |rexp x - expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂
⊢ |rexp x - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁

Tactic:
refine (abs_sub_le _ _ _).trans ((add_le_add_right h _).trans ?_)

Result:
n : ℕ
x a₁ b₁ : ℝ
m : ℕ
e₁ : n + 1 = m
a₂ b₂ : ℝ
e : |1 + x / ↑m * a₂ - a₁| ≤ b₁ - |x| / ↑m * b₂
h : |rexp x - expNear m x a₂| ≤ |x| ^ m / ↑m.factorial * b₂
⊢ |x| ^ m / ↑m.factorial * b₂ + |expNear m x a₂ - expNear n x a₁| ≤ |x| ^ n / ↑n.factorial * b₁