x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ sin x / cos x < sin y / cos y
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ tan x < tan y
rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos]
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ sin x / cos x < sin y / cos y
exact
  div_lt_div (sin_lt_sin_of_lt_of_le_pi_div_two (by linarith) (le_of_lt hy₂) hxy)
    (cos_le_cos_of_nonneg_of_le_pi hx₁ (by linarith) (le_of_lt hxy))
    (sin_nonneg_of_nonneg_of_le_pi (by linarith) (by linarith))
    (cos_pos_of_mem_Ioo ⟨by linarith, hy₂⟩)
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ -(π / 2) ≤ x
linarith
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ y ≤ π
linarith
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ 0 ≤ y
linarith
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ y ≤ π
linarith
no goals
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y < π / 2
hxy : x < y
⊢ -(π / 2) < y
linarith