no goals
E : Type ?u.19235
inst✝ : NormedAddCommGroup E
c : ℂ
R : ℝ
⊢ circleMap c R '' Ioc 0 (2 * π) = sphere c (Abs.abs R)
rw [← range_circleMap, ← (periodic_circleMap c R).image_Ioc Real.two_pi_pos 0, zero_add]