x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
⊢ x - x ^ 3 / 4 < sin x
x : ℝ
h : 0 < x
h' : x ≤ 1
⊢ x - x ^ 3 / 4 < sin x
have hx : |x| = x := abs_of_nonneg h.le
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : -(abs x ^ 4 * (5 / 96)) ≤ sin x - (x - x ^ 3 / 6)
⊢ x - x ^ 3 / 4 < sin x
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
⊢ x - x ^ 3 / 4 < sin x
have := neg_le_of_abs_le (sin_bound <| show |x| ≤ 1 by rwa [hx])
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
⊢ x - x ^ 3 / 4 < sin x
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : -(abs x ^ 4 * (5 / 96)) ≤ sin x - (x - x ^ 3 / 6)
⊢ x - x ^ 3 / 4 < sin x
rw [le_sub_iff_add_le, hx] at this
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs 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)
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
⊢ x - x ^ 3 / 4 < sin x
refine' lt_of_lt_of_le _ this
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs 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)
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs 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)
have : x ^ 3 / ↑4 - x ^ 3 / ↑6 = x ^ 3 * 12⁻¹ := by ring
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs 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⁻¹
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs 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)
rw [add_comm, sub_add, sub_neg_eq_add, sub_lt_sub_iff_left, ← lt_sub_iff_add_lt', this]
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs 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
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs 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⁻¹
refine' mul_lt_mul' _ (by norm_num) (by norm_num) (pow_pos h 3)
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs 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
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs 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
apply pow_le_pow_of_le_one h.le h'
no goals
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs 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
norm_num
no goals
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
⊢ abs x ≤ 1
rwa [hx]
no goals
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x
⊢ x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹
ring
no goals
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs 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⁻¹
norm_num
no goals
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs 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
norm_num