x y : ℝ
hx₁ : -(π / 2) < x
hy₂ : y < π / 2
hxy : x < y
hx0 : x ≤ 0
hy0 : y ≤ 0
⊢ tan (-y) < tan (-x)
x y : ℝ
hx₁ : -(π / 2) < x
hy₂ : y < π / 2
hxy : x < y
hx0 : x ≤ 0
hy0 : y ≤ 0
⊢ -tan y < -tan x
rw [← tan_neg, ← tan_neg]
no goals
x y : ℝ
hx₁ : -(π / 2) < x
hy₂ : y < π / 2
hxy : x < y
hx0 : x ≤ 0
hy0 : y ≤ 0
⊢ tan (-y) < tan (-x)
exact tan_lt_tan_of_nonneg_of_lt_pi_div_two (neg_nonneg.2 hy0) (neg_lt.2 hx₁) (neg_lt_neg hxy)
x y : ℝ
hx₁ : -(π / 2) < x
hy₂ : y < π / 2
hxy : x < y
hx0 : x ≤ 0
hy0✝ : 0 ≤ y
hy0 : 0 = y
⊢ tan x < 0
x y : ℝ
hx₁ : -(π / 2) < x
hy₂ : y < π / 2
hxy : x < y
hx0 : x ≤ 0
hy0✝ : 0 ≤ y
hy0 : 0 = y
⊢ tan x < tan y
rw [← hy0, tan_zero]
no goals
x y : ℝ
hx₁ : -(π / 2) < x
hy₂ : y < π / 2
hxy : x < y
hx0 : x ≤ 0
hy0✝ : 0 ≤ y
hy0 : 0 = y
⊢ tan x < 0
exact tan_neg_of_neg_of_pi_div_two_lt (hy0.symm ▸ hxy) hx₁
no goals
x y : ℝ
hx₁ : -(π / 2) < x
hy₂ : y < π / 2
hxy : x < y
hx0 : 0 ≤ x
hy0 : y ≤ 0
⊢ tan x < tan y
linarith