case h.e'_5.h.e'_3

⊢ -1 = sin (-(π / 2))
⊢ Tendsto sin (𝓝[Ioi (-(π / 2))] (-(π / 2))) (𝓝 (-1))
convert continuous_sin.continuousWithinAt.tendsto using 2
no goals
case h.e'_5.h.e'_3

⊢ -1 = sin (-(π / 2))
simp