case h.e'_3

⊢ tan = fun x => cos⁻¹ x * sin x
⊢ Tendsto tan (𝓝[Iio (π / 2)] (π / 2)) atTop
convert tendsto_cos_pi_div_two.inv_tendsto_zero.atTop_mul zero_lt_one tendsto_sin_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]