-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_bound {x : ℝ} (hx : |x| ≤ 1) : |sin x - (x - x ^ 3 / 6)| ≤ |x| ^ 4 * (5 / 96) :=
  calc
    |sin x - (x - x ^ 3 / 6)| = ‖Complex.sin x - (x - x ^ 3 / 6 : ℝ)‖

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
⊢ ‖↑(sin x - (x - x ^ 3 / 6))‖ = ‖Complex.sin ↑x - ↑(x - x ^ 3 / 6)‖

Tactic:
simp

Result:
no goals

Proof state:
case a
x : ℝ
hx : |x| ≤ 1
⊢ sin x - (cexp (-(↑x * I))).im - (2 * x - x * x * x * 3⁻¹) =
    sin x - (x + -(x * x * x * ((1 + 1 + 1 + 1 + 1 + 1) * ((1 + 1 + 1 + 1 + 1 + 1)⁻¹ * (1 + 1 + 1 + 1 + 1 + 1)⁻¹)))) -
      ((cexp (-(↑x * I))).im -
        (-x + x * x * x * ((1 + 1 + 1 + 1 + 1 + 1) * ((1 + 1 + 1 + 1 + 1 + 1)⁻¹ * (1 + 1 + 1 + 1 + 1 + 1)⁻¹))))

Tactic:
ring

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ 3 * 2 = 6

Tactic:
norm_num

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ 1
⊢ (cexp (-(↑x * I)) - cexp (↑x * I)) * I - (2 * ↑x - ↑1 * ↑x * ↑x * ↑x / 3) =
    (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)))) *
      I

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

Result:
case a
x : ℝ
hx : |x| ≤ 1
⊢ sin x - (cexp (-(↑x * I))).im - (2 * x - x * x * x * 3⁻¹) =
    sin x - (x + -(x * x * x * ((1 + 1 + 1 + 1 + 1 + 1) * ((1 + 1 + 1 + 1 + 1 + 1)⁻¹ * (1 + 1 + 1 + 1 + 1 + 1)⁻¹)))) -
      ((cexp (-(↑x * I))).im -
        (-x + x * x * x * ((1 + 1 + 1 + 1 + 1 + 1) * ((1 + 1 + 1 + 1 + 1 + 1)⁻¹ * (1 + 1 + 1 + 1 + 1 + 1)⁻¹))))

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) - ∑ 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
⊢ ‖-↑x * I‖ ≤ 1

Tactic:
simpa

Result:
no goals

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) * I / 2‖ +
      ‖-((cexp (↑x * I) - ∑ m ∈ range 4, (↑x * I) ^ m / ↑m.factorial) * I) / 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 [add_comm, map_div₀]

Result:
no goals

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

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

Result:
x : ℝ
hx : |x| ≤ 1
⊢ (cexp (-(↑x * I)) - cexp (↑x * I)) * I - (2 * ↑x - ↑1 * ↑x * ↑x * ↑x / 3) =
    (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)))) *
      I

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

Tactic:
simpa

Result:
no goals

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

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

Result:
x : ℝ
hx : |x| ≤ 1
⊢ ‖↑(sin x - (x - x ^ 3 / 6))‖ = ‖Complex.sin ↑x - ↑(x - x ^ 3 / 6)‖

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

Tactic:
simp [Complex.sin, sub_div, add_div, neg_div, mul_div_cancel_left₀ _ (two_ne_zero' ℂ),
  div_div, show (3 : ℂ) * 2 = 6 by norm_num]

Result:
no goals

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

Tactic:
rw [sub_mul, sub_eq_add_neg, add_div]

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