no goals
E : Type ?u.610728
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
hR : R ≠ 0
⊢ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹) = 2 * ↑π * I
simp [circleIntegral, ← div_eq_mul_inv, mul_div_cancel_left _ (circleMap_ne_center hR),
  intervalIntegral.integral_const I]