case inl
hx1 : -(3 * π / 2) ≤ 0
hx2 : 0 ≤ 3 * π / 2
⊢ cos 0 ≤ 1 / sqrt (0 ^ 2 + 1)

case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
⊢ cos x ≤ 1 / sqrt (x ^ 2 + 1)
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
⊢ cos x ≤ 1 / sqrt (x ^ 2 + 1)
rcases eq_or_ne x 0 with (rfl | hx3)
no goals
case inl
hx1 : -(3 * π / 2) ≤ 0
hx2 : 0 ≤ 3 * π / 2
⊢ cos 0 ≤ 1 / sqrt (0 ^ 2 + 1)
simp
no goals
case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
⊢ cos x ≤ 1 / sqrt (x ^ 2 + 1)
exact (cos_lt_one_div_sqrt_sq_add_one hx1 hx2 hx3).le