case inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
s : Set ℂ
hs : Set.Countable s
h0 : 0 ≤ 0
hc : ContinuousOn f (closedBall c 0)
hd : ∀ (z : ℂ), z ∈ ball c 0 \ s → DifferentiableAt ℂ f z
⊢ (∮ (z : ℂ) in C(c, 0), f z) = 0

case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
h0✝ : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (z : ℂ), z ∈ ball c R \ s → DifferentiableAt ℂ f z
h0 : 0 < R
⊢ (∮ (z : ℂ) in C(c, R), f z) = 0
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
h0 : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (z : ℂ), z ∈ ball c R \ s → DifferentiableAt ℂ f z
⊢ (∮ (z : ℂ) in C(c, R), f z) = 0
rcases h0.eq_or_lt with (rfl | h0)
no goals
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
h0✝ : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (z : ℂ), z ∈ ball c R \ s → DifferentiableAt ℂ f z
h0 : 0 < R
⊢ (∮ (z : ℂ) in C(c, R), f z) = 0
calc
  (∮ z in C(c, R), f z) = ∮ z in C(c, R), (z - c)⁻¹ • (z - c) • f z :=
    (circleIntegral.integral_sub_inv_smul_sub_smul _ _ _ _).symm
  _ = (2 * ↑π * I : ℂ) • (c - c) • f c :=
    (circleIntegral_sub_center_inv_smul_of_differentiable_on_off_countable h0 hs
      ((continuousOn_id.sub continuousOn_const).smul hc) fun z hz =>
      (differentiableAt_id.sub_const _).smul (hd z hz))
  _ = 0 := by rw [sub_self, zero_smul, smul_zero]
no goals
case inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
s : Set ℂ
hs : Set.Countable s
h0 : 0 ≤ 0
hc : ContinuousOn f (closedBall c 0)
hd : ∀ (z : ℂ), z ∈ ball c 0 \ s → DifferentiableAt ℂ f z
⊢ (∮ (z : ℂ) in C(c, 0), f z) = 0
apply circleIntegral.integral_radius_zero
no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
h0✝ : 0 ≤ R
f : ℂ → E
c : ℂ
s : Set ℂ
hs : Set.Countable s
hc : ContinuousOn f (closedBall c R)
hd : ∀ (z : ℂ), z ∈ ball c R \ s → DifferentiableAt ℂ f z
h0 : 0 < R
⊢ (2 * ↑π * I) • (c - c) • f c = 0
rw [sub_self, zero_smul, smul_zero]