case inl
x : ℝ
h : 0 < x
h' : 1 < x
⊢ sin x < x

case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
⊢ sin x < x
x : ℝ
h : 0 < x
⊢ sin x < x
cases' lt_or_le 1 x with h' h'
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
⊢ sin x < x
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
⊢ sin x < x
have hx : |x| = x := abs_of_nonneg h.le
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : sin x - (x - x ^ 3 / 6) ≤ abs x ^ 4 * (5 / 96)
⊢ sin x < x
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
⊢ sin x < x
have := le_of_abs_le (sin_bound <| show |x| ≤ 1 by rwa [hx])
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ sin x < x
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : sin x - (x - x ^ 3 / 6) ≤ abs x ^ 4 * (5 / 96)
⊢ sin x < x
rw [sub_le_iff_le_add', hx] at this
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x - x ^ 3 / 6 + x ^ 4 * (5 / 96) < x
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ sin x < x
apply this.trans_lt
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x ^ 4 * (5 / 96) < x ^ 3 * 6⁻¹
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x - x ^ 3 / 6 + x ^ 4 * (5 / 96) < x
rw [sub_add, sub_lt_self_iff, sub_pos, div_eq_mul_inv (x ^ 3)]
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x ^ 4 ≤ x ^ 3
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x ^ 4 * (5 / 96) < x ^ 3 * 6⁻¹
refine' mul_lt_mul' _ (by norm_num) (by norm_num) (pow_pos h 3)
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ 3 ≤ 4
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x ^ 4 ≤ x ^ 3
apply pow_le_pow_of_le_one h.le h'
no goals
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ 3 ≤ 4
norm_num
no goals
case inl
x : ℝ
h : 0 < x
h' : 1 < x
⊢ sin x < x
exact (sin_le_one x).trans_lt h'
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 : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ 5 / 96 < 6⁻¹
norm_num
no goals
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : abs x = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ 0 ≤ 5 / 96
norm_num