x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ 0 < sin x / cos x
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ 0 < tan x
rw [tan_eq_sin_div_cos]
no goals
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ 0 < sin x / cos x
exact div_pos (sin_pos_of_pos_of_lt_pi h0x (by linarith)) (cos_pos_of_mem_Ioo ⟨by linarith, hxp⟩)
no goals
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ x < π
linarith
no goals
x : ℝ
h0x : 0 < x
hxp : x < π / 2
⊢ -(π / 2) < x
linarith