case hc
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
⊢ 2 * ↑π * I ≠ 0
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
rw [← two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
  hs hw hc hd, smul_inv_smul₀]
no goals
case hc
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : Set.Countable s
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ (x : ℂ), x ∈ ball c R \ s → DifferentiableAt ℂ f x
⊢ 2 * ↑π * I ≠ 0
simp [Real.pi_ne_zero, I_ne_zero]