no goals
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
⊢ 0 < 2
norm_num
no goals
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
⊢ x ≤ 1 * 2
simpa
no goals
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
⊢ 0 < 2
norm_num
no goals
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
⊢ abs' (x / 2) ≤ 1
rwa [_root_.abs_of_nonneg (le_of_lt (half_pos hx0))]
no goals
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
⊢ 2 * sin (x / 2) * cos (x / 2) = sin x
rw [← sin_two_mul, two_mul, add_halves]