-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
theorem sin_gt_sub_cube {x : ℝ} (h : 0 < x) (h' : x ≤ 1) : x - x ^ 3 / 4 < sin x

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ |x| ≤ 1

Tactic:
rwa [hx]

Result:
no goals

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ 3 ≤ 4

Tactic:
norm_num

Result:
no goals

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
⊢ x - x ^ 3 / 4 < sin x

Tactic:
have hx : |x| = x := abs_of_nonneg h.le

Result:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ x - x ^ 3 / 4 < sin x

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ x ^ 4 ≤ x ^ 3

Tactic:
apply pow_le_pow_of_le_one h.le h'

Result:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ 3 ≤ 4

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ x - x ^ 3 / 4 < -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6)

Tactic:
rw [add_comm, sub_add, sub_neg_eq_add, sub_lt_sub_iff_left, ← lt_sub_iff_add_lt', this]

Result:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ x ^ 4 * (5 / 96) < x ^ 3 * 12⁻¹

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ x - x ^ 3 / 4 < sin x

Tactic:
have := neg_le_of_abs_le (sin_bound <| show |x| ≤ 1 by rwa [hx])

Result:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(|x| ^ 4 * (5 / 96)) ≤ sin x - (x - x ^ 3 / 6)
⊢ x - x ^ 3 / 4 < sin x

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ 5 / 96 < 12⁻¹

Tactic:
norm_num

Result:
no goals

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
⊢ x - x ^ 3 / 4 < -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6)

Tactic:
have : x ^ 3 / ↑4 - x ^ 3 / ↑6 = x ^ 3 * 12⁻¹ := by norm_num [div_eq_mul_inv, ← mul_sub]

Result:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ x - x ^ 3 / 4 < -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6)

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(|x| ^ 4 * (5 / 96)) ≤ sin x - (x - x ^ 3 / 6)
⊢ x - x ^ 3 / 4 < sin x

Tactic:
rw [le_sub_iff_add_le, hx] at this

Result:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
⊢ x - x ^ 3 / 4 < sin x

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ x ^ 4 * (5 / 96) < x ^ 3 * 12⁻¹

Tactic:
refine mul_lt_mul' ?_ (by norm_num) (by norm_num) (pow_pos h 3)

Result:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ x ^ 4 ≤ x ^ 3

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
⊢ 0 ≤ 5 / 96

Tactic:
norm_num

Result:
no goals

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
⊢ x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹

Tactic:
norm_num [div_eq_mul_inv, ← mul_sub]

Result:
no goals

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
⊢ x - x ^ 3 / 4 < sin x

Tactic:
refine lt_of_lt_of_le ?_ this

Result:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
⊢ x - x ^ 3 / 4 < -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6)