case h.e'_3

⊢ tan = fun x => cos⁻¹ x * sin x
⊢ Tendsto tan (𝓝[Ioi (-(π / 2))] (-(π / 2))) atBot
convert tendsto_cos_neg_pi_div_two.inv_tendsto_zero.atTop_mul_neg (by norm_num)
    tendsto_sin_neg_pi_div_two using 1
no goals
case h.e'_3

⊢ tan = fun x => cos⁻¹ x * sin x
simp only [Pi.inv_apply, ← div_eq_inv_mul, ← tan_eq_sin_div_cos]
no goals
⊢ -1 < 0
norm_num