case h1

⊢ Tendsto cos (𝓝[Ioi (-(π / 2))] (-(π / 2))) (𝓝 0)

case h2

⊢ ∀ᶠ (x : ℝ) in 𝓝[Ioi (-(π / 2))] (-(π / 2)), cos x ∈ Ioi 0
⊢ Tendsto cos (𝓝[Ioi (-(π / 2))] (-(π / 2))) (𝓝[Ioi 0] 0)
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
case h.e'_5.h.e'_3

⊢ 0 = cos (-(π / 2))
case h1

⊢ Tendsto cos (𝓝[Ioi (-(π / 2))] (-(π / 2))) (𝓝 0)
convert continuous_cos.continuousWithinAt.tendsto
no goals
case h.e'_5.h.e'_3

⊢ 0 = cos (-(π / 2))
simp
no goals
case h2

⊢ ∀ᶠ (x : ℝ) in 𝓝[Ioi (-(π / 2))] (-(π / 2)), cos x ∈ Ioi 0
filter_upwards [Ioo_mem_nhdsWithin_Ioi
    (left_mem_Ico.mpr (neg_lt_self pi_div_two_pos))]with x hx using cos_pos_of_mem_Ioo hx