-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_bound {x : ℝ} (hx : |x| ≤ 1) : |cos x - (1 - x ^ 2 / 2)| ≤ |x| ^ 4 * (5 / 96) :=
  calc
    |cos x - (1 - x ^ 2 / 2)| = ‖Complex.cos x - (1 - (x : ℂ) ^ 2 / 2)‖

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ ‖↑x * I‖ ≤ 1

Tactic:
simpa

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ ‖↑(cos x - (1 - x ^ 2 / 2))‖ = ‖Complex.cos ↑x - (1 - ↑x ^ 2 / 2)‖

Tactic:
simp

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ cexp (↑x * I) + cexp (-(↑x * I)) - (2 - 1 * ↑x * ↑x) =
    cexp (↑x * I) -
        (1 / (↑0 + 1) + 1 * (↑x * I) / (↑0 + 1) + 1 * (↑x * I) * (↑x * I) / (↑0 + 1 + 1) +
          1 * (↑x * I) * (↑x * I) * (↑x * I) / (↑0 + 1 + 1 + 1 + 1 + 1 + 1)) +
      (cexp (-(↑x * I)) -
        (1 / (↑0 + 1) + -(1 * (↑x * I)) / (↑0 + 1) + 1 * (↑x * I) * (↑x * I) / (↑0 + 1 + 1) +
          -(1 * (↑x * I) * (↑x * I) * (↑x * I)) / (↑0 + 1 + 1 + 1 + 1 + 1 + 1)))

Tactic:
apply Complex.ext <;> simp [div_eq_mul_inv, normSq] <;> ring_nf

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ ‖Complex.cos ↑x - (1 - ↑x ^ 2 / 2)‖ = ‖(cexp (↑x * I) + cexp (-↑x * I) - (2 - ↑x ^ 2)) / 2‖

Tactic:
simp [Complex.cos, sub_div, add_div, neg_div, div_self (two_ne_zero' ℂ)]

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ ‖-↑x * I‖ ≤ 1

Tactic:
simpa

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ |cos x - (1 - x ^ 2 / 2)| = ‖Complex.cos ↑x - (1 - ↑x ^ 2 / 2)‖

Tactic:
rw [← Real.norm_eq_abs, ← norm_real]

Result:
x : ℝ
hx : |x| ≤ 1
⊢ ‖↑(cos x - (1 - x ^ 2 / 2))‖ = ‖Complex.cos ↑x - (1 - ↑x ^ 2 / 2)‖

Proof state:
case h₁.hab
x : ℝ
hx : |x| ≤ 1
⊢ ‖cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial‖ ≤
    ‖↑x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹)

Tactic:
exact Complex.exp_bound (by simpa) (by decide)

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ ‖(cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) / 2 +
        (cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) / 2‖ ≤
    ‖(cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) / 2‖ +
      ‖(cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) / 2‖

Tactic:
exact norm_add_le _ _

Result:
no goals

Proof state:
case h₂.hab
x : ℝ
hx : |x| ≤ 1
⊢ ‖cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial‖ ≤
    ‖-↑x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹)

Tactic:
exact Complex.exp_bound (by simpa) (by decide)

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ ‖(cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial +
          (cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial)) /
        2‖ ≤
    ‖(cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) / 2‖ +
      ‖(cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) / 2‖

Tactic:
rw [add_div]

Result:
x : ℝ
hx : |x| ≤ 1
⊢ ‖(cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) / 2 +
        (cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) / 2‖ ≤
    ‖(cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) / 2‖ +
      ‖(cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) / 2‖

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ ‖cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial‖ / 2 ≤
    ‖↑x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 +
      ‖-↑x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2

Tactic:
gcongr

Result:
case h₁.hab
x : ℝ
hx : |x| ≤ 1
⊢ ‖cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial‖ ≤
    ‖↑x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹)

case h₂.hab
x : ℝ
hx : |x| ≤ 1
⊢ ‖cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial‖ ≤
    ‖-↑x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹)

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ 0 < 4

Tactic:
decide

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ ‖(cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) / 2‖ +
      ‖(cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial) / 2‖ =
    ‖cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial‖ / 2 +
      ‖cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial‖ / 2

Tactic:
simp [map_div₀]

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ ‖↑x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 +
      ‖-↑x * I‖ ^ 4 * (↑(Nat.succ 4) * (↑(Nat.factorial 4) * ↑4)⁻¹) / 2 ≤
    |x| ^ 4 * (5 / 96)

Tactic:
norm_num [Nat.factorial]

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ cexp (↑x * I) + cexp (-↑x * I) - (2 - ↑x ^ 2) =
    cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial +
      (cexp (-↑x * I) - ∑ m ∈ range 4, (-↑x * I) ^ m / ↑m.factorial)

Tactic:
simp only [neg_mul, pow_succ, pow_zero, sum_range_succ, range_zero, sum_empty,
Nat.factorial, Nat.cast_succ, zero_add, mul_one, Nat.mul_one, mul_neg, neg_neg]

Result:
x : ℝ
hx : |x| ≤ 1
⊢ cexp (↑x * I) + cexp (-(↑x * I)) - (2 - 1 * ↑x * ↑x) =
    cexp (↑x * I) -
        (1 / (↑0 + 1) + 1 * (↑x * I) / (↑0 + 1) + 1 * (↑x * I) * (↑x * I) / (↑0 + 1 + 1) +
          1 * (↑x * I) * (↑x * I) * (↑x * I) / (↑0 + 1 + 1 + 1 + 1 + 1 + 1)) +
      (cexp (-(↑x * I)) -
        (1 / (↑0 + 1) + -(1 * (↑x * I)) / (↑0 + 1) + 1 * (↑x * I) * (↑x * I) / (↑0 + 1 + 1) +
          -(1 * (↑x * I) * (↑x * I) * (↑x * I)) / (↑0 + 1 + 1 + 1 + 1 + 1 + 1)))